case intro.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ ↑n) = ↑n

case intro.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ log b (↑b ^ z) = z
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ 1 ≤ ↑b
case intro.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ ↑n) = ↑n
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]
no goals
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ 1 ≤ ↑b
exact_mod_cast hb.le
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ 1 ≤ ↑b
case intro.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n
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]
no goals
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ 1 ≤ ↑b
exact_mod_cast hb.le