[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)
[PROOFSTEP]
obtain rfl | hr := hr.eq_or_lt
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ log b 1 = -↑(Nat.clog b ⌈1⁻¹⌉₊)
[PROOFSTEP]
rw [log, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right, Nat.clog_one_right, Int.ofNat_zero,
  neg_zero]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)
[PROOFSTEP]
exact if_neg hr.not_le
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ log b ↑n = ↑(Nat.log b n)
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b ↑Nat.zero = ↑(Nat.log b Nat.zero)
[PROOFSTEP]
simp [log_of_right_le_one]
[GOAL]
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(Nat.succ n✝) = ↑(Nat.log b (Nat.succ n✝))
[PROOFSTEP]
rw [log_of_one_le_right, Nat.floor_coe]
[GOAL]
case succ.hr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(Nat.succ n✝)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ log b r = 0
[PROOFSTEP]
cases' le_total 1 r with h h
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ log b r = 0
[PROOFSTEP]
rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, Int.ofNat_zero]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ log b r = 0
[PROOFSTEP]
rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, Int.ofNat_zero, neg_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ log b r = 0
[PROOFSTEP]
rw [log_of_right_le_one _ (hr.trans zero_le_one),
  Nat.clog_of_right_le_one ((Nat.ceil_eq_zero.mpr <| inv_nonpos.2 hr).trans_le zero_le_one), Int.ofNat_zero, neg_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ log b r ≤ r
[PROOFSTEP]
cases' le_total 1 r with hr1 hr1
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ log b r ≤ r
[PROOFSTEP]
rw [log_of_one_le_right _ hr1]
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ ↑(Nat.log b ⌊r⌋₊) ≤ r
[PROOFSTEP]
rw [zpow_ofNat, ← Nat.cast_pow, ← Nat.le_floor_iff hr.le]
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊
[PROOFSTEP]
exact Nat.pow_log_le_self b (Nat.floor_pos.mpr hr1).ne'
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ ↑b ^ log b r ≤ r
[PROOFSTEP]
rw [log_of_right_le_one _ hr1, zpow_neg, zpow_ofNat, ← Nat.cast_pow]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ (↑(b ^ Nat.clog b ⌈r⁻¹⌉₊))⁻¹ ≤ r
[PROOFSTEP]
exact inv_le_of_inv_le hr (Nat.ceil_le.1 <| Nat.le_pow_clog hb _)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
cases' le_or_lt r 0 with hr hr
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
rw [log_of_right_le_zero _ hr, zero_add, zpow_one]
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b
[PROOFSTEP]
exact hr.trans_lt (zero_lt_one.trans_le <| by exact_mod_cast hb.le)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ 1 ≤ ↑b
[PROOFSTEP]
exact_mod_cast hb.le
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
cases' le_or_lt 1 r with hr1 hr1
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
rw [log_of_one_le_right _ hr1]
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ (↑(Nat.log b ⌊r⌋₊) + 1)
[PROOFSTEP]
rw [Int.ofNat_add_one_out, zpow_ofNat, ← Nat.cast_pow]
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑(b ^ Nat.succ (Nat.log b ⌊r⌋₊))
[PROOFSTEP]
apply Nat.lt_of_floor_lt
[GOAL]
case inr.inl.h
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ ⌊r⌋₊ < b ^ Nat.succ (Nat.log b ⌊r⌋₊)
[PROOFSTEP]
exact Nat.lt_pow_succ_log_self hb _
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
rw [log_of_right_le_one _ hr1.le]
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
[PROOFSTEP]
have hcri : 1 < r⁻¹ := one_lt_inv hr hr1
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
[PROOFSTEP]
have : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊ :=
  Nat.succ_le_of_lt (Nat.clog_pos hb <| Nat.one_lt_cast.1 <| hcri.trans_le (Nat.le_ceil _))
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
[PROOFSTEP]
rw [neg_add_eq_sub, ← neg_sub, ← Int.ofNat_one, ← Int.ofNat_sub this, zpow_neg, zpow_ofNat,
  lt_inv hr (pow_pos (Nat.cast_pos.mpr <| zero_lt_one.trans hb) _), ← Nat.cast_pow]
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ ↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) < r⁻¹
[PROOFSTEP]
refine' Nat.lt_ceil.1 _
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1) < ⌈r⁻¹⌉₊
[PROOFSTEP]
exact Nat.pow_pred_clog_lt_self hb <| Nat.one_lt_cast.1 <| hcri.trans_le <| Nat.le_ceil _
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b 1 = 0
[PROOFSTEP]
rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ log b (↑b ^ z) = z
[PROOFSTEP]
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
[GOAL]
case intro.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ ↑n) = ↑n
[PROOFSTEP]
rw [log_of_one_le_right _ (one_le_zpow_of_nonneg _ <| Int.coe_nat_nonneg _), zpow_ofNat, ← Nat.cast_pow, Nat.floor_coe,
  Nat.log_pow hb]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ 1 ≤ ↑b
[PROOFSTEP]
exact_mod_cast hb.le
[GOAL]
case intro.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n
[PROOFSTEP]
rw [log_of_right_le_one _ (zpow_le_one_of_nonpos _ <| neg_nonpos.mpr (Int.coe_nat_nonneg _)), zpow_neg, inv_inv,
  zpow_ofNat, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ 1 ≤ ↑b
[PROOFSTEP]
exact_mod_cast hb.le
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : b ≤ 1
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
rw [log_of_left_le_one hb, log_of_left_le_one hb]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
cases' le_total r₁ 1 with h₁ h₁
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
cases' le_total r₂ 1 with h₂ h₂
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : 1 ≤ r₁
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
cases' le_total r₂ 1 with h₂ h₂
[GOAL]
case inr.inl.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Int.ofNat_le]
[GOAL]
case inr.inl.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊
[PROOFSTEP]
exact Nat.clog_mono_right _ (Nat.ceil_mono <| inv_le_inv_of_le h₀ h)
[GOAL]
case inr.inl.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
rw [log_of_right_le_one _ h₁, log_of_one_le_right _ h₂]
[GOAL]
case inr.inl.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ ↑(Nat.log b ⌊r₂⌋₊)
[PROOFSTEP]
exact (neg_nonpos.mpr (Int.coe_nat_nonneg _)).trans (Int.coe_nat_nonneg _)
[GOAL]
case inr.inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : 1 ≤ r₁
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
obtain rfl := le_antisymm h (h₂.trans h₁)
[GOAL]
case inr.inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ : R
h₀ : 0 < r₁
hb : 1 < b
h₁ : 1 ≤ r₁
h : r₁ ≤ r₁
h₂ : r₁ ≤ 1
⊢ log b r₁ ≤ log b r₁
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂, Int.ofNat_le]
[GOAL]
case inr.inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊
[PROOFSTEP]
exact Nat.log_mono_right (Nat.floor_mono h)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ 0 < ↑b
[PROOFSTEP]
exact_mod_cast zero_lt_one.trans hb
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z₁ z₂ : ℤ
hz : z₁ ≤ z₂
⊢ 1 < ↑b
[PROOFSTEP]
exact_mod_cast hb
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 1
⊢ clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)
[PROOFSTEP]
obtain rfl | hr := hr.eq_or_lt
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ clog b 1 = -↑(Nat.log b ⌊1⁻¹⌋₊)
[PROOFSTEP]
rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right, Nat.clog_one_right, Int.ofNat_zero,
  neg_zero]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)
[PROOFSTEP]
exact if_neg hr.not_le
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ clog b r = 0
[PROOFSTEP]
rw [clog, if_neg (hr.trans_lt zero_lt_one).not_le, neg_eq_zero, Int.coe_nat_eq_zero, Nat.log_eq_zero_iff]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
[PROOFSTEP]
exact Or.inr hb
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
[PROOFSTEP]
refine' Or.inl (lt_of_le_of_lt _ hb)
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1
[PROOFSTEP]
exact Nat.floor_le_one_of_le_one ((inv_nonpos.2 hr).trans zero_le_one)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
cases' lt_or_le 0 r with hrp hrp
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
obtain hr | hr := le_total 1 r
[GOAL]
case inl.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
rw [clog_of_right_le_one _ (inv_le_one hr), log_of_one_le_right _ hr, inv_inv]
[GOAL]
case inl.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
rw [clog_of_one_le_right _ (one_le_inv hrp hr), log_of_right_le_one _ hr, neg_neg]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, neg_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ log b r⁻¹ = -clog b r
[PROOFSTEP]
rw [← inv_inv r, clog_inv, neg_neg, inv_inv]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ -log b r⁻¹ = clog b r
[PROOFSTEP]
rw [log_inv, neg_neg]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ -clog b r⁻¹ = log b r
[PROOFSTEP]
rw [clog_inv, neg_neg]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑n = ↑(Nat.clog b n)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b ↑Nat.zero = ↑(Nat.clog b Nat.zero)
[PROOFSTEP]
simp [clog_of_right_le_one]
[GOAL]
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑(Nat.succ n) = ↑(Nat.clog b (Nat.succ n))
[PROOFSTEP]
rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr]
[GOAL]
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ ↑(Nat.succ n - 1) < ↑(Nat.succ n) ∧ ↑(Nat.succ n) ≤ ↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
case succ.hr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ 1 ≤ ↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ clog b r = 0
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, neg_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
⊢ r ≤ ↑b ^ clog b r
[PROOFSTEP]
cases' le_or_lt r 0 with hr hr
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ ↑b ^ clog b r
[PROOFSTEP]
rw [clog_of_right_le_zero _ hr, zpow_zero]
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ 1
[PROOFSTEP]
exact hr.trans zero_le_one
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r ≤ ↑b ^ clog b r
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, zpow_neg, le_inv hr (zpow_pos_of_pos _ _)]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ ↑b ^ log b r⁻¹ ≤ r⁻¹
[PROOFSTEP]
exact zpow_log_le_self hb (inv_pos.mpr hr)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ 0 < ↑b
[PROOFSTEP]
exact Nat.cast_pos.mpr (zero_le_one.trans_lt hb)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ (clog b r - 1) < r
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt _ hr]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ r⁻¹ < ↑b ^ (log b r⁻¹ + 1)
[PROOFSTEP]
exact lt_zpow_succ_log_self hb _
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)
[PROOFSTEP]
exact zpow_pos_of_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b 1 = 0
[PROOFSTEP]
rw [clog_of_one_le_right _ le_rfl, Nat.ceil_one, Nat.clog_one_right, Int.ofNat_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ clog b (↑b ^ z) = z
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ clog b r₁ ≤ clog b r₂
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, ← neg_log_inv_eq_clog, neg_le_neg_iff]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹
[PROOFSTEP]
exact log_mono_right (inv_pos.mpr <| h₀.trans_le h) (inv_le_inv_of_le h₀ h)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ 0 < ↑b
[PROOFSTEP]
exact_mod_cast zero_lt_one.trans hb
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z₁ z₂ : ℤ
hz : z₁ ≤ z₂
⊢ 1 < ↑b
[PROOFSTEP]
exact_mod_cast hb
