[GOAL]
b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
[PROOFSTEP]
rw [log, dite_eq_right_iff]
[GOAL]
b n : ℕ
⊢ (∀ (h : b ≤ n ∧ 1 < b),
      (let_fun this := (_ : n / b < n);
        log b (n / b) + 1) =
        0) ↔
    n < b ∨ b ≤ 1
[PROOFSTEP]
simp only [Nat.succ_ne_zero, imp_false, not_and_or, not_le, not_lt]
[GOAL]
b n : ℕ
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, log_eq_zero_iff, not_or, not_lt, not_le]
[GOAL]
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n = log b (n / b) + 1
[PROOFSTEP]
rw [log]
[GOAL]
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ (if h : b ≤ n ∧ 1 < b then
      let_fun this := (_ : n / b < n);
      log b (n / b) + 1
    else 0) =
    log b (n / b) + 1
[PROOFSTEP]
exact if_pos ⟨hn, h⟩
[GOAL]
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y
[PROOFSTEP]
induction' y using Nat.strong_induction_on with y ih generalizing x
[GOAL]
case h
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
x : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y
[PROOFSTEP]
cases x with
| zero => exact iff_of_true hy.bot_lt (zero_le _)
| succ x =>
  rw [log]; split_ifs with h
  · have b_pos : 0 < b := zero_le_one.trans_lt hb
    rw [succ_eq_add_one, add_le_add_iff_right, ← ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne',
      le_div_iff_mul_le b_pos, pow_succ', mul_comm]
  · exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩) (not_succ_le_zero _)
[GOAL]
case h
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
x : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y
[PROOFSTEP]
cases x with
| zero => exact iff_of_true hy.bot_lt (zero_le _)
| succ x =>
  rw [log]; split_ifs with h
  · have b_pos : 0 < b := zero_le_one.trans_lt hb
    rw [succ_eq_add_one, add_le_add_iff_right, ← ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne',
      le_div_iff_mul_le b_pos, pow_succ', mul_comm]
  · exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩) (not_succ_le_zero _)
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
x y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
⊢ b ^ zero ≤ y ↔ zero ≤ log b y
[PROOFSTEP]

| zero => exact iff_of_true hy.bot_lt (zero_le _)
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
x y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
⊢ b ^ zero ≤ y ↔ zero ≤ log b y
[PROOFSTEP]
exact iff_of_true hy.bot_lt (zero_le _)
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔ succ x ≤ log b y
[PROOFSTEP]

| succ x =>
  rw [log]; split_ifs with h
  · have b_pos : 0 < b := zero_le_one.trans_lt hb
    rw [succ_eq_add_one, add_le_add_iff_right, ← ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne',
      le_div_iff_mul_le b_pos, pow_succ', mul_comm]
  · exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩) (not_succ_le_zero _)
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔ succ x ≤ log b y
[PROOFSTEP]
rw [log]
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      if h : b ≤ y ∧ 1 < b then
        let_fun this := (_ : y / b < y);
        log b (y / b) + 1
      else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      let_fun this := (_ : y / b < y);
      log b (y / b) + 1
[PROOFSTEP]
have b_pos : 0 < b := zero_le_one.trans_lt hb
[GOAL]
case pos
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
b_pos : 0 < b
⊢ b ^ succ x ≤ y ↔
    succ x ≤
      let_fun this := (_ : y / b < y);
      log b (y / b) + 1
[PROOFSTEP]
rw [succ_eq_add_one, add_le_add_iff_right, ← ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne',
  le_div_iff_mul_le b_pos, pow_succ', mul_comm]
[GOAL]
case neg
b : ℕ
hb : 1 < b
x✝ y✝ : ℕ
hy✝ : y✝ ≠ 0
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : ¬(b ≤ y ∧ 1 < b)
⊢ b ^ succ x ≤ y ↔ succ x ≤ 0
[PROOFSTEP]
exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩) (not_succ_le_zero _)
[GOAL]
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ^ x ≤ y
[PROOFSTEP]
refine' (le_or_lt b 1).elim (fun hb => _) fun hb => (pow_le_iff_le_log hb hy).2 h
[GOAL]
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
⊢ b ^ x ≤ y
[PROOFSTEP]
rw [log_of_left_le_one hb, nonpos_iff_eq_zero] at h 
[GOAL]
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ x ≤ y
[PROOFSTEP]
rwa [h, pow_zero, one_le_iff_ne_zero]
[GOAL]
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
⊢ x ≤ log b y
[PROOFSTEP]
rcases ne_or_eq y 0 with (hy | rfl)
[GOAL]
case inl
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y
case inr b x : ℕ hb : 1 < b h : b ^ x ≤ 0 ⊢ x ≤ log b 0
[PROOFSTEP]
exacts [(pow_le_iff_le_log hb hy).1 h, (h.not_lt (pow_pos (zero_lt_one.trans hb) _)).elim]
[GOAL]
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
[GOAL]
case inl.intro
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
rw [le_antisymm_iff, ← lt_succ_iff, ← pow_le_iff_le_log, ← lt_pow_iff_log_lt, and_comm]
[GOAL]
case inl.intro.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
have hm : m ≠ 0 := h.resolve_right hbn
[GOAL]
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
rw [not_and_or, not_lt, Ne.def, not_not] at hbn 
[GOAL]
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ n = 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
rcases hbn with (hb | rfl)
[GOAL]
case inr.inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
[PROOFSTEP]
simpa only [log_of_left_le_one hb, hm.symm, false_iff_iff, not_and, not_lt] using
  le_trans (pow_le_pow_of_le_one' hb m.le_succ)
[GOAL]
case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)
[PROOFSTEP]
simpa only [log_zero_right, hm.symm, nonpos_iff_eq_zero, false_iff, not_and, not_lt, add_pos_iff, or_true,
  pow_eq_zero_iff] using pow_eq_zero
[GOAL]
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
⊢ log b n = m
[PROOFSTEP]
rcases eq_or_ne m 0 with (rfl | hm)
[GOAL]
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b ^ (0 + 1)
⊢ log b n = 0
[PROOFSTEP]
rw [pow_one] at h₂ 
[GOAL]
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b
⊢ log b n = 0
[PROOFSTEP]
exact log_of_lt h₂
[GOAL]
case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m
[PROOFSTEP]
exact (log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩
[GOAL]
b n : ℕ
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b
[PROOFSTEP]
rw [log_eq_iff (Or.inl one_ne_zero), pow_add, pow_one]
[GOAL]
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n * b) = log b n + 1
[PROOFSTEP]
apply log_eq_of_pow_le_of_lt_pow
[GOAL]
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ (log b n + 1) ≤ n * b
[PROOFSTEP]
rw [pow_succ', mul_comm b]
[GOAL]
case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1 + 1)
[PROOFSTEP]
rw [pow_succ', mul_comm b]
[GOAL]
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b
case h₂ b n : ℕ hb : 1 < b hn : n ≠ 0 ⊢ n * b < b ^ (log b n + 1) * b
[PROOFSTEP]
exacts [mul_le_mul_right' (pow_log_le_self _ hn) _,
  (mul_lt_mul_right (zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]
[GOAL]
b : ℕ
⊢ b ^ log b 0 ≤ 0 + 1
[PROOFSTEP]
rw [log_zero_right, pow_zero]
[GOAL]
b : ℕ
⊢ Monotone (log b)
[PROOFSTEP]
refine' monotone_nat_of_le_succ fun n => _
[GOAL]
b n : ℕ
⊢ log b n ≤ log b (n + 1)
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)
[PROOFSTEP]
rw [log_of_left_le_one hb]
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)
[PROOFSTEP]
exact le_log_of_pow_le hb (pow_log_le_add_one _ _)
[GOAL]
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0
[PROOFSTEP]
rw [log_zero_right, log_zero_right]
[GOAL]
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n
[PROOFSTEP]
apply le_log_of_pow_le hc
[GOAL]
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n
[PROOFSTEP]
calc
  c ^ log b n ≤ b ^ log b n := pow_le_pow_of_le_left' hb _
  _ ≤ n := pow_log_le_self _ hn
[GOAL]
b n : ℕ
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
cases' lt_or_le n b with h h
[GOAL]
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
[GOAL]
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1
[PROOFSTEP]
rw [log_of_one_lt_of_le hb h, add_tsub_cancel_right]
[GOAL]
b n : ℕ
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
rw [log_of_left_le_one hb, log_of_left_le_one hb]
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
cases' lt_or_le n b with h h
[GOAL]
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
rw [div_eq_of_lt h, zero_mul, log_zero_right, log_of_lt h]
[GOAL]
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n
[PROOFSTEP]
rw [log_mul_base hb (Nat.div_pos h (zero_le_one.trans_lt hb)).ne', log_div_base,
  tsub_add_cancel_of_le (succ_le_iff.2 <| log_pos hb h)]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1) / b < n
[PROOFSTEP]
rw [div_lt_iff_lt_mul (zero_lt_one.trans hb), ← succ_le_iff, ← pred_eq_sub_one,
  succ_pred_eq_of_pos (add_pos (zero_lt_one.trans hn) (zero_lt_one.trans hb))]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b
[PROOFSTEP]
exact add_le_mul hn hb
[GOAL]
b : ℕ
hb : b ≤ 1
n : ℕ
⊢ clog b n = 0
[PROOFSTEP]
rw [clog, dif_neg fun h : 1 < b ∧ 1 < n => h.1.not_le hb]
[GOAL]
n : ℕ
hn : n ≤ 1
b : ℕ
⊢ clog b n = 0
[PROOFSTEP]
rw [clog, dif_neg fun h : 1 < b ∧ 1 < n => h.2.not_le hn]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ clog b n = clog b ((n + b - 1) / b) + 1
[PROOFSTEP]
rw [clog, dif_pos (⟨hb, hn⟩ : 1 < b ∧ 1 < n)]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b n
[PROOFSTEP]
rw [clog_of_two_le hb hn]
[GOAL]
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b ((n + b - 1) / b) + 1
[PROOFSTEP]
exact zero_lt_succ _
[GOAL]
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ clog b n = 1
[PROOFSTEP]
rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]
[GOAL]
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1
[PROOFSTEP]
have n_pos : 0 < n := (zero_lt_two' ℕ).trans_le hn
[GOAL]
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
n_pos : 0 < n
⊢ (n + b - 1) / b ≤ 1
[PROOFSTEP]
rw [← lt_succ_iff, Nat.div_lt_iff_lt_mul (n_pos.trans_le h), ← succ_le_iff, ← pred_eq_sub_one,
  succ_pred_eq_of_pos (add_pos n_pos (n_pos.trans_le h)), succ_mul, one_mul]
[GOAL]
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
n_pos : 0 < n
⊢ n + b ≤ b + b
[PROOFSTEP]
exact add_le_add_right h _
[GOAL]
b : ℕ
hb : 1 < b
x y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y
[PROOFSTEP]
induction' x using Nat.strong_induction_on with x ih generalizing y
[GOAL]
case h
b : ℕ
hb : 1 < b
y✝ x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
y : ℕ
⊢ x ≤ b ^ y ↔ clog b x ≤ y
[PROOFSTEP]
cases y
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ b ^ zero ↔ clog b x ≤ zero
[PROOFSTEP]
rw [pow_zero]
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ x ≤ 1 ↔ clog b x ≤ zero
[PROOFSTEP]
refine' ⟨fun h => (clog_of_right_le_one h b).le, _⟩
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ clog b x ≤ zero → x ≤ 1
[PROOFSTEP]
simp_rw [← not_lt]
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ ¬zero < clog b x → ¬1 < x
[PROOFSTEP]
contrapose!
[GOAL]
case h.zero
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
⊢ 1 < x → zero < clog b x
[PROOFSTEP]
exact clog_pos hb
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
⊢ x ≤ b ^ succ n✝ ↔ clog b x ≤ succ n✝
[PROOFSTEP]
have b_pos : 0 < b := (zero_lt_one' ℕ).trans hb
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ succ n✝ ↔ clog b x ≤ succ n✝
[PROOFSTEP]
rw [clog]
[GOAL]
case h.succ
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
⊢ x ≤ b ^ succ n✝ ↔
    (if h : 1 < b ∧ 1 < x then
        let_fun this := (_ : (x + b - 1) / b < x);
        clog b ((x + b - 1) / b) + 1
      else 0) ≤
      succ n✝
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
h : 1 < b ∧ 1 < x
⊢ x ≤ b ^ succ n✝ ↔
    (let_fun this := (_ : (x + b - 1) / b < x);
      clog b ((x + b - 1) / b) + 1) ≤
      succ n✝
[PROOFSTEP]
rw [succ_eq_add_one, add_le_add_iff_right, ← ih ((x + b - 1) / b) (add_pred_div_lt hb h.2),
  Nat.div_le_iff_le_mul_add_pred b_pos, mul_comm b, ← pow_succ, add_tsub_assoc_of_le (Nat.succ_le_of_lt b_pos),
  add_le_add_iff_right]
[GOAL]
case neg
b : ℕ
hb : 1 < b
y x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y
n✝ : ℕ
b_pos : 0 < b
h : ¬(1 < b ∧ 1 < x)
⊢ x ≤ b ^ succ n✝ ↔ 0 ≤ succ n✝
[PROOFSTEP]
exact iff_of_true ((not_lt.1 (not_and.1 h hb)).trans <| succ_le_of_lt <| pow_pos b_pos _) (zero_le _)
[GOAL]
b x : ℕ
hb : 1 < b
z : ℕ
⊢ clog b (b ^ x) ≤ z ↔ x ≤ z
[PROOFSTEP]
rw [← le_pow_iff_clog_le hb]
[GOAL]
b x : ℕ
hb : 1 < b
z : ℕ
⊢ b ^ x ≤ b ^ z ↔ x ≤ z
[PROOFSTEP]
exact (pow_right_strictMono hb).le_iff_le
[GOAL]
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ pred (clog b x) < x
[PROOFSTEP]
rw [← not_le, le_pow_iff_clog_le hb, not_le]
[GOAL]
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ pred (clog b x) < clog b x
[PROOFSTEP]
exact pred_lt (clog_pos hb hx).ne'
[GOAL]
b n m : ℕ
h : n ≤ m
⊢ clog b n ≤ clog b m
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m
[PROOFSTEP]
rw [clog_of_left_le_one hb]
[GOAL]
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m
[PROOFSTEP]
rw [← le_pow_iff_clog_le hb]
[GOAL]
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ n ≤ b ^ clog b m
[PROOFSTEP]
exact h.trans (le_pow_clog hb _)
[GOAL]
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ clog b n ≤ clog c n
[PROOFSTEP]
rw [← le_pow_iff_clog_le (lt_of_lt_of_le hc hb)]
[GOAL]
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n
[PROOFSTEP]
calc
  n ≤ c ^ clog c n := le_pow_clog hc _
  _ ≤ b ^ clog c n := pow_le_pow_of_le_left hb _
[GOAL]
b n : ℕ
⊢ log b n ≤ clog b n
[PROOFSTEP]
obtain hb | hb := le_or_lt b 1
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n
[PROOFSTEP]
rw [log_of_left_le_one hb]
[GOAL]
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
[PROOFSTEP]
cases n with
| zero =>
  rw [log_zero_right]
  exact zero_le _
| succ n => exact (pow_right_strictMono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
[GOAL]
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
[PROOFSTEP]
cases n with
| zero =>
  rw [log_zero_right]
  exact zero_le _
| succ n => exact (pow_right_strictMono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
[GOAL]
case inr.zero
b : ℕ
hb : 1 < b
⊢ log b zero ≤ clog b zero
[PROOFSTEP]

| zero =>
  rw [log_zero_right]
  exact zero_le _
[GOAL]
case inr.zero
b : ℕ
hb : 1 < b
⊢ log b zero ≤ clog b zero
[PROOFSTEP]
rw [log_zero_right]
[GOAL]
case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b zero
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr.succ
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (succ n) ≤ clog b (succ n)
[PROOFSTEP]

| succ n => exact (pow_right_strictMono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
[GOAL]
case inr.succ
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (succ n) ≤ clog b (succ n)
[PROOFSTEP]
exact (pow_right_strictMono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
