[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
[PROOFSTEP]
simp only [rpow_def, Complex.cpow_def]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 1.re = 1
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 1.re = 0
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ↑y = 0
h✝ : ¬x = 0
⊢ 1.re = exp (log x * y)
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 0.re = 1
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0.re = 0
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ¬↑y = 0
h✝ : ¬x = 0
⊢ 0.re = exp (log x * y)
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 1
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 0
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : ¬↑x = 0
h✝ : ¬x = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = exp (log x * y)
[PROOFSTEP]
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul, (Complex.ofReal_mul _ _).symm,
  Complex.exp_ofReal_re, Complex.ofReal_eq_zero]
[GOAL]
x : ℝ
hx : 0 < x
y : ℝ
⊢ x ^ y = exp (log x * y)
[PROOFSTEP]
rw [rpow_def_of_nonneg (le_of_lt hx), if_neg (ne_of_gt hx)]
[GOAL]
x y : ℝ
⊢ exp (x * y) = exp x ^ y
[PROOFSTEP]
rw [rpow_def_of_pos (exp_pos _), log_exp]
[GOAL]
x : ℝ
⊢ exp 1 ^ x = exp x
[PROOFSTEP]
rw [← exp_mul, one_mul]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp only [rpow_def_of_nonneg hx]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
case neg
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
case neg
x y : ℝ
hx : 0 ≤ x
h✝ : ¬x = 0
⊢ exp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
⊢ x ^ y = exp (log x * y) * cos (y * π)
[PROOFSTEP]
rw [rpow_def, Complex.cpow_def, if_neg]
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = exp (log x * y) * cos (y * π)
case hnc x : ℝ hx : x < 0 y : ℝ ⊢ ¬↑x = 0
[PROOFSTEP]
have : Complex.log x * y = ↑(log (-x) * y) + ↑(y * π) * Complex.I :=
  by
  simp only [Complex.log, abs_of_neg hx, Complex.arg_ofReal_of_neg hx, Complex.abs_ofReal, Complex.ofReal_mul]
  ring
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
⊢ Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
[PROOFSTEP]
simp only [Complex.log, abs_of_neg hx, Complex.arg_ofReal_of_neg hx, Complex.abs_ofReal, Complex.ofReal_mul]
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
⊢ (↑(log (-x)) + ↑π * Complex.I) * ↑y = ↑(log (-x)) * ↑y + ↑y * ↑π * Complex.I
[PROOFSTEP]
ring
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = exp (log x * y) * cos (y * π)
[PROOFSTEP]
rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ← Complex.ofReal_sin, mul_add, ←
  Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul, Complex.add_re, Complex.ofReal_re, Complex.mul_re,
  Complex.I_re, Complex.ofReal_im, Real.log_neg_eq_log]
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ exp (log x * y) * cos (y * π) + ((↑(exp (log x * y) * sin (y * π))).re * 0 - 0 * Complex.I.im) =
    exp (log x * y) * cos (y * π)
[PROOFSTEP]
ring
[GOAL]
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0
[PROOFSTEP]
rw [Complex.ofReal_eq_zero]
[GOAL]
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0
[PROOFSTEP]
exact ne_of_lt hx
[GOAL]
x : ℝ
hx : x ≤ 0
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y) * cos (y * π)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h✝ : y = 0
⊢ x ^ y = 1
[PROOFSTEP]
simp [rpow_def, *]
[GOAL]
case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h✝ : ¬y = 0
⊢ x ^ y = 0
[PROOFSTEP]
simp [rpow_def, *]
[GOAL]
case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ x ^ y = exp (log x * y) * cos (y * π)
[PROOFSTEP]
simp [rpow_def, *]
[GOAL]
case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ (↑x ^ ↑y).re = exp (log x * y) * cos (y * π)
[PROOFSTEP]
exact rpow_def_of_neg (lt_of_le_of_ne hx h) _
[GOAL]
x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < x ^ y
[PROOFSTEP]
rw [rpow_def_of_pos hx]
[GOAL]
x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < exp (log x * y)
[PROOFSTEP]
apply exp_pos
[GOAL]
x : ℝ
⊢ x ^ 0 = 1
[PROOFSTEP]
simp [rpow_def]
[GOAL]
x : ℝ
⊢ 0 < x ^ 0
[PROOFSTEP]
simp
[GOAL]
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0
[PROOFSTEP]
simp [rpow_def, *]
[GOAL]
x a : ℝ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
x a : ℝ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
intro hyp
[GOAL]
case mp
x a : ℝ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
simp only [rpow_def, Complex.ofReal_zero] at hyp 
[GOAL]
case mp
x a : ℝ
hyp : (0 ^ ↑x).re = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
by_cases x = 0
[GOAL]
case mp
x a : ℝ
hyp : (0 ^ ↑x).re = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
by_cases x = 0
[GOAL]
case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
subst h
[GOAL]
case pos
a : ℝ
hyp : (0 ^ ↑0).re = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
[PROOFSTEP]
simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp 
[GOAL]
case pos
a : ℝ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
[PROOFSTEP]
exact Or.inr ⟨rfl, hyp.symm⟩
[GOAL]
case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp 
[GOAL]
case neg
x a : ℝ
hyp : 0.re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
exact Or.inl ⟨h, hyp.symm⟩
[GOAL]
case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
[PROOFSTEP]
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case mpr.inl.intro
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0
[PROOFSTEP]
exact zero_rpow h
[GOAL]
case mpr.inr.intro
⊢ 0 ^ 0 = 1
[PROOFSTEP]
exact rpow_zero _
[GOAL]
x a : ℝ
⊢ a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
rw [← zero_rpow_eq_iff, eq_comm]
[GOAL]
x : ℝ
⊢ x ^ 1 = x
[PROOFSTEP]
simp [rpow_def]
[GOAL]
x : ℝ
⊢ 1 ^ x = 1
[PROOFSTEP]
simp [rpow_def]
[GOAL]
x : ℝ
⊢ 0 ^ x ≤ 1
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
x : ℝ
h : x = 0
⊢ 0 ^ x ≤ 1
[PROOFSTEP]
simp [h, zero_le_one]
[GOAL]
case neg
x : ℝ
h : ¬x = 0
⊢ 0 ^ x ≤ 1
[PROOFSTEP]
simp [h, zero_le_one]
[GOAL]
x : ℝ
⊢ 0 ≤ 0 ^ x
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
x : ℝ
h : x = 0
⊢ 0 ≤ 0 ^ x
[PROOFSTEP]
simp [h, zero_le_one]
[GOAL]
case neg
x : ℝ
h : ¬x = 0
⊢ 0 ≤ 0 ^ x
[PROOFSTEP]
simp [h, zero_le_one]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ x ^ y
[PROOFSTEP]
rw [rpow_def_of_nonneg hx]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : y = 0
⊢ 0 ≤ 1
[PROOFSTEP]
simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 0
[PROOFSTEP]
simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ 0 ≤ exp (log x * y)
[PROOFSTEP]
simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]
[GOAL]
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y
[PROOFSTEP]
have h_rpow_nonneg : 0 ≤ x ^ y := Real.rpow_nonneg_of_nonneg hx_nonneg _
[GOAL]
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = |x| ^ y
[PROOFSTEP]
rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg]
[GOAL]
x y : ℝ
⊢ |x ^ y| ≤ |x| ^ y
[PROOFSTEP]
cases' le_or_lt 0 x with hx hx
[GOAL]
case inl
x y : ℝ
hx : 0 ≤ x
⊢ |x ^ y| ≤ |x| ^ y
[PROOFSTEP]
rw [abs_rpow_of_nonneg hx]
[GOAL]
case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y
[PROOFSTEP]
rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul, abs_of_pos (exp_pos _)]
[GOAL]
case inr
x y : ℝ
hx : x < 0
⊢ exp (log x * y) * |cos (y * π)| ≤ exp (log x * y)
[PROOFSTEP]
exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)
[GOAL]
x y : ℝ
⊢ |x ^ y| ≤ exp (log x * y)
[PROOFSTEP]
refine' (abs_rpow_le_abs_rpow x y).trans _
[GOAL]
x y : ℝ
⊢ |x| ^ y ≤ exp (log x * y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x y : ℝ
hx : x = 0
⊢ |x| ^ y ≤ exp (log x * y)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
x y : ℝ
hx : x = 0
hy : y = 0
⊢ |x| ^ y ≤ exp (log x * y)
[PROOFSTEP]
simp [hx, hy, zero_le_one]
[GOAL]
case neg
x y : ℝ
hx : x = 0
hy : ¬y = 0
⊢ |x| ^ y ≤ exp (log x * y)
[PROOFSTEP]
simp [hx, hy, zero_le_one]
[GOAL]
case neg
x y : ℝ
hx : ¬x = 0
⊢ |x| ^ y ≤ exp (log x * y)
[PROOFSTEP]
rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]
[GOAL]
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ ‖x ^ y‖ = ‖x‖ ^ y
[PROOFSTEP]
simp_rw [Real.norm_eq_abs]
[GOAL]
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y
[PROOFSTEP]
exact abs_rpow_of_nonneg hx_nonneg
[GOAL]
x y✝ z✝ : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y + z) = x ^ y * x ^ z
[PROOFSTEP]
simp only [rpow_def_of_pos hx, mul_add, exp_add]
[GOAL]
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z
[PROOFSTEP]
rcases hx.eq_or_lt with (rfl | pos)
[GOAL]
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z
[PROOFSTEP]
rw [zero_rpow h, zero_eq_mul]
[GOAL]
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0
[PROOFSTEP]
have : y ≠ 0 ∨ z ≠ 0 := not_and_or.1 fun ⟨hy, hz⟩ => h <| hy.symm ▸ hz.symm ▸ zero_add 0
[GOAL]
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
this : y ≠ 0 ∨ z ≠ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0
[PROOFSTEP]
exact this.imp zero_rpow zero_rpow
[GOAL]
case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
[PROOFSTEP]
exact rpow_add pos _ _
[GOAL]
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z
[PROOFSTEP]
rcases hy.eq_or_lt with (rfl | hy)
[GOAL]
case inl
x z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ x ^ (0 + z) = x ^ 0 * x ^ z
[PROOFSTEP]
rw [zero_add, rpow_zero, one_mul]
[GOAL]
case inr
x y z : ℝ
hx : 0 ≤ x
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ x ^ (y + z) = x ^ y * x ^ z
[PROOFSTEP]
exact rpow_add' hx (ne_of_gt <| add_pos_of_pos_of_nonneg hy hz)
[GOAL]
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
[PROOFSTEP]
rcases le_iff_eq_or_lt.1 hx with (H | pos)
[GOAL]
case inl
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
[PROOFSTEP]
by_cases h : y + z = 0
[GOAL]
case pos
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
[PROOFSTEP]
simp only [H.symm, h, rpow_zero]
[GOAL]
case pos
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1
[PROOFSTEP]
calc
  (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 := mul_le_mul (zero_rpow_le_one y) (zero_rpow_le_one z) (zero_rpow_nonneg z) zero_le_one
  _ = 1 := by simp
[GOAL]
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
case neg
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
[PROOFSTEP]
simp [rpow_add', ← H, h]
[GOAL]
case inr
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
[PROOFSTEP]
simp [rpow_add pos]
[GOAL]
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h : ∀ (x : ι), x ∈ s → 0 ≤ f x
⊢ a ^ ∑ x in s, f x = ∏ x in s, a ^ f x
[PROOFSTEP]
induction' s using Finset.cons_induction with i s hi ihs
[GOAL]
case empty
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s → 0 ≤ f x
h : ∀ (x : ι), x ∈ ∅ → 0 ≤ f x
⊢ a ^ ∑ x in ∅, f x = ∏ x in ∅, a ^ f x
[PROOFSTEP]
rw [sum_empty, Finset.prod_empty, rpow_zero]
[GOAL]
case cons
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s✝ : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s✝ → 0 ≤ f x
i : ι
s : Finset ι
hi : ¬i ∈ s
ihs : (∀ (x : ι), x ∈ s → 0 ≤ f x) → a ^ ∑ x in s, f x = ∏ x in s, a ^ f x
h : ∀ (x : ι), x ∈ cons i s hi → 0 ≤ f x
⊢ a ^ ∑ x in cons i s hi, f x = ∏ x in cons i s hi, a ^ f x
[PROOFSTEP]
rw [forall_mem_cons] at h 
[GOAL]
case cons
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s✝ : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s✝ → 0 ≤ f x
i : ι
s : Finset ι
hi : ¬i ∈ s
ihs : (∀ (x : ι), x ∈ s → 0 ≤ f x) → a ^ ∑ x in s, f x = ∏ x in s, a ^ f x
h : 0 ≤ f i ∧ ∀ (x : ι), x ∈ s → 0 ≤ f x
⊢ a ^ ∑ x in cons i s hi, f x = ∏ x in cons i s hi, a ^ f x
[PROOFSTEP]
rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]
[GOAL]
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹
[PROOFSTEP]
simp only [rpow_def_of_nonneg hx]
[GOAL]
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if x = 0 then if -y = 0 then 1 else 0 else exp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y))⁻¹
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : y = 0
⊢ 1 = 1⁻¹
[PROOFSTEP]
simp_all [exp_neg]
[GOAL]
case neg
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : ¬y = 0
⊢ 1 = 0⁻¹
[PROOFSTEP]
simp_all [exp_neg]
[GOAL]
case pos
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : y = 0
⊢ 0 = 1⁻¹
[PROOFSTEP]
simp_all [exp_neg]
[GOAL]
case neg
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹
[PROOFSTEP]
simp_all [exp_neg]
[GOAL]
case neg
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ exp (log x * -y) = (exp (log x * y))⁻¹
[PROOFSTEP]
simp_all [exp_neg]
[GOAL]
x✝ y✝ z✝ x : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y - z) = x ^ y / x ^ z
[PROOFSTEP]
simp only [sub_eq_add_neg, rpow_add hx, rpow_neg (le_of_lt hx), div_eq_mul_inv]
[GOAL]
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y - z ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z
[PROOFSTEP]
simp only [sub_eq_add_neg] at h ⊢
[GOAL]
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y + -z ≠ 0
⊢ x ^ (y + -z) = x ^ y / x ^ z
[PROOFSTEP]
simp only [rpow_add' hx h, rpow_neg hx, div_eq_mul_inv]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ ↑y
[PROOFSTEP]
simp only [Real.rpow_def_of_nonneg hx, Complex.cpow_def, ofReal_eq_zero]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y)) =
    if x = 0 then if y = 0 then 1 else 0 else exp (log ↑x * ↑y)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : y = 0
⊢ ↑1 = 1
[PROOFSTEP]
simp [Complex.ofReal_log hx]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ ↑0 = 0
[PROOFSTEP]
simp [Complex.ofReal_log hx]
[GOAL]
case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ ↑(Real.exp (Real.log x * y)) = exp (log ↑x * ↑y)
[PROOFSTEP]
simp [Complex.ofReal_log hx]
[GOAL]
x : ℝ
hx : x ≤ 0
y : ℂ
⊢ ↑x ^ y = (-↑x) ^ y * exp (↑π * I * y)
[PROOFSTEP]
rcases hx.eq_or_lt with (rfl | hlt)
[GOAL]
case inl
y : ℂ
hx : 0 ≤ 0
⊢ ↑0 ^ y = (-↑0) ^ y * exp (↑π * I * y)
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inl.inl
hx : 0 ≤ 0
⊢ ↑0 ^ 0 = (-↑0) ^ 0 * exp (↑π * I * 0)
[PROOFSTEP]
simp [*]
[GOAL]
case inl.inr
y : ℂ
hx : 0 ≤ 0
hy : y ≠ 0
⊢ ↑0 ^ y = (-↑0) ^ y * exp (↑π * I * y)
[PROOFSTEP]
simp [*]
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ ↑x ^ y = (-↑x) ^ y * exp (↑π * I * y)
[PROOFSTEP]
have hne : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr hlt.ne
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ ↑x ^ y = (-↑x) ^ y * exp (↑π * I * y)
[PROOFSTEP]
rw [cpow_def_of_ne_zero hne, cpow_def_of_ne_zero (neg_ne_zero.2 hne), ← exp_add, ← add_mul, log, log, abs.map_neg,
  arg_ofReal_of_neg hlt, ← ofReal_neg, arg_ofReal_of_nonneg (neg_nonneg.2 hx), ofReal_zero, zero_mul, add_zero]
[GOAL]
z : ℂ
hz : z ≠ 0
w : ℂ
⊢ ↑abs (z ^ w) = ↑abs z ^ w.re / Real.exp (arg z * w.im)
[PROOFSTEP]
rw [cpow_def_of_ne_zero hz, abs_exp, mul_re, log_re, log_im, Real.exp_sub, Real.rpow_def_of_pos (abs.pos hz)]
[GOAL]
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ↑abs (z ^ w) = ↑abs z ^ w.re / Real.exp (arg z * w.im)
[PROOFSTEP]
rcases ne_or_eq z 0 with (hz | rfl) <;> [exact abs_cpow_of_ne_zero hz w; rw [map_zero]]
[GOAL]
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ↑abs (z ^ w) = ↑abs z ^ w.re / Real.exp (arg z * w.im)
[PROOFSTEP]
rcases ne_or_eq z 0 with (hz | rfl)
[GOAL]
case inl
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
hz : z ≠ 0
⊢ ↑abs (z ^ w) = ↑abs z ^ w.re / Real.exp (arg z * w.im)
[PROOFSTEP]
exact abs_cpow_of_ne_zero hz w
[GOAL]
case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ↑abs (0 ^ w) = ↑abs 0 ^ w.re / Real.exp (arg 0 * w.im)
[PROOFSTEP]
rw [map_zero]
[GOAL]
case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)
[PROOFSTEP]
cases' eq_or_ne w.re 0 with hw hw
[GOAL]
case inr.inl
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)
[PROOFSTEP]
simp [hw, h rfl hw]
[GOAL]
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)
[PROOFSTEP]
rw [Real.zero_rpow hw, zero_div, zero_cpow, map_zero]
[GOAL]
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0
[PROOFSTEP]
exact ne_of_apply_ne re hw
[GOAL]
z w : ℂ
⊢ ↑abs (z ^ w) ≤ ↑abs z ^ w.re / Real.exp (arg z * w.im)
[PROOFSTEP]
rcases ne_or_eq z 0 with (hz | rfl) <;> [exact (abs_cpow_of_ne_zero hz w).le; rw [map_zero]]
[GOAL]
z w : ℂ
⊢ ↑abs (z ^ w) ≤ ↑abs z ^ w.re / Real.exp (arg z * w.im)
[PROOFSTEP]
rcases ne_or_eq z 0 with (hz | rfl)
[GOAL]
case inl
z w : ℂ
hz : z ≠ 0
⊢ ↑abs (z ^ w) ≤ ↑abs z ^ w.re / Real.exp (arg z * w.im)
[PROOFSTEP]
exact (abs_cpow_of_ne_zero hz w).le
[GOAL]
case inr
w : ℂ
⊢ ↑abs (0 ^ w) ≤ ↑abs 0 ^ w.re / Real.exp (arg 0 * w.im)
[PROOFSTEP]
rw [map_zero]
[GOAL]
case inr
w : ℂ
⊢ ↑abs (0 ^ w) ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
[PROOFSTEP]
rcases eq_or_ne w 0 with (rfl | hw)
[GOAL]
case inr.inl
⊢ ↑abs (0 ^ 0) ≤ 0 ^ 0.re / Real.exp (arg 0 * 0.im)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
w : ℂ
hw : w ≠ 0
⊢ ↑abs (0 ^ w) ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
[PROOFSTEP]
rw [zero_cpow hw, map_zero]
[GOAL]
case inr.inr
w : ℂ
hw : w ≠ 0
⊢ 0 ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
[PROOFSTEP]
exact div_nonneg (Real.rpow_nonneg_of_nonneg le_rfl _) (Real.exp_pos _).le
[GOAL]
x : ℂ
y : ℝ
⊢ ↑abs (x ^ ↑y) = ↑abs x ^ y
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx) <;> [rcases eq_or_ne y 0 with (rfl | hy); skip]
[GOAL]
x : ℂ
y : ℝ
⊢ ↑abs (x ^ ↑y) = ↑abs x ^ y
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
y : ℝ
⊢ ↑abs (0 ^ ↑y) = ↑abs 0 ^ y
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑abs (x ^ ↑y) = ↑abs x ^ y
[PROOFSTEP]
skip
[GOAL]
case inl.inl
⊢ ↑abs (0 ^ ↑0) = ↑abs 0 ^ 0
[PROOFSTEP]
simp [*, abs_cpow_of_ne_zero]
[GOAL]
case inl.inr
y : ℝ
hy : y ≠ 0
⊢ ↑abs (0 ^ ↑y) = ↑abs 0 ^ y
[PROOFSTEP]
simp [*, abs_cpow_of_ne_zero]
[GOAL]
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑abs (x ^ ↑y) = ↑abs x ^ y
[PROOFSTEP]
simp [*, abs_cpow_of_ne_zero]
[GOAL]
x : ℂ
n : ℕ
⊢ ↑abs (x ^ (↑n)⁻¹) = ↑abs x ^ (↑n)⁻¹
[PROOFSTEP]
rw [← abs_cpow_real]
[GOAL]
x : ℂ
n : ℕ
⊢ ↑abs (x ^ (↑n)⁻¹) = ↑abs (x ^ ↑(↑n)⁻¹)
[PROOFSTEP]
simp [-abs_cpow_real]
[GOAL]
x : ℝ
hx : 0 < x
y : ℂ
⊢ ↑abs (↑x ^ y) = x ^ y.re
[PROOFSTEP]
rw [abs_cpow_of_ne_zero (ofReal_ne_zero.mpr hx.ne'), arg_ofReal_of_nonneg hx.le, zero_mul, Real.exp_zero, div_one,
  abs_of_nonneg hx.le]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ↑abs (↑x ^ y) = x ^ y.re
[PROOFSTEP]
rcases hx.eq_or_lt with (rfl | hlt)
[GOAL]
case inl
y : ℂ
hy : y.re ≠ 0
hx : 0 ≤ 0
⊢ ↑abs (↑0 ^ y) = 0 ^ y.re
[PROOFSTEP]
rw [ofReal_zero, zero_cpow, map_zero, Real.zero_rpow hy]
[GOAL]
case inl
y : ℂ
hy : y.re ≠ 0
hx : 0 ≤ 0
⊢ y ≠ 0
[PROOFSTEP]
exact ne_of_apply_ne re hy
[GOAL]
case inr
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
hlt : 0 < x
⊢ ↑abs (↑x ^ y) = x ^ y.re
[PROOFSTEP]
exact abs_cpow_eq_rpow_re_of_pos hlt y
[GOAL]
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z
[PROOFSTEP]
rw [← Complex.ofReal_inj, Complex.ofReal_cpow (rpow_nonneg_of_nonneg hx _), Complex.ofReal_cpow hx, Complex.ofReal_mul,
  Complex.cpow_mul, Complex.ofReal_cpow hx]
[GOAL]
case h₁
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ -π < (Complex.log ↑x * ↑y).im
[PROOFSTEP]
simp only [(Complex.ofReal_mul _ _).symm, (Complex.ofReal_log hx).symm, Complex.ofReal_im, neg_lt_zero, pi_pos,
  le_of_lt pi_pos]
[GOAL]
case h₂
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ (Complex.log ↑x * ↑y).im ≤ π
[PROOFSTEP]
simp only [(Complex.ofReal_mul _ _).symm, (Complex.ofReal_log hx).symm, Complex.ofReal_im, neg_lt_zero, pi_pos,
  le_of_lt pi_pos]
[GOAL]
x✝ y✝ z x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n
[PROOFSTEP]
rw [rpow_def, rpow_def, Complex.ofReal_add, Complex.cpow_add _ _ (Complex.ofReal_ne_zero.mpr hx),
  Complex.ofReal_int_cast, Complex.cpow_int_cast, ← Complex.ofReal_zpow, mul_comm, Complex.ofReal_mul_re, mul_comm]
[GOAL]
x✝ y✝ z x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n
[PROOFSTEP]
simpa using rpow_add_int hx y n
[GOAL]
x✝ y✝ z x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n
[PROOFSTEP]
simpa using rpow_add_int hx y (-n)
[GOAL]
x✝ y✝ z x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n
[PROOFSTEP]
simpa using rpow_sub_int hx y n
[GOAL]
x✝ y✝ z x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x
[PROOFSTEP]
simpa using rpow_add_nat hx y 1
[GOAL]
x✝ y✝ z x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x
[PROOFSTEP]
simpa using rpow_sub_nat hx y 1
[GOAL]
x✝ y z x : ℝ
n : ℤ
⊢ x ^ ↑n = x ^ n
[PROOFSTEP]
simp only [rpow_def, ← Complex.ofReal_zpow, Complex.cpow_int_cast, Complex.ofReal_int_cast, Complex.ofReal_re]
[GOAL]
x✝ y z x : ℝ
n : ℕ
⊢ x ^ ↑n = x ^ n
[PROOFSTEP]
simpa using rpow_int_cast x n
[GOAL]
x✝ y z x : ℝ
⊢ x ^ 2 = x ^ 2
[PROOFSTEP]
rw [← rpow_nat_cast]
[GOAL]
x✝ y z x : ℝ
⊢ x ^ 2 = x ^ ↑2
[PROOFSTEP]
simp only [Nat.cast_ofNat]
[GOAL]
x✝ y z x : ℝ
⊢ x ^ (-1) = x⁻¹
[PROOFSTEP]
suffices H : x ^ ((-1 : ℤ) : ℝ) = x⁻¹
[GOAL]
x✝ y z x : ℝ
H : x ^ ↑(-1) = x⁻¹
⊢ x ^ (-1) = x⁻¹
[PROOFSTEP]
rwa [Int.cast_neg, Int.cast_one] at H 
[GOAL]
case H
x✝ y z x : ℝ
⊢ x ^ ↑(-1) = x⁻¹
[PROOFSTEP]
simp only [rpow_int_cast, zpow_one, zpow_neg]
[GOAL]
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ (x * y) ^ z = x ^ z * y ^ z
[PROOFSTEP]
iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all
[GOAL]
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ (x * y) ^ z = x ^ z * y ^ z
[PROOFSTEP]
rw [Real.rpow_def_of_nonneg]
[GOAL]
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ (if x * y = 0 then if z = 0 then 1 else 0 else exp (log (x * y) * z)) = x ^ z * y ^ z
[PROOFSTEP]
split_ifs with h_ifs
[GOAL]
case pos
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x * y = 0
h✝ : z = 0
⊢ 1 = x ^ z * y ^ z
[PROOFSTEP]
simp_all
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x * y = 0
h✝ : ¬z = 0
⊢ 0 = x ^ z * y ^ z
[PROOFSTEP]
simp_all
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x * y = 0
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
[PROOFSTEP]
simp_all
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ x ^ z = 0 ∨ y ^ z = 0
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬(x = 0 ∨ y = 0)
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
case hx x✝ y✝ z✝ x y z : ℝ h : 0 ≤ x h₁ : 0 ≤ y ⊢ 0 ≤ x * y
[PROOFSTEP]
rw [Real.rpow_def_of_nonneg]
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ (if x = 0 then if z = 0 then 1 else 0 else exp (log x * z)) = 0 ∨ y ^ z = 0
[PROOFSTEP]
split_ifs with h_ifs
[GOAL]
case pos
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs✝ : x = 0 ∨ y = 0
h✝ : ¬z = 0
h_ifs : x = 0
⊢ 0 = 0 ∨ y ^ z = 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs✝ : x = 0 ∨ y = 0
h✝ : ¬z = 0
h_ifs : ¬x = 0
⊢ exp (log x * z) = 0 ∨ y ^ z = 0
[PROOFSTEP]
simp_all
[GOAL]
case neg.hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : x = 0 ∨ y = 0
h✝ : ¬z = 0
⊢ 0 ≤ x
[PROOFSTEP]
exact h
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬(x = 0 ∨ y = 0)
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
[PROOFSTEP]
rw [not_or] at h_ifs 
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
[PROOFSTEP]
have hx : 0 < x := by
  cases' lt_or_eq_of_le h with h₂ h₂
  · exact h₂
  exfalso
  apply h_ifs.1
  exact Eq.symm h₂
[GOAL]
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 < x
[PROOFSTEP]
cases' lt_or_eq_of_le h with h₂ h₂
[GOAL]
case inl
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 < x
⊢ 0 < x
[PROOFSTEP]
exact h₂
[GOAL]
case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ 0 < x
[PROOFSTEP]
exfalso
[GOAL]
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ False
[PROOFSTEP]
apply h_ifs.1
[GOAL]
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
h₂ : 0 = x
⊢ x = 0
[PROOFSTEP]
exact Eq.symm h₂
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
[PROOFSTEP]
have hy : 0 < y := by
  cases' lt_or_eq_of_le h₁ with h₂ h₂
  · exact h₂
  exfalso
  apply h_ifs.2
  exact Eq.symm h₂
[GOAL]
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
⊢ 0 < y
[PROOFSTEP]
cases' lt_or_eq_of_le h₁ with h₂ h₂
[GOAL]
case inl
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 < y
⊢ 0 < y
[PROOFSTEP]
exact h₂
[GOAL]
case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ 0 < y
[PROOFSTEP]
exfalso
[GOAL]
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ False
[PROOFSTEP]
apply h_ifs.2
[GOAL]
case inr.h
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
h₂ : 0 = y
⊢ y = 0
[PROOFSTEP]
exact Eq.symm h₂
[GOAL]
case neg
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
hx : 0 < x
hy : 0 < y
⊢ exp (log (x * y) * z) = x ^ z * y ^ z
[PROOFSTEP]
rw [log_mul (ne_of_gt hx) (ne_of_gt hy), add_mul, exp_add, rpow_def_of_pos hx, rpow_def_of_pos hy]
[GOAL]
case hx
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : 0 ≤ y
⊢ 0 ≤ x * y
[PROOFSTEP]
exact mul_nonneg h h₁
[GOAL]
x y✝ z : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
[PROOFSTEP]
simp only [← rpow_neg_one, ← rpow_mul hx, mul_comm]
[GOAL]
x y z✝ : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
z : ℝ
⊢ (x / y) ^ z = x ^ z / y ^ z
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_rpow hx (inv_nonneg.2 hy), inv_rpow hy]
[GOAL]
x✝ y✝ z x : ℝ
hx : 0 < x
y : ℝ
⊢ log (x ^ y) = y * log x
[PROOFSTEP]
apply exp_injective
[GOAL]
case a
x✝ y✝ z x : ℝ
hx : 0 < x
y : ℝ
⊢ exp (log (x ^ y)) = exp (y * log x)
[PROOFSTEP]
rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]
[GOAL]
x y z : ℝ
hx : 0 ≤ x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
[PROOFSTEP]
rw [le_iff_eq_or_lt] at hx 
[GOAL]
x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z
[PROOFSTEP]
rw [← hx, zero_rpow (ne_of_gt hz)]
[GOAL]
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z
[PROOFSTEP]
exact rpow_pos_of_pos (by rwa [← hx] at hxy ) _
[GOAL]
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y
[PROOFSTEP]
rwa [← hx] at hxy 
[GOAL]
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z
[PROOFSTEP]
rw [rpow_def_of_pos hx, rpow_def_of_pos (lt_trans hx hxy), exp_lt_exp]
[GOAL]
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ log x * z < log y * z
[PROOFSTEP]
exact mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz
[GOAL]
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
⊢ x ^ z ≤ y ^ z
[PROOFSTEP]
rcases eq_or_lt_of_le h₁ with (rfl | h₁')
[GOAL]
case inl
x✝ y z✝ x z : ℝ
h : 0 ≤ x
h₂ : 0 ≤ z
h₁ : x ≤ x
⊢ x ^ z ≤ x ^ z
[PROOFSTEP]
rfl
[GOAL]
case inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
⊢ x ^ z ≤ y ^ z
[PROOFSTEP]
rcases eq_or_lt_of_le h₂ with (rfl | h₂')
[GOAL]
case inr.inl
x✝ y✝ z x y : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₁' : x < y
h₂ : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
x✝ y✝ z✝ x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
h₂' : 0 < z
⊢ x ^ z ≤ y ^ z
[PROOFSTEP]
exact le_of_lt (rpow_lt_rpow h h₁' h₂')
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
[PROOFSTEP]
have hz' : 0 < -z := by rwa [lt_neg, neg_zero]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < -z
[PROOFSTEP]
rwa [lt_neg, neg_zero]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
[PROOFSTEP]
have hxz : 0 < x ^ (-z) := Real.rpow_pos_of_pos hx _
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
[PROOFSTEP]
have hyz : 0 < y ^ z⁻¹ := Real.rpow_pos_of_pos hy _
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
[PROOFSTEP]
rw [← Real.rpow_le_rpow_iff hx.le hyz.le hz', ← Real.rpow_mul hy.le]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ^ (-z) ≤ y ^ (z⁻¹ * -z) ↔ y ≤ x ^ z
[PROOFSTEP]
simp only [ne_of_lt hz, Real.rpow_neg_one, mul_neg, inv_mul_cancel, Ne.def, not_false_iff]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ^ (-z) ≤ y⁻¹ ↔ y ≤ x ^ z
[PROOFSTEP]
rw [le_inv hxz hy, ← Real.rpow_neg_one, ← Real.rpow_mul hx.le]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ y ≤ x ^ (-z * -1) ↔ y ≤ x ^ z
[PROOFSTEP]
simp
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x < y ^ z⁻¹ ↔ y < x ^ z
[PROOFSTEP]
have hz' : 0 < -z := by rwa [lt_neg, neg_zero]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < -z
[PROOFSTEP]
rwa [lt_neg, neg_zero]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
⊢ x < y ^ z⁻¹ ↔ y < x ^ z
[PROOFSTEP]
have hxz : 0 < x ^ (-z) := Real.rpow_pos_of_pos hx _
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
⊢ x < y ^ z⁻¹ ↔ y < x ^ z
[PROOFSTEP]
have hyz : 0 < y ^ z⁻¹ := Real.rpow_pos_of_pos hy _
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x < y ^ z⁻¹ ↔ y < x ^ z
[PROOFSTEP]
rw [← Real.rpow_lt_rpow_iff hx.le hyz.le hz', ← Real.rpow_mul hy.le]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ^ (-z) < y ^ (z⁻¹ * -z) ↔ y < x ^ z
[PROOFSTEP]
simp only [ne_of_lt hz, Real.rpow_neg_one, mul_neg, inv_mul_cancel, Ne.def, not_false_iff]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ^ (-z) < y⁻¹ ↔ y < x ^ z
[PROOFSTEP]
rw [lt_inv hxz hy, ← Real.rpow_neg_one, ← Real.rpow_mul hx.le]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ y < x ^ (-z * -1) ↔ y < x ^ z
[PROOFSTEP]
simp
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ < y ↔ y ^ z < x
[PROOFSTEP]
convert lt_rpow_inv_iff_of_neg (Real.rpow_pos_of_pos hx z⁻¹) (Real.rpow_pos_of_pos hy z) hz
[GOAL]
case h.e'_1.h.e'_4
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ y = (y ^ z) ^ z⁻¹
[PROOFSTEP]
simp [← Real.rpow_mul hx.le, ← Real.rpow_mul hy.le, ne_of_lt hz]
[GOAL]
case h.e'_2.h.e'_4
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x = (x ^ z⁻¹) ^ z
[PROOFSTEP]
simp [← Real.rpow_mul hx.le, ← Real.rpow_mul hy.le, ne_of_lt hz]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x
[PROOFSTEP]
convert le_rpow_inv_iff_of_neg (Real.rpow_pos_of_pos hx z⁻¹) (Real.rpow_pos_of_pos hy z) hz
[GOAL]
case h.e'_1.h.e'_4
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ y = (y ^ z) ^ z⁻¹
[PROOFSTEP]
simp [← Real.rpow_mul hx.le, ← Real.rpow_mul hy.le, ne_of_lt hz]
[GOAL]
case h.e'_2.h.e'_4
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x = (x ^ z⁻¹) ^ z
[PROOFSTEP]
simp [← Real.rpow_mul hx.le, ← Real.rpow_mul hy.le, ne_of_lt hz]
[GOAL]
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z
[PROOFSTEP]
repeat' rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
[GOAL]
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z
[PROOFSTEP]
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
[GOAL]
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ exp (log x * y) < x ^ z
[PROOFSTEP]
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
[GOAL]
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ exp (log x * y) < exp (log x * z)
[PROOFSTEP]
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
[GOAL]
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ exp (log x * y) < exp (log x * z)
[PROOFSTEP]
rw [exp_lt_exp]
[GOAL]
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z
[PROOFSTEP]
exact mul_lt_mul_of_pos_left hyz (log_pos hx)
[GOAL]
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z
[PROOFSTEP]
repeat' rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
[GOAL]
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z
[PROOFSTEP]
rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
[GOAL]
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ exp (log x * y) ≤ x ^ z
[PROOFSTEP]
rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
[GOAL]
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ exp (log x * y) ≤ exp (log x * z)
[PROOFSTEP]
rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
[GOAL]
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ exp (log x * y) ≤ exp (log x * z)
[PROOFSTEP]
rw [exp_le_exp]
[GOAL]
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left hyz (log_nonneg hx)
[GOAL]
x✝ y✝ z✝ x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
⊢ x ^ z < y ^ z
[PROOFSTEP]
have hx : 0 < x := hy.trans hxy
[GOAL]
x✝ y✝ z✝ x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
hx : 0 < x
⊢ x ^ z < y ^ z
[PROOFSTEP]
rw [← neg_neg z, Real.rpow_neg (le_of_lt hx) (-z), Real.rpow_neg (le_of_lt hy) (-z),
  inv_lt_inv (rpow_pos_of_pos hx _) (rpow_pos_of_pos hy _)]
[GOAL]
x✝ y✝ z✝ x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
hx : 0 < x
⊢ y ^ (-z) < x ^ (-z)
[PROOFSTEP]
exact Real.rpow_lt_rpow (by positivity) hxy <| neg_pos_of_neg hz
[GOAL]
x✝ y✝ z✝ x y z : ℝ
hy : 0 < y
hxy : y < x
hz : z < 0
hx : 0 < x
⊢ 0 ≤ y
[PROOFSTEP]
positivity
[GOAL]
x✝ y✝ z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ y ^ z
[PROOFSTEP]
rcases ne_or_eq z 0 with hz_zero | rfl
[GOAL]
case inl
x✝ y✝ z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
⊢ x ^ z ≤ y ^ z
case inr x✝ y✝ x y : ℝ hy : 0 < y hxy : y ≤ x hz : 0 ≤ 0 ⊢ x ^ 0 ≤ y ^ 0
[PROOFSTEP]
case inl =>
  rcases ne_or_eq x y with hxy' | rfl
  case inl =>
    exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy) (Ne.lt_of_le hz_zero hz)
  case inr => simp
[GOAL]
x✝ y✝ z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
⊢ x ^ z ≤ y ^ z
[PROOFSTEP]
case inl =>
  rcases ne_or_eq x y with hxy' | rfl
  case inl =>
    exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy) (Ne.lt_of_le hz_zero hz)
  case inr => simp
[GOAL]
x✝ y✝ z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
⊢ x ^ z ≤ y ^ z
[PROOFSTEP]
rcases ne_or_eq x y with hxy' | rfl
[GOAL]
case inl
x✝ y✝ z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
hxy' : x ≠ y
⊢ x ^ z ≤ y ^ z
case inr x✝ y z x : ℝ hz : z ≤ 0 hz_zero : z ≠ 0 hy : 0 < x hxy : x ≤ x ⊢ x ^ z ≤ x ^ z
[PROOFSTEP]
case inl =>
  exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy) (Ne.lt_of_le hz_zero hz)
[GOAL]
x✝ y✝ z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
hxy' : x ≠ y
⊢ x ^ z ≤ y ^ z
[PROOFSTEP]
case inl =>
  exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy) (Ne.lt_of_le hz_zero hz)
[GOAL]
x✝ y✝ z x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : z ≤ 0
hz_zero : z ≠ 0
hxy' : x ≠ y
⊢ x ^ z ≤ y ^ z
[PROOFSTEP]
exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy) (Ne.lt_of_le hz_zero hz)
[GOAL]
case inr
x✝ y z x : ℝ
hz : z ≤ 0
hz_zero : z ≠ 0
hy : 0 < x
hxy : x ≤ x
⊢ x ^ z ≤ x ^ z
[PROOFSTEP]
case inr => simp
[GOAL]
x✝ y z x : ℝ
hz : z ≤ 0
hz_zero : z ≠ 0
hy : 0 < x
hxy : x ≤ x
⊢ x ^ z ≤ x ^ z
[PROOFSTEP]
case inr => simp
[GOAL]
x✝ y z x : ℝ
hz : z ≤ 0
hz_zero : z ≠ 0
hy : 0 < x
hxy : x ≤ x
⊢ x ^ z ≤ x ^ z
[PROOFSTEP]
simp
[GOAL]
case inr
x✝ y✝ x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0
[PROOFSTEP]
case inr => simp
[GOAL]
x✝ y✝ x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0
[PROOFSTEP]
case inr => simp
[GOAL]
x✝ y✝ x y : ℝ
hy : 0 < y
hxy : y ≤ x
hz : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0
[PROOFSTEP]
simp
[GOAL]
x y z : ℝ
hx : 1 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
[PROOFSTEP]
have x_pos : 0 < x := lt_trans zero_lt_one hx
[GOAL]
x y z : ℝ
hx : 1 < x
x_pos : 0 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
[PROOFSTEP]
rw [← log_le_log (rpow_pos_of_pos x_pos y) (rpow_pos_of_pos x_pos z), log_rpow x_pos, log_rpow x_pos,
  mul_le_mul_right (log_pos hx)]
[GOAL]
x y z : ℝ
hx : 1 < x
⊢ x ^ y < x ^ z ↔ y < z
[PROOFSTEP]
rw [lt_iff_not_le, rpow_le_rpow_left_iff hx, lt_iff_not_le]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z
[PROOFSTEP]
repeat' rw [rpow_def_of_pos hx0]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z
[PROOFSTEP]
rw [rpow_def_of_pos hx0]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ exp (log x * y) < x ^ z
[PROOFSTEP]
rw [rpow_def_of_pos hx0]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ exp (log x * y) < exp (log x * z)
[PROOFSTEP]
rw [rpow_def_of_pos hx0]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ exp (log x * y) < exp (log x * z)
[PROOFSTEP]
rw [exp_lt_exp]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z
[PROOFSTEP]
exact mul_lt_mul_of_neg_left hyz (log_neg hx0 hx1)
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z
[PROOFSTEP]
repeat' rw [rpow_def_of_pos hx0]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z
[PROOFSTEP]
rw [rpow_def_of_pos hx0]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ exp (log x * y) ≤ x ^ z
[PROOFSTEP]
rw [rpow_def_of_pos hx0]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ exp (log x * y) ≤ exp (log x * z)
[PROOFSTEP]
rw [rpow_def_of_pos hx0]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ exp (log x * y) ≤ exp (log x * z)
[PROOFSTEP]
rw [exp_le_exp]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z
[PROOFSTEP]
exact mul_le_mul_of_nonpos_left hyz (log_nonpos (le_of_lt hx0) hx1)
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y ≤ x ^ z ↔ z ≤ y
[PROOFSTEP]
rw [← log_le_log (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z), log_rpow hx0, log_rpow hx0,
  mul_le_mul_right_of_neg (log_neg hx0 hx1)]
[GOAL]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y < x ^ z ↔ z < y
[PROOFSTEP]
rw [lt_iff_not_le, rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1, lt_iff_not_le]
[GOAL]
x✝ y z✝ x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1
[PROOFSTEP]
rw [← one_rpow z]
[GOAL]
x✝ y z✝ x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1 ^ z
[PROOFSTEP]
exact rpow_lt_rpow hx1 hx2 hz
[GOAL]
x✝ y z✝ x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1
[PROOFSTEP]
rw [← one_rpow z]
[GOAL]
x✝ y z✝ x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1 ^ z
[PROOFSTEP]
exact rpow_le_rpow hx1 hx2 hz
[GOAL]
x✝ y z✝ x z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1
[PROOFSTEP]
convert rpow_lt_rpow_of_exponent_lt hx hz
[GOAL]
case h.e'_4
x✝ y z✝ x z : ℝ
hx : 1 < x
hz : z < 0
⊢ 1 = x ^ 0
[PROOFSTEP]
exact (rpow_zero x).symm
[GOAL]
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ 1
[PROOFSTEP]
convert rpow_le_rpow_of_exponent_le hx hz
[GOAL]
case h.e'_4
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ 1 = x ^ 0
[PROOFSTEP]
exact (rpow_zero x).symm
[GOAL]
x✝ y z✝ x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z
[PROOFSTEP]
rw [← one_rpow z]
[GOAL]
x✝ y z✝ x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 ^ z < x ^ z
[PROOFSTEP]
exact rpow_lt_rpow zero_le_one hx hz
[GOAL]
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ≤ x ^ z
[PROOFSTEP]
rw [← one_rpow z]
[GOAL]
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ^ z ≤ x ^ z
[PROOFSTEP]
exact rpow_le_rpow zero_le_one hx hz
[GOAL]
x y z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 < x ^ z
[PROOFSTEP]
convert rpow_lt_rpow_of_exponent_gt hx1 hx2 hz
[GOAL]
case h.e'_3
x y z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 = x ^ 0
[PROOFSTEP]
exact (rpow_zero x).symm
[GOAL]
x y z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 ≤ x ^ z
[PROOFSTEP]
convert rpow_le_rpow_of_exponent_ge hx1 hx2 hz
[GOAL]
case h.e'_3
x y z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 = x ^ 0
[PROOFSTEP]
exact (rpow_zero x).symm
[GOAL]
x y z : ℝ
hx : 0 < x
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
[PROOFSTEP]
rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx, log_neg_iff hx]
[GOAL]
x y z : ℝ
hx : 0 ≤ x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
[PROOFSTEP]
rcases hx.eq_or_lt with (rfl | hx)
[GOAL]
case inl
y z : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y
[PROOFSTEP]
rcases _root_.em (y = 0) with (rfl | hy)
[GOAL]
case inl.inl
z : ℝ
hx : 0 ≤ 0
⊢ 0 ^ 0 < 1 ↔ 0 = 0 ∧ 0 ≠ 0 ∨ 1 < 0 ∧ 0 < 0 ∨ 0 < 1 ∧ 0 < 0
[PROOFSTEP]
simp [*, lt_irrefl, zero_lt_one]
[GOAL]
case inl.inr
y z : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y
[PROOFSTEP]
simp [*, lt_irrefl, zero_lt_one]
[GOAL]
case inr
x y z : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
[PROOFSTEP]
simp [rpow_lt_one_iff_of_pos hx, hx.ne.symm]
[GOAL]
x y z : ℝ
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
[PROOFSTEP]
rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx, log_neg_iff hx]
[GOAL]
x y z : ℝ
hx : 0 ≤ x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
[PROOFSTEP]
rcases hx.eq_or_lt with (rfl | hx)
[GOAL]
case inl
y z : ℝ
hx : 0 ≤ 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0
[PROOFSTEP]
rcases _root_.em (y = 0) with (rfl | hy)
[GOAL]
case inl.inl
z : ℝ
hx : 0 ≤ 0
⊢ 1 < 0 ^ 0 ↔ 1 < 0 ∧ 0 < 0 ∨ 0 < 0 ∧ 0 < 1 ∧ 0 < 0
[PROOFSTEP]
simp [*, lt_irrefl, (zero_lt_one' ℝ).not_lt]
[GOAL]
case inl.inr
y z : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0
[PROOFSTEP]
simp [*, lt_irrefl, (zero_lt_one' ℝ).not_lt]
[GOAL]
case inr
x y z : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
[PROOFSTEP]
simp [one_lt_rpow_iff_of_pos hx, hx]
[GOAL]
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hz : 0 ≤ z
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z
[PROOFSTEP]
rcases eq_or_lt_of_le hx0 with (rfl | hx0')
[GOAL]
case inl
y z : ℝ
hz : 0 ≤ z
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
⊢ 0 ^ y ≤ 0 ^ z
[PROOFSTEP]
rcases eq_or_lt_of_le hz with (rfl | hz')
[GOAL]
case inl.inl
y : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hz : 0 ≤ 0
hyz : 0 ≤ y
⊢ 0 ^ y ≤ 0 ^ 0
[PROOFSTEP]
exact (rpow_zero 0).symm ▸ rpow_le_one hx0 hx1 hyz
[GOAL]
case inl.inr
y z : ℝ
hz : 0 ≤ z
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hz' : 0 < z
⊢ 0 ^ y ≤ 0 ^ z
[PROOFSTEP]
rw [zero_rpow, zero_rpow]
[GOAL]
case inl.inr
y z : ℝ
hz : 0 ≤ z
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hz' : 0 < z
⊢ z ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case inl.inr
y z : ℝ
hz : 0 ≤ z
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hz' : 0 < z
⊢ y ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hz : 0 ≤ z
hyz : z ≤ y
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z
[PROOFSTEP]
exact rpow_le_rpow_of_exponent_ge hx0' hx1 hyz
[GOAL]
x✝ y z x : ℝ
hx : x ≠ 0
⊢ InjOn (fun y => y ^ x) {y | 0 ≤ y}
[PROOFSTEP]
rintro y hy z hz (hyz : y ^ x = z ^ x)
[GOAL]
x✝ y✝ z✝ x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y = z
[PROOFSTEP]
rw [← rpow_one y, ← rpow_one z, ← _root_.mul_inv_cancel hx, rpow_mul hy, rpow_mul hz, hyz]
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x ≤ y ^ z ↔ log x ≤ z * log y
[PROOFSTEP]
rw [← Real.log_le_log hx (Real.rpow_pos_of_pos hy z), Real.log_rpow hy]
[GOAL]
x y z : ℝ
hx : 0 ≤ x
hy : 0 < y
h : log x ≤ z * log y
⊢ x ≤ y ^ z
[PROOFSTEP]
obtain hx | rfl := hx.lt_or_eq
[GOAL]
case inl
x y z : ℝ
hx✝ : 0 ≤ x
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z
[PROOFSTEP]
exact (le_rpow_iff_log_le hx hy).2 h
[GOAL]
case inr
y z : ℝ
hy : 0 < y
hx : 0 ≤ 0
h : log 0 ≤ z * log y
⊢ 0 ≤ y ^ z
[PROOFSTEP]
exact (Real.rpow_pos_of_pos hy z).le
[GOAL]
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < y ^ z ↔ log x < z * log y
[PROOFSTEP]
rw [← Real.log_lt_log_iff hx (Real.rpow_pos_of_pos hy z), Real.log_rpow hy]
[GOAL]
x y z : ℝ
hx : 0 ≤ x
hy : 0 < y
h : log x < z * log y
⊢ x < y ^ z
[PROOFSTEP]
obtain hx | rfl := hx.lt_or_eq
[GOAL]
case inl
x y z : ℝ
hx✝ : 0 ≤ x
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z
[PROOFSTEP]
exact (lt_rpow_iff_log_lt hx hy).2 h
[GOAL]
case inr
y z : ℝ
hy : 0 < y
hx : 0 ≤ 0
h : log 0 < z * log y
⊢ 0 < y ^ z
[PROOFSTEP]
exact Real.rpow_pos_of_pos hy z
[GOAL]
x y z : ℝ
hx : 0 < x
⊢ x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y
[PROOFSTEP]
rw [rpow_def_of_pos hx, exp_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx]
[GOAL]
x✝ y z x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| < 1 / t
[PROOFSTEP]
rw [lt_div_iff ht]
[GOAL]
x✝ y z x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| * t < 1
[PROOFSTEP]
have := abs_log_mul_self_lt (x ^ t) (rpow_pos_of_pos h1 t) (rpow_le_one h1.le h2 ht.le)
[GOAL]
x✝ y z x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
⊢ |log x * x ^ t| * t < 1
[PROOFSTEP]
rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this 
[GOAL]
x✝ y z x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x
[PROOFSTEP]
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
[GOAL]
x✝ y z x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x
[PROOFSTEP]
rw [← rpow_nat_cast, ← rpow_mul hx, mul_inv_cancel hn0, rpow_one]
[GOAL]
x✝ y z x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
[PROOFSTEP]
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
[GOAL]
x✝ y z x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
[PROOFSTEP]
rw [← rpow_nat_cast, ← rpow_mul hx, inv_mul_cancel hn0, rpow_one]
[GOAL]
x y z b : ℝ
hb : 1 < b
⊢ StrictMono (rpow b)
[PROOFSTEP]
show StrictMono (fun (x : ℝ) => b ^ x)
[GOAL]
x y z b : ℝ
hb : 1 < b
⊢ StrictMono fun x => b ^ x
[PROOFSTEP]
simp_rw [Real.rpow_def_of_pos (zero_lt_one.trans hb)]
[GOAL]
x y z b : ℝ
hb : 1 < b
⊢ StrictMono fun x => exp (log b * x)
[PROOFSTEP]
exact exp_strictMono.comp <| StrictMono.const_mul strictMono_id <| Real.log_pos hb
[GOAL]
x y z b : ℝ
hb : 1 ≤ b
⊢ Monotone (rpow b)
[PROOFSTEP]
rcases lt_or_eq_of_le hb with hb | rfl
[GOAL]
case inl
x y z b : ℝ
hb✝ : 1 ≤ b
hb : 1 < b
⊢ Monotone (rpow b)
case inr x y z : ℝ hb : 1 ≤ 1 ⊢ Monotone (rpow 1)
[PROOFSTEP]
case inl => exact (strictMono_rpow_of_base_gt_one hb).monotone
[GOAL]
x y z b : ℝ
hb✝ : 1 ≤ b
hb : 1 < b
⊢ Monotone (rpow b)
[PROOFSTEP]
case inl => exact (strictMono_rpow_of_base_gt_one hb).monotone
[GOAL]
x y z b : ℝ
hb✝ : 1 ≤ b
hb : 1 < b
⊢ Monotone (rpow b)
[PROOFSTEP]
exact (strictMono_rpow_of_base_gt_one hb).monotone
[GOAL]
case inr
x y z : ℝ
hb : 1 ≤ 1
⊢ Monotone (rpow 1)
[PROOFSTEP]
case inr => intro _ _ _; simp
[GOAL]
x y z : ℝ
hb : 1 ≤ 1
⊢ Monotone (rpow 1)
[PROOFSTEP]
case inr => intro _ _ _; simp
[GOAL]
x y z : ℝ
hb : 1 ≤ 1
⊢ Monotone (rpow 1)
[PROOFSTEP]
intro _ _ _
[GOAL]
x y z : ℝ
hb : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ rpow 1 a✝¹ ≤ rpow 1 b✝
[PROOFSTEP]
simp
[GOAL]
x y z b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti (rpow b)
[PROOFSTEP]
show StrictAnti (fun (x : ℝ) => b ^ x)
[GOAL]
x y z b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x => b ^ x
[PROOFSTEP]
simp_rw [Real.rpow_def_of_pos hb₀]
[GOAL]
x y z b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x => exp (log b * x)
[PROOFSTEP]
exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id <| Real.log_neg hb₀ hb₁
[GOAL]
x y z b : ℝ
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ Antitone (rpow b)
[PROOFSTEP]
rcases lt_or_eq_of_le hb₁ with hb₁ | rfl
[GOAL]
case inl
x y z b : ℝ
hb₀ : 0 < b
hb₁✝ : b ≤ 1
hb₁ : b < 1
⊢ Antitone (rpow b)
case inr x y z : ℝ hb₀ : 0 < 1 hb₁ : 1 ≤ 1 ⊢ Antitone (rpow 1)
[PROOFSTEP]
case inl => exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone
[GOAL]
x y z b : ℝ
hb₀ : 0 < b
hb₁✝ : b ≤ 1
hb₁ : b < 1
⊢ Antitone (rpow b)
[PROOFSTEP]
case inl => exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone
[GOAL]
x y z b : ℝ
hb₀ : 0 < b
hb₁✝ : b ≤ 1
hb₁ : b < 1
⊢ Antitone (rpow b)
[PROOFSTEP]
exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone
[GOAL]
case inr
x y z : ℝ
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone (rpow 1)
[PROOFSTEP]
case inr => intro _ _ _; simp
[GOAL]
x y z : ℝ
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone (rpow 1)
[PROOFSTEP]
case inr => intro _ _ _; simp
[GOAL]
x y z : ℝ
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone (rpow 1)
[PROOFSTEP]
intro _ _ _
[GOAL]
x y z : ℝ
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ rpow 1 b✝ ≤ rpow 1 a✝¹
[PROOFSTEP]
simp
[GOAL]
z x✝ y x : ℝ
⊢ sqrt x = x ^ (1 / 2)
[PROOFSTEP]
obtain h | h := le_or_lt 0 x
[GOAL]
case inl
z x✝ y x : ℝ
h : 0 ≤ x
⊢ sqrt x = x ^ (1 / 2)
[PROOFSTEP]
rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg_of_nonneg h _), mul_self_sqrt h, ← sq, ← rpow_nat_cast, ←
  rpow_mul h]
[GOAL]
case inl
z x✝ y x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2 * ↑2)
[PROOFSTEP]
norm_num
[GOAL]
case inr
z x✝ y x : ℝ
h : x < 0
⊢ sqrt x = x ^ (1 / 2)
[PROOFSTEP]
have : 1 / (2 : ℝ) * π = π / (2 : ℝ)
[GOAL]
case this
z x✝ y x : ℝ
h : x < 0
⊢ 1 / 2 * π = π / 2
case inr z x✝ y x : ℝ h : x < 0 this : 1 / 2 * π = π / 2 ⊢ sqrt x = x ^ (1 / 2)
[PROOFSTEP]
ring
[GOAL]
case inr
z x✝ y x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ sqrt x = x ^ (1 / 2)
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]
[GOAL]
z x✝ y x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = sqrt x ^ r
[PROOFSTEP]
rw [sqrt_eq_rpow, ← rpow_mul hx]
[GOAL]
z x✝ y x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)
[PROOFSTEP]
congr
[GOAL]
case e_a
z x✝ y x r : ℝ
hx : 0 ≤ x
⊢ r / 2 = 1 / 2 * r
[PROOFSTEP]
ring
[GOAL]
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
have hn' : 0 < (n : ℝ) := by exact_mod_cast hn.bot_lt
[GOAL]
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
⊢ 0 < ↑n
[PROOFSTEP]
exact_mod_cast hn.bot_lt
[GOAL]
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
obtain ⟨q, hxq, hqy⟩ := exists_rat_btwn (rpow_lt_rpow (le_max_left 0 x) (max_lt hy h) <| inv_pos.mpr hn')
[GOAL]
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
have := rpow_nonneg_of_nonneg (le_max_left 0 x) n⁻¹
[GOAL]
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
have hq := this.trans_lt hxq
[GOAL]
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
replace hxq := rpow_lt_rpow this hxq hn'
[GOAL]
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ ↑n < ↑q ^ ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
replace hqy := rpow_lt_rpow hq.le hqy hn'
[GOAL]
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ ↑n < ↑q ^ ↑n
hqy : ↑q ^ ↑n < (y ^ (↑n)⁻¹) ^ ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
rw [rpow_nat_cast, rpow_nat_cast, rpow_nat_inv_pow_nat _ hn] at hxq hqy 
[GOAL]
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : max 0 x < ↑q ^ n
hqy : ↑q ^ n < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
exact ⟨q, by exact_mod_cast hq, (le_max_right _ _).trans_lt hxq, hqy⟩
[GOAL]
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : max 0 x < ↑q ^ n
hqy : ↑q ^ n < y
⊢ 0 < q
[PROOFSTEP]
exact_mod_cast hq
[GOAL]
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : max 0 x < ↑q ^ n
hqy : ↑q ^ n < (y ^ (↑n)⁻¹) ^ n
⊢ 0 ≤ y
[PROOFSTEP]
exact hy.le
[GOAL]
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ n < ↑q ^ n
hqy : ↑q ^ n < (y ^ (↑n)⁻¹) ^ n
⊢ 0 ≤ max 0 x
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℚ
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y
[PROOFSTEP]
apply_mod_cast exists_rat_pow_btwn_rat_aux hn x y
[GOAL]
case a
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℚ
h : x < y
hy : 0 < y
⊢ x < y
[PROOFSTEP]
assumption
[GOAL]
case a
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℚ
h : x < y
hy : 0 < y
⊢ 0 < y
[PROOFSTEP]
assumption
[GOAL]
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
obtain ⟨q₂, hx₂, hy₂⟩ := exists_rat_btwn (max_lt h hy)
[GOAL]
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
obtain ⟨q₁, hx₁, hq₁₂⟩ := exists_rat_btwn hx₂
[GOAL]
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
have : (0 : α) < q₂ := (le_max_right _ _).trans_lt hx₂
[GOAL]
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
this : 0 < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
norm_cast at hq₁₂ this 
[GOAL]
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
obtain ⟨q, hq, hq₁, hq₂⟩ := exists_rat_pow_btwn_rat hn hq₁₂ this
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
[PROOFSTEP]
refine' ⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans _, hy₂.trans' _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_1
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ↑q₁ < ↑q ^ n
[PROOFSTEP]
assumption_mod_cast
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_2
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ↑q ^ n < ↑q₂
[PROOFSTEP]
assumption_mod_cast
