[GOAL]
b x y : ℝ
⊢ logb b 0 = 0
[PROOFSTEP]
simp [logb]
[GOAL]
b x y : ℝ
⊢ logb b 1 = 0
[PROOFSTEP]
simp [logb]
[GOAL]
b x✝ y x : ℝ
⊢ logb b |x| = logb b x
[PROOFSTEP]
rw [logb, logb, log_abs]
[GOAL]
b x✝ y x : ℝ
⊢ logb b (-x) = logb b x
[PROOFSTEP]
rw [← logb_abs x, ← logb_abs (-x), abs_neg]
[GOAL]
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x * y) = logb b x + logb b y
[PROOFSTEP]
simp_rw [logb, log_mul hx hy, add_div]
[GOAL]
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x / y) = logb b x - logb b y
[PROOFSTEP]
simp_rw [logb, log_div hx hy, sub_div]
[GOAL]
b x✝ y x : ℝ
⊢ logb b x⁻¹ = -logb b x
[PROOFSTEP]
simp [logb, neg_div]
[GOAL]
b✝ x y a b : ℝ
⊢ (logb a b)⁻¹ = logb b a
[PROOFSTEP]
simp_rw [logb, inv_div]
[GOAL]
b✝ x y a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹
[PROOFSTEP]
simp_rw [inv_logb]
[GOAL]
b✝ x y a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a * b) = logb c a + logb c b
[PROOFSTEP]
exact logb_mul h₁ h₂
[GOAL]
b✝ x y a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹
[PROOFSTEP]
simp_rw [inv_logb]
[GOAL]
b✝ x y a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a / b) = logb c a - logb c b
[PROOFSTEP]
exact logb_div h₁ h₂
[GOAL]
b✝ x y a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹
[PROOFSTEP]
rw [← inv_logb_mul_base h₁ h₂ c, inv_inv]
[GOAL]
b✝ x y a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹
[PROOFSTEP]
rw [← inv_logb_div_base h₁ h₂ c, inv_inv]
[GOAL]
b✝ x y a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ logb a b * logb b c = logb a c
[PROOFSTEP]
unfold logb
[GOAL]
b✝ x y a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ log b / log a * (log c / log b) = log c / log a
[PROOFSTEP]
rw [mul_comm, div_mul_div_cancel _ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0
[PROOFSTEP]
have b_ne_zero : b ≠ 0
[GOAL]
case b_ne_zero
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ b ≠ 0
b x y : ℝ b_pos : 0 < b b_ne_one : b ≠ 1 b_ne_zero : b ≠ 0 ⊢ log b ≠ 0
[PROOFSTEP]
linarith
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ log b ≠ 0
[PROOFSTEP]
have b_ne_minus_one : b ≠ -1
[GOAL]
case b_ne_minus_one
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ b ≠ -1
b x y : ℝ b_pos : 0 < b b_ne_one : b ≠ 1 b_ne_zero : b ≠ 0 b_ne_minus_one : b ≠ -1 ⊢ log b ≠ 0
[PROOFSTEP]
linarith
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
b_ne_minus_one : b ≠ -1
⊢ log b ≠ 0
[PROOFSTEP]
simp [b_ne_one, b_ne_zero, b_ne_minus_one]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ logb b (b ^ x) = x
[PROOFSTEP]
rw [logb, div_eq_iff, log_rpow b_pos]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0
[PROOFSTEP]
exact log_b_ne_zero b_pos b_ne_one
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x = |x|
[PROOFSTEP]
apply log_injOn_pos
[GOAL]
case a
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x ∈ Ioi 0
case a
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ |x| ∈ Ioi 0
case a b x y : ℝ b_pos : 0 < b b_ne_one : b ≠ 1 hx : x ≠ 0 ⊢ log (b ^ logb b x) = log |x|
[PROOFSTEP]
simp only [Set.mem_Ioi]
[GOAL]
case a
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ 0 < b ^ logb b x
case a
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ |x| ∈ Ioi 0
case a b x y : ℝ b_pos : 0 < b b_ne_one : b ≠ 1 hx : x ≠ 0 ⊢ log (b ^ logb b x) = log |x|
[PROOFSTEP]
apply rpow_pos_of_pos b_pos
[GOAL]
case a
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ |x| ∈ Ioi 0
case a b x y : ℝ b_pos : 0 < b b_ne_one : b ≠ 1 hx : x ≠ 0 ⊢ log (b ^ logb b x) = log |x|
[PROOFSTEP]
simp only [abs_pos, mem_Ioi, Ne.def, hx, not_false_iff]
[GOAL]
case a
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|
[PROOFSTEP]
rw [log_rpow b_pos, logb, log_abs]
[GOAL]
case a
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log x / log b * log b = log x
[PROOFSTEP]
field_simp [log_b_ne_zero b_pos b_ne_one]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ b ^ logb b x = x
[PROOFSTEP]
rw [rpow_logb_eq_abs b_pos b_ne_one hx.ne']
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ |x| = x
[PROOFSTEP]
exact abs_of_pos hx
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ b ^ logb b x = -x
[PROOFSTEP]
rw [rpow_logb_eq_abs b_pos b_ne_one (ne_of_lt hx)]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ |x| = -x
[PROOFSTEP]
exact abs_of_neg hx
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ SurjOn (logb b) (Iio 0) univ
[PROOFSTEP]
intro x _
[GOAL]
b x✝ y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ x ∈ logb b '' Iio 0
[PROOFSTEP]
use-b ^ x
[GOAL]
case h
b x✝ y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ -b ^ x ∈ Iio 0 ∧ logb b (-b ^ x) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
b x✝ y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ -b ^ x ∈ Iio 0
[PROOFSTEP]
simp only [Right.neg_neg_iff, Set.mem_Iio]
[GOAL]
case h.left
b x✝ y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ 0 < b ^ x
[PROOFSTEP]
apply rpow_pos_of_pos b_pos
[GOAL]
case h.right
b x✝ y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ logb b (-b ^ x) = x
[PROOFSTEP]
rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]
[GOAL]
b x y : ℝ
hb : 1 < b
⊢ 0 < b
[PROOFSTEP]
linarith
  -- Porting note: prime added to avoid clashing with `b_ne_one` further down the file
[GOAL]
b x y : ℝ
hb : 1 < b
⊢ b ≠ 1
[PROOFSTEP]
linarith
[GOAL]
b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ x ≤ y
[PROOFSTEP]
rw [logb, logb, div_le_div_right (log_pos hb), log_le_log h h₁]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ logb b x < logb b y
[PROOFSTEP]
rw [logb, logb, div_lt_div_right (log_pos hb)]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y
[PROOFSTEP]
exact log_lt_log hx hxy
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ logb b x < logb b y ↔ x < y
[PROOFSTEP]
rw [logb, logb, div_lt_div_right (log_pos hb)]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y
[PROOFSTEP]
exact log_lt_log_iff hx hy
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x ≤ y ↔ x ≤ b ^ y
[PROOFSTEP]
rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x < y ↔ x < b ^ y
[PROOFSTEP]
rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]
[GOAL]
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ x ≤ logb b y ↔ b ^ x ≤ y
[PROOFSTEP]
rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]
[GOAL]
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ x < logb b y ↔ b ^ x < y
[PROOFSTEP]
rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 < logb b x ↔ 1 < x
[PROOFSTEP]
rw [← @logb_one b]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x
[PROOFSTEP]
rw [logb_lt_logb_iff hb zero_lt_one hx]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 1 < x
⊢ 0 < logb b x
[PROOFSTEP]
rw [logb_pos_iff hb (lt_trans zero_lt_one hx)]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 1 < x
⊢ 1 < x
[PROOFSTEP]
exact hx
[GOAL]
b x y : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < 0 ↔ x < 1
[PROOFSTEP]
rw [← logb_one]
[GOAL]
b x y : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < logb ?m.14910 1 ↔ x < 1
b x y : ℝ hb : 1 < b h : 0 < x ⊢ ℝ
[PROOFSTEP]
exact logb_lt_logb_iff hb h zero_lt_one
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 ≤ logb b x ↔ 1 ≤ x
[PROOFSTEP]
rw [← not_lt, logb_neg_iff hb hx, not_lt]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
rw [← not_lt, logb_pos_iff hb hx, not_lt]
[GOAL]
b x y : ℝ
hb : 1 < b
hx : 0 ≤ x
⊢ logb b x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
rcases hx.eq_or_lt with (rfl | hx)
[GOAL]
case inl
b y : ℝ
hb : 1 < b
hx : 0 ≤ 0
⊢ logb b 0 ≤ 0 ↔ 0 ≤ 1
[PROOFSTEP]
simp [le_refl, zero_le_one]
[GOAL]
case inr
b x y : ℝ
hb : 1 < b
hx✝ : 0 ≤ x
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
exact logb_nonpos_iff hb hx
[GOAL]
b x y : ℝ
hb : 1 < b
⊢ StrictAntiOn (logb b) (Iio 0)
[PROOFSTEP]
rintro x (hx : x < 0) y (hy : y < 0) hxy
[GOAL]
b x✝ y✝ : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b y < logb b x
[PROOFSTEP]
rw [← logb_abs y, ← logb_abs x]
[GOAL]
b x✝ y✝ : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |y| < logb b |x|
[PROOFSTEP]
refine' logb_lt_logb hb (abs_pos.2 hy.ne) _
[GOAL]
b x✝ y✝ : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|
[PROOFSTEP]
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ b ≠ 1
[PROOFSTEP]
linarith
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ y ≤ x
[PROOFSTEP]
rw [logb, logb, div_le_div_right_of_neg (log_neg b_pos b_lt_one), log_le_log h₁ h]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ logb b y < logb b x
[PROOFSTEP]
rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ log x < log y
[PROOFSTEP]
exact log_lt_log hx hxy
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ logb b x < logb b y ↔ y < x
[PROOFSTEP]
rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ log y < log x ↔ y < x
[PROOFSTEP]
exact log_lt_log_iff hy hx
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ y ↔ b ^ y ≤ x
[PROOFSTEP]
rw [← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hx]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x < y ↔ b ^ y < x
[PROOFSTEP]
rw [← rpow_lt_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hx]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x ≤ logb b y ↔ y ≤ b ^ x
[PROOFSTEP]
rw [← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hy]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x < logb b y ↔ y < b ^ x
[PROOFSTEP]
rw [← rpow_lt_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hy]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 < logb b x ↔ x < 1
[PROOFSTEP]
rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one zero_lt_one hx]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ 0 < logb b x
[PROOFSTEP]
rw [logb_pos_iff_of_base_lt_one b_pos b_lt_one hx]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ x < 1
[PROOFSTEP]
exact hx'
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
⊢ logb b x < 0 ↔ 1 < x
[PROOFSTEP]
rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one h zero_lt_one]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 ≤ logb b x ↔ x ≤ 1
[PROOFSTEP]
rw [← not_lt, logb_neg_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ 0 ≤ logb b x
[PROOFSTEP]
rw [logb_nonneg_iff_of_base_lt_one b_pos b_lt_one hx]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ x ≤ 1
[PROOFSTEP]
exact hx'
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ 0 ↔ 1 ≤ x
[PROOFSTEP]
rw [← not_lt, logb_pos_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ StrictMonoOn (logb b) (Iio 0)
[PROOFSTEP]
rintro x (hx : x < 0) y (hy : y < 0) hxy
[GOAL]
b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b y
[PROOFSTEP]
rw [← logb_abs y, ← logb_abs x]
[GOAL]
b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |x| < logb b |y|
[PROOFSTEP]
refine' logb_lt_logb_of_base_lt_one b_pos b_lt_one (abs_pos.2 hy.ne) _
[GOAL]
b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|
[PROOFSTEP]
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ Tendsto (logb b) atTop atBot
[PROOFSTEP]
rw [tendsto_atTop_atBot]
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ ∀ (b_1 : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ b_1
[PROOFSTEP]
intro e
[GOAL]
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ e
[PROOFSTEP]
use 1 ⊔ b ^ e
[GOAL]
case h
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∀ (a : ℝ), 1 ⊔ b ^ e ≤ a → logb b a ≤ e
[PROOFSTEP]
intro a
[GOAL]
case h
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ 1 ⊔ b ^ e ≤ a → logb b a ≤ e
[PROOFSTEP]
simp only [and_imp, sup_le_iff]
[GOAL]
case h
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ 1 ≤ a → b ^ e ≤ a → logb b a ≤ e
[PROOFSTEP]
intro ha
[GOAL]
case h
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → logb b a ≤ e
[PROOFSTEP]
rw [logb_le_iff_le_rpow_of_base_lt_one b_pos b_lt_one]
[GOAL]
case h
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → b ^ e ≤ a
case h b x y : ℝ b_pos : 0 < b b_lt_one : b < 1 e a : ℝ ha : 1 ≤ a ⊢ 0 < a
[PROOFSTEP]
tauto
[GOAL]
case h
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ 0 < a
[PROOFSTEP]
exact lt_of_lt_of_le zero_lt_one ha
[GOAL]
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr : 0 ≤ r
⊢ ⌊logb (↑b) r⌋ = Int.log b r
[PROOFSTEP]
obtain rfl | hr := hr.eq_or_lt
[GOAL]
case inl
b✝ x y : ℝ
b : ℕ
hb : 1 < b
hr : 0 ≤ 0
⊢ ⌊logb (↑b) 0⌋ = Int.log b 0
[PROOFSTEP]
rw [logb_zero, Int.log_zero_right, Int.floor_zero]
[GOAL]
case inr
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
⊢ ⌊logb (↑b) r⌋ = Int.log b r
[PROOFSTEP]
have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
[GOAL]
case inr
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ ⌊logb (↑b) r⌋ = Int.log b r
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ ⌊logb (↑b) r⌋ ≤ Int.log b r
[PROOFSTEP]
rw [← Int.zpow_le_iff_le_log hb hr, ← rpow_int_cast b]
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ ↑b ^ ↑⌊logb (↑b) r⌋ ≤ r
[PROOFSTEP]
refine' le_of_le_of_eq _ (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr)
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ ↑b ^ ↑⌊logb (↑b) r⌋ ≤ ↑b ^ logb (↑b) r
[PROOFSTEP]
exact rpow_le_rpow_of_exponent_le hb1'.le (Int.floor_le _)
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ Int.log b r ≤ ⌊logb (↑b) r⌋
[PROOFSTEP]
rw [Int.le_floor, le_logb_iff_rpow_le hb1' hr, rpow_int_cast]
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ ↑b ^ Int.log b r ≤ r
[PROOFSTEP]
exact Int.zpow_log_le_self hb hr
[GOAL]
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr : 0 ≤ r
⊢ ⌈logb (↑b) r⌉ = Int.clog b r
[PROOFSTEP]
obtain rfl | hr := hr.eq_or_lt
[GOAL]
case inl
b✝ x y : ℝ
b : ℕ
hb : 1 < b
hr : 0 ≤ 0
⊢ ⌈logb (↑b) 0⌉ = Int.clog b 0
[PROOFSTEP]
rw [logb_zero, Int.clog_zero_right, Int.ceil_zero]
[GOAL]
case inr
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
⊢ ⌈logb (↑b) r⌉ = Int.clog b r
[PROOFSTEP]
have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
[GOAL]
case inr
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ ⌈logb (↑b) r⌉ ≤ Int.clog b r
[PROOFSTEP]
rw [Int.ceil_le, logb_le_iff_le_rpow hb1' hr, rpow_int_cast]
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ Int.clog b r
[PROOFSTEP]
refine' Int.self_le_zpow_clog hb r
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ Int.clog b r ≤ ⌈logb (↑b) r⌉
[PROOFSTEP]
rw [← Int.le_zpow_iff_clog_le hb hr, ← rpow_int_cast b]
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ ↑⌈logb (↑b) r⌉
[PROOFSTEP]
refine' (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr).symm.trans_le _
[GOAL]
case inr.a
b✝ x y : ℝ
b : ℕ
r : ℝ
hb : 1 < b
hr✝ : 0 ≤ r
hr : 0 < r
hb1' : 1 < ↑b
⊢ ↑b ^ logb (↑b) r ≤ ↑b ^ ↑⌈logb (↑b) r⌉
[PROOFSTEP]
exact rpow_le_rpow_of_exponent_le hb1'.le (Int.le_ceil _)
[GOAL]
b x y : ℝ
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
simp_rw [logb, div_eq_zero_iff, log_eq_zero]
[GOAL]
b x y : ℝ
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
tauto
[GOAL]
b x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (x : α), x ∈ s → f x ≠ 0
⊢ logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s ha ih
· simp
simp only [Finset.mem_insert, forall_eq_or_imp] at hf 
simp [ha, ih hf.2, logb_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]
[GOAL]
b x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (x : α), x ∈ s → f x ≠ 0
⊢ logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
[PROOFSTEP]
induction' s using Finset.induction_on with a s ha ih
[GOAL]
case empty
b x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s → f x ≠ 0
hf : ∀ (x : α), x ∈ ∅ → f x ≠ 0
⊢ logb b (∏ i in ∅, f i) = ∑ i in ∅, logb b (f i)
[PROOFSTEP]
simp
[GOAL]
case insert
b x y : ℝ
α : Type u_1
s✝ : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s✝ → f x ≠ 0
a : α
s : Finset α
ha : ¬a ∈ s
ih : (∀ (x : α), x ∈ s → f x ≠ 0) → logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
hf : ∀ (x : α), x ∈ insert a s → f x ≠ 0
⊢ logb b (∏ i in insert a s, f i) = ∑ i in insert a s, logb b (f i)
[PROOFSTEP]
simp only [Finset.mem_insert, forall_eq_or_imp] at hf 
[GOAL]
case insert
b x y : ℝ
α : Type u_1
s✝ : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s✝ → f x ≠ 0
a : α
s : Finset α
ha : ¬a ∈ s
ih : (∀ (x : α), x ∈ s → f x ≠ 0) → logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
hf : f a ≠ 0 ∧ ∀ (a : α), a ∈ s → f a ≠ 0
⊢ logb b (∏ i in insert a s, f i) = ∑ i in insert a s, logb b (f i)
[PROOFSTEP]
simp [ha, ih hf.2, logb_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]
