[GOAL]
x y : ℝ
hx : 0 < x
⊢ log x = ↑(OrderIso.symm expOrderIso) { val := x, property := hx }
[PROOFSTEP]
rw [log_of_ne_zero hx.ne']
[GOAL]
x y : ℝ
hx : 0 < x
⊢ ↑(OrderIso.symm expOrderIso) { val := |x|, property := (_ : 0 < |x|) } =
    ↑(OrderIso.symm expOrderIso) { val := x, property := hx }
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h.e_val
x y : ℝ
hx : 0 < x
⊢ |x| = x
[PROOFSTEP]
exact abs_of_pos hx
[GOAL]
x y : ℝ
hx : x ≠ 0
⊢ exp (log x) = |x|
[PROOFSTEP]
rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ exp (log x) = x
[PROOFSTEP]
rw [exp_log_eq_abs hx.ne']
[GOAL]
x y : ℝ
hx : 0 < x
⊢ |x| = x
[PROOFSTEP]
exact abs_of_pos hx
[GOAL]
x y : ℝ
hx : x < 0
⊢ exp (log x) = -x
[PROOFSTEP]
rw [exp_log_eq_abs (ne_of_lt hx)]
[GOAL]
x y : ℝ
hx : x < 0
⊢ |x| = -x
[PROOFSTEP]
exact abs_of_neg hx
[GOAL]
x✝ y x : ℝ
⊢ x ≤ exp (log x)
[PROOFSTEP]
by_cases h_zero : x = 0
[GOAL]
case pos
x✝ y x : ℝ
h_zero : x = 0
⊢ x ≤ exp (log x)
[PROOFSTEP]
rw [h_zero, log, dif_pos rfl, exp_zero]
[GOAL]
case pos
x✝ y x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
case neg
x✝ y x : ℝ
h_zero : ¬x = 0
⊢ x ≤ exp (log x)
[PROOFSTEP]
rw [exp_log_eq_abs h_zero]
[GOAL]
case neg
x✝ y x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|
[PROOFSTEP]
exact le_abs_self _
[GOAL]
x y : ℝ
⊢ exp (log 1) = exp 0
[PROOFSTEP]
rw [exp_log zero_lt_one, exp_zero]
[GOAL]
x✝ y x : ℝ
⊢ log |x| = log x
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
x✝ y x : ℝ
h : x = 0
⊢ log |x| = log x
[PROOFSTEP]
simp [h]
[GOAL]
case neg
x✝ y x : ℝ
h : ¬x = 0
⊢ log |x| = log x
[PROOFSTEP]
rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]
[GOAL]
x✝ y x : ℝ
⊢ log (-x) = log x
[PROOFSTEP]
rw [← log_abs x, ← log_abs (-x), abs_neg]
[GOAL]
x✝ y x : ℝ
hx : 0 < x
⊢ sinh (log x) = (x - x⁻¹) / 2
[PROOFSTEP]
rw [sinh_eq, exp_neg, exp_log hx]
[GOAL]
x✝ y x : ℝ
hx : 0 < x
⊢ cosh (log x) = (x + x⁻¹) / 2
[PROOFSTEP]
rw [cosh_eq, exp_neg, exp_log hx]
[GOAL]
x✝¹ y x : ℝ
x✝ : x ∈ univ
⊢ log (-exp x) = x
[PROOFSTEP]
rw [log_neg_eq_log, log_exp]
[GOAL]
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ exp (log (x * y)) = exp (log x + log y)
[PROOFSTEP]
rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]
[GOAL]
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ exp (log (x / y)) = exp (log x - log y)
[PROOFSTEP]
rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]
[GOAL]
x✝ y x : ℝ
⊢ log x⁻¹ = -log x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x✝ y x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
x✝ y x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x
[PROOFSTEP]
rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
[GOAL]
x y : ℝ
h : 0 < x
h₁ : 0 < y
⊢ log x ≤ log y ↔ x ≤ y
[PROOFSTEP]
rw [← exp_le_exp, exp_log h, exp_log h₁]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ x < y → log x < log y
[PROOFSTEP]
intro h
[GOAL]
x y : ℝ
hx : 0 < x
h : x < y
⊢ log x < log y
[PROOFSTEP]
rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ x ≤ y → log x ≤ log y
[PROOFSTEP]
intro hxy
[GOAL]
x y : ℝ
hx : 0 < x
hxy : x ≤ y
⊢ log x ≤ log y
[PROOFSTEP]
cases hxy.eq_or_lt with
| inl h_eq => simp [h_eq]
| inr hlt => exact le_of_lt <| log_lt_log hx hlt
[GOAL]
x y : ℝ
hx : 0 < x
hxy : x ≤ y
x✝ : x = y ∨ x < y
⊢ log x ≤ log y
[PROOFSTEP]
cases hxy.eq_or_lt with
| inl h_eq => simp [h_eq]
| inr hlt => exact le_of_lt <| log_lt_log hx hlt
[GOAL]
case inl
x y : ℝ
hx : 0 < x
hxy : x ≤ y
h_eq : x = y
⊢ log x ≤ log y
[PROOFSTEP]

| inl h_eq => simp [h_eq]
[GOAL]
case inl
x y : ℝ
hx : 0 < x
hxy : x ≤ y
h_eq : x = y
⊢ log x ≤ log y
[PROOFSTEP]
simp [h_eq]
[GOAL]
case inr
x y : ℝ
hx : 0 < x
hxy : x ≤ y
hlt : x < y
⊢ log x ≤ log y
[PROOFSTEP]

| inr hlt => exact le_of_lt <| log_lt_log hx hlt
[GOAL]
case inr
x y : ℝ
hx : 0 < x
hxy : x ≤ y
hlt : x < y
⊢ log x ≤ log y
[PROOFSTEP]
exact le_of_lt <| log_lt_log hx hlt
[GOAL]
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y
[PROOFSTEP]
rw [← exp_lt_exp, exp_log hx, exp_log hy]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ log x ≤ y ↔ x ≤ exp y
[PROOFSTEP]
rw [← exp_le_exp, exp_log hx]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ log x < y ↔ x < exp y
[PROOFSTEP]
rw [← exp_lt_exp, exp_log hx]
[GOAL]
x y : ℝ
hy : 0 < y
⊢ x ≤ log y ↔ exp x ≤ y
[PROOFSTEP]
rw [← exp_le_exp, exp_log hy]
[GOAL]
x y : ℝ
hy : 0 < y
⊢ x < log y ↔ exp x < y
[PROOFSTEP]
rw [← exp_lt_exp, exp_log hy]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ 0 < log x ↔ 1 < x
[PROOFSTEP]
rw [← log_one]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x
[PROOFSTEP]
exact log_lt_log_iff zero_lt_one hx
[GOAL]
x y : ℝ
hx : x < -1
⊢ 0 < log x
[PROOFSTEP]
rw [← neg_neg x, log_neg_eq_log]
[GOAL]
x y : ℝ
hx : x < -1
⊢ 0 < log (-x)
[PROOFSTEP]
have : 1 < -x := by linarith
[GOAL]
x y : ℝ
hx : x < -1
⊢ 1 < -x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hx : x < -1
this : 1 < -x
⊢ 0 < log (-x)
[PROOFSTEP]
exact log_pos this
[GOAL]
x y : ℝ
h : 0 < x
⊢ log x < 0 ↔ x < 1
[PROOFSTEP]
rw [← log_one]
[GOAL]
x y : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1
[PROOFSTEP]
exact log_lt_log_iff h zero_lt_one
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log x < 0
[PROOFSTEP]
rw [← neg_neg x, log_neg_eq_log]
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log (-x) < 0
[PROOFSTEP]
have h0' : 0 < -x := by linarith
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
⊢ 0 < -x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ log (-x) < 0
[PROOFSTEP]
have h1' : -x < 1 := by linarith
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
⊢ -x < 1
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
h0 : x < 0
h1 : -1 < x
h0' : 0 < -x
h1' : -x < 1
⊢ log (-x) < 0
[PROOFSTEP]
exact log_neg h0' h1'
[GOAL]
x y : ℝ
hx : 0 < x
⊢ 0 ≤ log x ↔ 1 ≤ x
[PROOFSTEP]
rw [← not_lt, log_neg_iff hx, not_lt]
[GOAL]
x y : ℝ
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
rw [← not_lt, log_pos_iff hx, not_lt]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ log x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
rcases hx.eq_or_lt with (rfl | hx)
[GOAL]
case inl
y : ℝ
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1
[PROOFSTEP]
simp [le_refl, zero_le_one]
[GOAL]
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
[PROOFSTEP]
exact log_nonpos_iff hx
[GOAL]
x y : ℝ
n : ℕ
⊢ 0 ≤ log ↑n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
x y : ℝ
n : ℕ
hn : n = 0
⊢ 0 ≤ log ↑n
case neg x y : ℝ n : ℕ hn : ¬n = 0 ⊢ 0 ≤ log ↑n
[PROOFSTEP]
case pos => simp [hn]
[GOAL]
x y : ℝ
n : ℕ
hn : n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
case pos => simp [hn]
[GOAL]
x y : ℝ
n : ℕ
hn : n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
x y : ℝ
n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
case neg =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
  exact log_nonneg this
[GOAL]
x y : ℝ
n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
case neg =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
  exact log_nonneg this
[GOAL]
x y : ℝ
n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
have : (1 : ℝ) ≤ n := by exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
[GOAL]
x y : ℝ
n : ℕ
hn : ¬n = 0
⊢ 1 ≤ ↑n
[PROOFSTEP]
exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
[GOAL]
x y : ℝ
n : ℕ
hn : ¬n = 0
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
exact log_nonneg this
[GOAL]
x y : ℝ
n : ℕ
⊢ 0 ≤ log (-↑n)
[PROOFSTEP]
rw [← log_neg_eq_log, neg_neg]
[GOAL]
x y : ℝ
n : ℕ
⊢ 0 ≤ log ↑n
[PROOFSTEP]
exact log_nat_cast_nonneg _
[GOAL]
x y : ℝ
n : ℤ
⊢ 0 ≤ log ↑n
[PROOFSTEP]
cases lt_trichotomy 0 n with
| inl hn =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast hn
  exact log_nonneg this
| inr hn =>
  cases hn with
  | inl hn => simp [hn.symm]
  | inr hn =>
    have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
    rw [← log_neg_eq_log]
    exact log_nonneg this
[GOAL]
x y : ℝ
n : ℤ
x✝ : 0 < n ∨ 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
cases lt_trichotomy 0 n with
| inl hn =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast hn
  exact log_nonneg this
| inr hn =>
  cases hn with
  | inl hn => simp [hn.symm]
  | inr hn =>
    have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
    rw [← log_neg_eq_log]
    exact log_nonneg this
[GOAL]
case inl
x y : ℝ
n : ℤ
hn : 0 < n
⊢ 0 ≤ log ↑n
[PROOFSTEP]

| inl hn =>
  have : (1 : ℝ) ≤ n := by exact_mod_cast hn
  exact log_nonneg this
[GOAL]
case inl
x y : ℝ
n : ℤ
hn : 0 < n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
have : (1 : ℝ) ≤ n := by exact_mod_cast hn
[GOAL]
x y : ℝ
n : ℤ
hn : 0 < n
⊢ 1 ≤ ↑n
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case inl
x y : ℝ
n : ℤ
hn : 0 < n
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
exact log_nonneg this
[GOAL]
case inr
x y : ℝ
n : ℤ
hn : 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]

| inr hn =>
  cases hn with
  | inl hn => simp [hn.symm]
  | inr hn =>
    have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
    rw [← log_neg_eq_log]
    exact log_nonneg this
[GOAL]
case inr
x y : ℝ
n : ℤ
hn : 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
cases hn with
| inl hn => simp [hn.symm]
| inr hn =>
  have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
  rw [← log_neg_eq_log]
  exact log_nonneg this
[GOAL]
case inr
x y : ℝ
n : ℤ
hn : 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
cases hn with
| inl hn => simp [hn.symm]
| inr hn =>
  have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
  rw [← log_neg_eq_log]
  exact log_nonneg this
[GOAL]
case inr.inl
x y : ℝ
n : ℤ
hn : 0 = n
⊢ 0 ≤ log ↑n
[PROOFSTEP]

| inl hn => simp [hn.symm]
[GOAL]
case inr.inl
x y : ℝ
n : ℤ
hn : 0 = n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
simp [hn.symm]
[GOAL]
case inr.inr
x y : ℝ
n : ℤ
hn : n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]

| inr hn =>
  have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
  rw [← log_neg_eq_log]
  exact log_nonneg this
[GOAL]
case inr.inr
x y : ℝ
n : ℤ
hn : n < 0
⊢ 0 ≤ log ↑n
[PROOFSTEP]
have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn ; exact_mod_cast hn
[GOAL]
x y : ℝ
n : ℤ
hn : n < 0
⊢ 1 ≤ -↑n
[PROOFSTEP]
rw [← neg_zero, ← lt_neg] at hn 
[GOAL]
x y : ℝ
n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case inr.inr
x y : ℝ
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log ↑n
[PROOFSTEP]
rw [← log_neg_eq_log]
[GOAL]
case inr.inr
x y : ℝ
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log (-↑n)
[PROOFSTEP]
exact log_nonneg this
[GOAL]
x y : ℝ
⊢ StrictAntiOn log (Iio 0)
[PROOFSTEP]
rintro x (hx : x < 0) y (hy : y < 0) hxy
[GOAL]
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log y < log x
[PROOFSTEP]
rw [← log_abs y, ← log_abs x]
[GOAL]
x✝ y✝ x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log |y| < log |x|
[PROOFSTEP]
refine' log_lt_log (abs_pos.2 hy.ne) _
[GOAL]
x✝ y✝ 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]
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x < x - 1
[PROOFSTEP]
have h : log x ≠ 0
[GOAL]
case h
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ 0
[PROOFSTEP]
rwa [← log_one, log_injOn_pos.ne_iff hx1]
[GOAL]
case h
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0
[PROOFSTEP]
exact mem_Ioi.mpr zero_lt_one
[GOAL]
x y : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
⊢ log x < x - 1
[PROOFSTEP]
linarith [add_one_lt_exp_of_nonzero h, exp_log hx1]
[GOAL]
x✝ y x : ℝ
⊢ log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
constructor
[GOAL]
case mp
x✝ y x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
intro h
[GOAL]
case mp
x✝ y x : ℝ
h : log x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)
[GOAL]
case mp.inl
x✝ y x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
refine' Or.inr (Or.inr (neg_eq_iff_eq_neg.mp _))
[GOAL]
case mp.inl
x✝ y x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1
[PROOFSTEP]
rw [← log_neg_eq_log x] at h 
[GOAL]
case mp.inl
x✝ y x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1
[PROOFSTEP]
exact eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h
[GOAL]
case mp.inr.inl
x y : ℝ
h : log 0 = 0
⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = -1
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case mp.inr.inr
x✝ y x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1
[PROOFSTEP]
exact Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))
[GOAL]
case mpr
x✝ y x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0
[PROOFSTEP]
rintro (rfl | rfl | rfl)
[GOAL]
case mpr.inl
x y : ℝ
⊢ log 0 = 0
[PROOFSTEP]
simp only [log_one, log_zero, log_neg_eq_log]
[GOAL]
case mpr.inr.inl
x y : ℝ
⊢ log 1 = 0
[PROOFSTEP]
simp only [log_one, log_zero, log_neg_eq_log]
[GOAL]
case mpr.inr.inr
x y : ℝ
⊢ log (-1) = 0
[PROOFSTEP]
simp only [log_one, log_zero, log_neg_eq_log]
[GOAL]
x✝ y x : ℝ
⊢ log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1
[PROOFSTEP]
simpa only [not_or] using log_eq_zero.not
[GOAL]
x✝ y x : ℝ
n : ℕ
⊢ log (x ^ n) = ↑n * log x
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
x✝ y x : ℝ
⊢ log (x ^ Nat.zero) = ↑Nat.zero * log x
[PROOFSTEP]
simp
[GOAL]
case succ
x✝ y x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
⊢ log (x ^ Nat.succ n) = ↑(Nat.succ n) * log x
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case succ.inl
x y : ℝ
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ Nat.succ n) = ↑(Nat.succ n) * log 0
[PROOFSTEP]
simp
[GOAL]
case succ.inr
x✝ y x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ Nat.succ n) = ↑(Nat.succ n) * log x
[PROOFSTEP]
rw [pow_succ', log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
[GOAL]
x✝ y x : ℝ
n : ℤ
⊢ log (x ^ n) = ↑n * log x
[PROOFSTEP]
induction n
[GOAL]
case ofNat
x✝ y x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.ofNat a✝) = ↑(Int.ofNat a✝) * log x
[PROOFSTEP]
rw [Int.ofNat_eq_coe, zpow_ofNat, log_pow, Int.cast_ofNat]
[GOAL]
case negSucc
x✝ y x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.negSucc a✝) = ↑(Int.negSucc a✝) * log x
[PROOFSTEP]
rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]
[GOAL]
x✝ y x : ℝ
hx : 0 ≤ x
⊢ log (sqrt x) = log x / 2
[PROOFSTEP]
rw [eq_div_iff, mul_comm, ← Nat.cast_two, ← log_pow, sq_sqrt hx]
[GOAL]
x✝ y x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0
[PROOFSTEP]
exact two_ne_zero
[GOAL]
x✝ y x : ℝ
hx : 0 < x
⊢ log x ≤ x - 1
[PROOFSTEP]
rw [le_sub_iff_add_le]
[GOAL]
x✝ y x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x
[PROOFSTEP]
convert add_one_le_exp (log x)
[GOAL]
case h.e'_4
x✝ y x : ℝ
hx : 0 < x
⊢ x = exp (log x)
[PROOFSTEP]
rw [exp_log hx]
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ |log x * x| < 1
[PROOFSTEP]
have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ 0 < 1 / x
[PROOFSTEP]
simpa only [one_div, inv_pos] using h1
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ |log x * x| < 1
[PROOFSTEP]
replace := log_le_sub_one_of_pos this
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ |log x * x| < 1
[PROOFSTEP]
replace : log (1 / x) < 1 / x := by linarith
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ log (1 / x) < 1 / x
[PROOFSTEP]
linarith
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ |log x * x| < 1
[PROOFSTEP]
rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff h1] at this 
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1
[PROOFSTEP]
have aux : 0 ≤ -log x * x := by
  refine' mul_nonneg _ h1.le
  rw [← log_inv]
  apply log_nonneg
  rw [← le_inv h1 zero_lt_one, inv_one]
  exact h2
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x * x
[PROOFSTEP]
refine' mul_nonneg _ h1.le
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x
[PROOFSTEP]
rw [← log_inv]
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹
[PROOFSTEP]
apply log_nonneg
[GOAL]
case hx
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹
[PROOFSTEP]
rw [← le_inv h1 zero_lt_one, inv_one]
[GOAL]
case hx
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1
[PROOFSTEP]
exact h2
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1
[PROOFSTEP]
rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this 
[GOAL]
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |log x * x| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1
[PROOFSTEP]
exact this
[GOAL]
x y : ℝ
⊢ Tendsto (fun x => log (exp x)) atTop atTop
[PROOFSTEP]
simpa only [log_exp] using tendsto_id
[GOAL]
x y : ℝ
⊢ Tendsto log (𝓝[{0}ᶜ] 0) atBot
[PROOFSTEP]
rw [← show _ = log from funext log_abs]
[GOAL]
x y : ℝ
⊢ Tendsto (fun x => log |x|) (𝓝[{0}ᶜ] 0) atBot
[PROOFSTEP]
refine' Tendsto.comp (g := log) _ tendsto_abs_nhdsWithin_zero
[GOAL]
x y : ℝ
⊢ Tendsto log (𝓝[Ioi 0] 0) atBot
[PROOFSTEP]
simpa [← tendsto_comp_exp_atBot] using tendsto_id
[GOAL]
x y : ℝ
⊢ ContinuousOn log {0}ᶜ
[PROOFSTEP]
simp only [continuousOn_iff_continuous_restrict, restrict]
[GOAL]
x y : ℝ
⊢ Continuous fun x => log ↑x
[PROOFSTEP]
conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
[GOAL]
x✝ y : ℝ
x : ↑{0}ᶜ
| log ↑x
[PROOFSTEP]
rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
[GOAL]
x✝ y : ℝ
x : ↑{0}ᶜ
| log ↑x
[PROOFSTEP]
rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
[GOAL]
x✝ y : ℝ
x : ↑{0}ᶜ
| log ↑x
[PROOFSTEP]
rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
[GOAL]
x y : ℝ
⊢ Continuous fun x => ↑(OrderIso.symm expOrderIso) { val := |↑x|, property := (_ : 0 < |↑x|) }
[PROOFSTEP]
exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)
[GOAL]
x y : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0
[PROOFSTEP]
refine' ⟨_, continuousAt_log⟩
[GOAL]
x y : ℝ
⊢ ContinuousAt log x → x ≠ 0
[PROOFSTEP]
rintro h rfl
[GOAL]
y : ℝ
h : ContinuousAt log 0
⊢ False
[PROOFSTEP]
exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsWithin_zero _ (h.tendsto.mono_left inf_le_left)
[GOAL]
x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (x : α), x ∈ s → f x ≠ 0
⊢ log (∏ i in s, f i) = ∑ i in s, log (f i)
[PROOFSTEP]
induction' s using Finset.cons_induction_on with a s ha ih
[GOAL]
case h₁
x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s → f x ≠ 0
hf : ∀ (x : α), x ∈ ∅ → f x ≠ 0
⊢ log (∏ i in ∅, f i) = ∑ i in ∅, log (f i)
[PROOFSTEP]
simp
[GOAL]
case h₂
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) → log (∏ i in s, f i) = ∑ i in s, log (f i)
hf : ∀ (x : α), x ∈ Finset.cons a s ha → f x ≠ 0
⊢ log (∏ i in Finset.cons a s ha, f i) = ∑ i in Finset.cons a s ha, log (f i)
[PROOFSTEP]
rw [Finset.forall_mem_cons] at hf 
[GOAL]
case h₂
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) → log (∏ i in s, f i) = ∑ i in s, log (f i)
hf : f a ≠ 0 ∧ ∀ (x : α), x ∈ s → f x ≠ 0
⊢ log (∏ i in Finset.cons a s ha, f i) = ∑ i in Finset.cons a s ha, log (f i)
[PROOFSTEP]
simp [ih hf.2, log_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]
[GOAL]
x y : ℝ
n : ℕ
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => ↑t * log ↑p
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
x y : ℝ
⊢ log ↑0 = Finsupp.sum (Nat.factorization 0) fun p t => ↑t * log ↑p
[PROOFSTEP]
simp
  -- relies on junk values of `log` and `Nat.factorization`
[GOAL]
case inr
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => ↑t * log ↑p
[PROOFSTEP]
simp only [← log_pow, ← Nat.cast_pow]
[GOAL]
case inr
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => log ↑(p ^ t)
[PROOFSTEP]
rw [← Finsupp.log_prod, ← Nat.cast_finsupp_prod, Nat.factorization_prod_pow_eq_self hn]
[GOAL]
case inr.hg
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ ↑(Nat.factorization n) a) = 0 → ↑(Nat.factorization n) a = 0
[PROOFSTEP]
intro p hp
[GOAL]
case inr.hg
x y : ℝ
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ ↑(Nat.factorization n) p) = 0
⊢ ↑(Nat.factorization n) p = 0
[PROOFSTEP]
rw [pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]
[GOAL]
x y a b : ℝ
n : ℕ
ha : a ≠ 0
⊢ (fun x => x ^ n / (a * exp x + b)) ∘ log =ᶠ[atTop] fun x => log x ^ n / (a * x + b)
[PROOFSTEP]
filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]
[GOAL]
x✝ y a b : ℝ
n : ℕ
ha : a ≠ 0
x : ℝ
hx : 0 < x
⊢ ((fun x => x ^ n / (a * exp x + b)) ∘ log) x = log x ^ n / (a * x + b)
[PROOFSTEP]
simp [exp_log hx]
[GOAL]
x y : ℝ
n : ℕ
⊢ (fun x => log x ^ n) =o[atTop] id
[PROOFSTEP]
rw [Asymptotics.isLittleO_iff_tendsto']
[GOAL]
x y : ℝ
n : ℕ
⊢ Tendsto (fun x => log x ^ n / id x) atTop (𝓝 0)
[PROOFSTEP]
simpa using tendsto_pow_log_div_mul_add_atTop 1 0 n one_ne_zero
[GOAL]
x y : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
[PROOFSTEP]
filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim
[GOAL]
x y c : ℝ
⊢ (fun x => c) =o[atTop] log
[PROOFSTEP]
refine Asymptotics.isLittleO_of_tendsto' ?_ <| Tendsto.div_atTop (a := c) (by simp) tendsto_log_atTop
[GOAL]
x y c : ℝ
⊢ Tendsto (fun x => c) atTop (𝓝 c)
[PROOFSTEP]
simp
[GOAL]
x y c : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0
[PROOFSTEP]
filter_upwards [eventually_gt_atTop 1] with x hx
[GOAL]
case h
x✝ y c x : ℝ
hx : 1 < x
⊢ log x = 0 → c = 0
[PROOFSTEP]
aesop (add safe forward log_pos)
[GOAL]
y : ℝ
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
[PROOFSTEP]
have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
[GOAL]
case this
y : ℝ
⊢ Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
[PROOFSTEP]
exact tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)
[GOAL]
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
[PROOFSTEP]
rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]
[GOAL]
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (exp ∘ fun x => log (x + y) - log x) atTop (𝓝 (1 + 0))
[PROOFSTEP]
refine' this.congr' _
[GOAL]
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ (fun x => 1 + y / x) =ᶠ[atTop] exp ∘ fun x => log (x + y) - log x
[PROOFSTEP]
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy
[GOAL]
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (exp ∘ fun x => log (x + y) - log x) x
[PROOFSTEP]
rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div]
[GOAL]
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ x ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x
[PROOFSTEP]
linarith
[GOAL]
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y
[PROOFSTEP]
linarith
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log e
[PROOFSTEP]
rw [NormNum.IsNat.to_eq h rfl]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log ↑n
[PROOFSTEP]
exact Real.log_nat_cast_nonneg _
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log e
[PROOFSTEP]
rw [NormNum.IsNat.to_eq h rfl]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n
[PROOFSTEP]
apply Real.log_pos
[GOAL]
case hx
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 1 < ↑n
[PROOFSTEP]
simpa using w
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log e
[PROOFSTEP]
rw [NormNum.IsInt.neg_to_eq h rfl]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-↑n)
[PROOFSTEP]
exact Real.log_neg_nat_cast_nonneg _
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log e
[PROOFSTEP]
rw [NormNum.IsInt.neg_to_eq h rfl]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (-↑n)
[PROOFSTEP]
rw [Real.log_neg_eq_log]
[GOAL]
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n
[PROOFSTEP]
apply Real.log_pos
[GOAL]
case hx
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 1 < ↑n
[PROOFSTEP]
simpa using w
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log e
[PROOFSTEP]
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log (↑n / ↑d)
[PROOFSTEP]
have : 1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 1 < ↑n / ↑d
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
this : 1 < ↑n / ↑d
⊢ 0 < Real.log (↑n / ↑d)
[PROOFSTEP]
exact Real.log_pos this
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log e
[PROOFSTEP]
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log (↑n / ↑d)
[PROOFSTEP]
have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ ↑n / ↑d < -1
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
this : ↑n / ↑d < -1
⊢ 0 < Real.log (↑n / ↑d)
[PROOFSTEP]
exact Real.log_pos_of_lt_neg_one this
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log e ≠ 0
[PROOFSTEP]
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
have h₁' : 0 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₁
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ 0 < ↑n / ↑d
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h₁
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
have h₂' : (n : ℝ) / d < 1 := by exact_mod_cast of_decide_eq_true h₂
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ ↑n / ↑d < 1
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h₂
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
h₂' : ↑n / ↑d < 1
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
exact ne_of_lt <| Real.log_neg h₁' h₂'
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log e ≠ 0
[PROOFSTEP]
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
have h₁' : (n : ℝ) / d < 0 := by exact_mod_cast of_decide_eq_true h₁
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ ↑n / ↑d < 0
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h₁
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
have h₂' : -1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₂
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
⊢ -1 < ↑n / ↑d
[PROOFSTEP]
exact_mod_cast of_decide_eq_true h₂
[GOAL]
e : ℝ
n : ℤ
d : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
h₂' : -1 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0
[PROOFSTEP]
exact ne_of_lt <| Real.log_neg_of_lt_zero h₁' h₂'
[GOAL]
$x✝ : Type x✝
«$_zα» : Zero $x✝
«$_pα» : PartialOrder $x✝
«$e» : $x✝
«$f» : ℝ → ℝ
«$a» : ℝ
«$n» : ℤ
«$d» : ℕ
«$i» : DivisionRing ℝ := Real.instDivisionRingReal
«$p» : NormNum.IsRat «$a» «$n» «$d»
⊢ Sort ?u.471336
[PROOFSTEP]
clear! «$i»
[GOAL]
$x✝ : Type x✝
«$_zα» : Zero $x✝
«$_pα» : PartialOrder $x✝
«$e» : $x✝
«$f» : ℝ → ℝ
«$a» : ℝ
«$n» : ℤ
«$d» : ℕ
⊢ Sort ?u.471336
[PROOFSTEP]
exact NormNum.IsRat «$a» «$n» «$d»
