Real exponentiation, part I
Analysis I, Section 5.6: Real exponentiation, part I
I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.
Main constructions and results of this section:
-
Exponentiating reals to natural numbers and integers.
-
nth roots.
-
Raising a real to a rational number.
Tips from past users
Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.
-
(Add tip here)
namespace Chapter5
Definition 5.6.1 (Exponentiating a real by a natural number). Here we use the
Mathlib definition coming from Monoid.
lemma Real.pow_zero (x: Real) : x ^ 0 = 1 := rfllemma Real.pow_succ (x: Real) (n:ℕ) : x ^ (n+1) = (x ^ n) * x := rfllemma Real.pow_of_coe (q: ℚ) (n:ℕ) : (q:Real) ^ n = (q ^ n:ℚ) := q:ℚn:ℕ⊢ ↑q ^ n = ↑(q ^ n) q:ℚ⊢ ↑q ^ 0 = ↑(q ^ 0)q:ℚn:ℕhn:↑q ^ n = ↑(q ^ n)⊢ ↑q ^ (n + 1) = ↑(q ^ (n + 1)) q:ℚ⊢ ↑q ^ 0 = ↑(q ^ 0)q:ℚn:ℕhn:↑q ^ n = ↑(q ^ n)⊢ ↑q ^ (n + 1) = ↑(q ^ (n + 1)) All goals completed! 🐙/- The claims below can be handled easily by existing Mathlib API (as `Real` already is known
to be a `Field`), but the spirit of the exercises is to adapt the proofs of
Proposition 4.3.10 that you previously established. -/Analogue of Proposition 4.3.10(a)
theorem Real.pow_add (x:Real) (m n:ℕ) : x^n * x^m = x^(n+m) := x:Realm:ℕn:ℕ⊢ x ^ n * x ^ m = x ^ (n + m) All goals completed! 🐙Analogue of Proposition 4.3.10(a)
theorem Real.pow_mul (x:Real) (m n:ℕ) : (x^n)^m = x^(n*m) := x:Realm:ℕn:ℕ⊢ (x ^ n) ^ m = x ^ (n * m) All goals completed! 🐙Analogue of Proposition 4.3.10(a)
theorem Real.mul_pow (x y:Real) (n:ℕ) : (x*y)^n = x^n * y^n := x:Realy:Realn:ℕ⊢ (x * y) ^ n = x ^ n * y ^ n All goals completed! 🐙Analogue of Proposition 4.3.10(b)
theorem Real.pow_eq_zero (x:Real) (n:ℕ) (hn : 0 < n) : x^n = 0 ↔ x = 0 := x:Realn:ℕhn:0 < n⊢ x ^ n = 0 ↔ x = 0 All goals completed! 🐙Analogue of Proposition 4.3.10(c)
theorem Real.pow_nonneg {x:Real} (n:ℕ) (hx: x ≥ 0) : x^n ≥ 0 := x:Realn:ℕhx:x ≥ 0⊢ x ^ n ≥ 0 All goals completed! 🐙Analogue of Proposition 4.3.10(c)
theorem Real.pow_pos {x:Real} (n:ℕ) (hx: x > 0) : x^n > 0 := x:Realn:ℕhx:x > 0⊢ x ^ n > 0 All goals completed! 🐙Analogue of Proposition 4.3.10(c)
theorem Real.pow_ge_pow (x y:Real) (n:ℕ) (hxy: x ≥ y) (hy: y ≥ 0) : x^n ≥ y^n := x:Realy:Realn:ℕhxy:x ≥ yhy:y ≥ 0⊢ x ^ n ≥ y ^ n All goals completed! 🐙Analogue of Proposition 4.3.10(c)
theorem Real.pow_gt_pow (x y:Real) (n:ℕ) (hxy: x > y) (hy: y ≥ 0) (hn: n > 0) : x^n > y^n := x:Realy:Realn:ℕhxy:x > yhy:y ≥ 0hn:n > 0⊢ x ^ n > y ^ n All goals completed! 🐙Analogue of Proposition 4.3.10(d)
theorem Real.pow_abs (x:Real) (n:ℕ) : |x|^n = |x^n| := x:Realn:ℕ⊢ |x| ^ n = |x ^ n| All goals completed! 🐙
Definition 5.6.2 (Exponentiating a real by an integer). Here we use the Mathlib definition coming from DivInvMonoid.
lemma Real.pow_eq_pow (x: Real) (n:ℕ): x ^ (n:ℤ) = x ^ n := x:Realn:ℕ⊢ x ^ ↑n = x ^ n All goals completed! 🐙@[simp]
lemma Real.zpow_zero (x: Real) : x ^ (0:ℤ) = 1 := x:Real⊢ x ^ 0 = 1 All goals completed! 🐙lemma Real.zpow_neg {x:Real} (n:ℕ) : x^(-n:ℤ) = 1 / (x^n) := x:Realn:ℕ⊢ x ^ (-↑n) = 1 / x ^ n All goals completed! 🐙Analogue of Proposition 4.3.12(a)
theorem Real.zpow_add (x:Real) (n m:ℤ) (hx: x ≠ 0): x^n * x^m = x^(n+m) := x:Realn:ℤm:ℤhx:x ≠ 0⊢ x ^ n * x ^ m = x ^ (n + m) All goals completed! 🐙Analogue of Proposition 4.3.12(a)
theorem Real.zpow_mul (x:Real) (n m:ℤ) : (x^n)^m = x^(n*m) := x:Realn:ℤm:ℤ⊢ (x ^ n) ^ m = x ^ (n * m) All goals completed! 🐙Analogue of Proposition 4.3.12(a)
theorem Real.mul_zpow (x y:Real) (n:ℤ) : (x*y)^n = x^n * y^n := x:Realy:Realn:ℤ⊢ (x * y) ^ n = x ^ n * y ^ n All goals completed! 🐙Analogue of Proposition 4.3.12(b)
theorem Real.zpow_pos {x:Real} (n:ℤ) (hx: x > 0) : x^n > 0 := x:Realn:ℤhx:x > 0⊢ x ^ n > 0 All goals completed! 🐙Analogue of Proposition 4.3.12(b)
theorem Real.zpow_ge_zpow {x y:Real} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n > 0): x^n ≥ y^n := x:Realy:Realn:ℤhxy:x ≥ yhy:y > 0hn:n > 0⊢ x ^ n ≥ y ^ n All goals completed! 🐙theorem Real.zpow_ge_zpow_ofneg {x y:Real} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n < 0) : x^n ≤ y^n := x:Realy:Realn:ℤhxy:x ≥ yhy:y > 0hn:n < 0⊢ x ^ n ≤ y ^ n
All goals completed! 🐙Analogue of Proposition 4.3.12(c)
theorem Real.zpow_inj {x y:Real} {n:ℤ} (hx: x > 0) (hy : y > 0) (hn: n ≠ 0) (hxy: x^n = y^n) : x = y := x:Realy:Realn:ℤhx:x > 0hy:y > 0hn:n ≠ 0hxy:x ^ n = y ^ n⊢ x = y
All goals completed! 🐙Analogue of Proposition 4.3.12(d)
theorem Real.zpow_abs (x:Real) (n:ℤ) : |x|^n = |x^n| := x:Realn:ℤ⊢ |x| ^ n = |x ^ n| All goals completed! 🐙
Definition 5.6.2. We permit ``junk values'' when x is negative or n vanishes.
noncomputable abbrev Real.root (x:Real) (n:ℕ) : Real := sSup { y:Real | y ≥ 0 ∧ y^n ≤ x }noncomputable abbrev Real.sqrt (x:Real) := x.root 2Lemma 5.6.5 (Existence of n^th roots)
theorem Real.rootset_nonempty {x:Real} (hx: x ≥ 0) (n:ℕ) (hn: n ≥ 1) : { y:Real | y ≥ 0 ∧ y^n ≤ x }.Nonempty := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ {y | y ≥ 0 ∧ y ^ n ≤ x}.Nonempty
x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ 0 ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}
All goals completed! 🐙theorem Real.rootset_bddAbove {x:Real} (n:ℕ) (hn: n ≥ 1) : BddAbove { y:Real | y ≥ 0 ∧ y^n ≤ x } := x:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
-- This proof is written to follow the structure of the original text.
x:Realn:ℕhn:n ≥ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1
x:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1x:Realn:ℕhn:n ≥ 1h:1 < x⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1
x:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1 x:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ 1; x:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}⊢ y ≤ 1; x:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:0 ≤ y ∧ y ^ n ≤ x⊢ y ≤ 1
x:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:0 ≤ y ∧ y ^ n ≤ xhy':1 < y⊢ False
replace hy' : 1 < y^n := x:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
All goals completed! 🐙
All goals completed! 🐙
x:Realn:ℕhn:n ≥ 1h:1 < x⊢ ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x; x:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}⊢ y ≤ x; x:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:0 ≤ y ∧ y ^ n ≤ x⊢ y ≤ x
x:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:0 ≤ y ∧ y ^ n ≤ xhy':x < y⊢ False
replace hy' : x < y^n := x:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
All goals completed! 🐙
All goals completed! 🐙Lemma 5.6.6 (ab) / Exercise 5.6.1
theorem Real.eq_root_iff_pow_eq {x y:Real} (hx: x ≥ 0) (hy: y ≥ 0) {n:ℕ} (hn: n ≥ 1) :
y = x.root n ↔ y^n = x := x:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ y = x.root n ↔ y ^ n = x All goals completed! 🐙Lemma 5.6.6 (c) / Exercise 5.6.1
theorem Real.root_nonneg {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) : x.root n ≥ 0 := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n ≥ 0 All goals completed! 🐙Lemma 5.6.6 (c) / Exercise 5.6.1
theorem Real.root_pos {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) : x.root n > 0 ↔ x > 0 := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n > 0 ↔ x > 0 All goals completed! 🐙theorem Real.pow_of_root {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) :
(x.root n)^n = x := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n ^ n = x All goals completed! 🐙theorem Real.root_of_pow {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) :
(x^n).root n = x := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ (x ^ n).root n = x All goals completed! 🐙Lemma 5.6.6 (d) / Exercise 5.6.1
theorem Real.root_mono {x y:Real} (hx: x ≥ 0) (hy: y ≥ 0) {n:ℕ} (hn: n ≥ 1) : x > y ↔ x.root n > y.root n := x:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ x > y ↔ x.root n > y.root n All goals completed! 🐙Lemma 5.6.6 (e) / Exercise 5.6.1
theorem Real.root_mono_of_gt_one {x : Real} (hx: x > 1) {k l: ℕ} (hkl: k > l) (hl: l ≥ 1) : x.root k < x.root l := x:Realhx:x > 1k:ℕl:ℕhkl:k > lhl:l ≥ 1⊢ x.root k < x.root l All goals completed! 🐙Lemma 5.6.6 (e) / Exercise 5.6.1
theorem Real.root_mono_of_lt_one {x : Real} (hx0: 0 < x) (hx: x < 1) {k l: ℕ} (hkl: k > l) (hl: l ≥ 1) : x.root k > x.root l := x:Realhx0:0 < xhx:x < 1k:ℕl:ℕhkl:k > lhl:l ≥ 1⊢ x.root k > x.root l All goals completed! 🐙Lemma 5.6.6 (e) / Exercise 5.6.1
theorem Real.root_of_one {k: ℕ} (hk: k ≥ 1): (1:Real).root k = 1 := k:ℕhk:k ≥ 1⊢ root 1 k = 1 All goals completed! 🐙Lemma 5.6.6 (f) / Exercise 5.6.1
theorem Real.root_mul {x y:Real} (hx: x ≥ 0) (hy: y ≥ 0) {n:ℕ} (hn: n ≥ 1) : (x*y).root n = (x.root n) * (y.root n) := x:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ (x * y).root n = x.root n * y.root n All goals completed! 🐙Lemma 5.6.6 (f) / Exercise 5.6.1
theorem Real.root_root {x:Real} (hx: x ≥ 0) {n m:ℕ} (hn: n ≥ 1) (hm: m ≥ 1): (x.root n).root m = x.root (n*m) := x:Realhx:x ≥ 0n:ℕm:ℕhn:n ≥ 1hm:m ≥ 1⊢ (x.root n).root m = x.root (n * m) All goals completed! 🐙theorem Real.root_one {x:Real} (hx: x > 0): x.root 1 = x := x:Realhx:x > 0⊢ x.root 1 = x All goals completed! 🐙theorem Real.pow_cancel {y z:Real} (hy: y > 0) (hz: z > 0) {n:ℕ} (hn: n ≥ 1)
(h: y^n = z^n) : y = z := y:Realz:Realhy:y > 0hz:z > 0n:ℕhn:n ≥ 1h:y ^ n = z ^ n⊢ y = z All goals completed! 🐙example : ¬(∀ (y:Real) (z:Real) (n:ℕ) (_: n ≥ 1) (_: y^n = z^n), y = z) := ⊢ ¬∀ (y z : Real), ∀ n ≥ 1, y ^ n = z ^ n → y = z
⊢ ∃ x x_1 x_2, 1 ≤ x_2 ∧ x ^ x_2 = x_1 ^ x_2 ∧ ¬x = x_1; ⊢ 1 ≤ 2⊢ (-3) ^ 2 = 3 ^ 2⊢ ¬-3 = 3 ⊢ 1 ≤ 2⊢ (-3) ^ 2 = 3 ^ 2⊢ ¬-3 = 3 All goals completed! 🐙
noncomputable instance Real.instRatPow : Pow Real ℚ where
pow x q := x.ratPow qtheorem Rat.eq_quot (q:ℚ) : ∃ a:ℤ, ∃ b:ℕ, b > 0 ∧ q = a / b := q:ℚ⊢ ∃ a, ∃ b > 0, q = ↑a / ↑b
q:ℚ⊢ q.den > 0 ∧ q = ↑q.num / ↑q.den; q:ℚthis:?_mvar.65025 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ q.den > 0 ∧ q = ↑q.num / ↑q.den
refine ⟨ q:ℚthis:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ q.den > 0 All goals completed! 🐙, (Rat.num_div_den q).symm ⟩Lemma 5.6.8
theorem Real.pow_root_eq_pow_root {a a':ℤ} {b b':ℕ} (hb: b > 0) (hb' : b' > 0)
(hq : (a/b:ℚ) = (a'/b':ℚ)) {x:Real} (hx: x > 0) :
(x.root b')^(a') = (x.root b)^(a) := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a
-- This proof is written to follow the structure of the original text.
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha:¬a > 0⊢ x.root b' ^ a' = x.root b ^ ax:Realhx:x > 0a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'ha:a > 0⊢ x.root b' ^ a' = x.root b ^ a
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha:¬a > 0⊢ x.root b' ^ a' = x.root b ^ a a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha:a ≤ 0⊢ x.root b' ^ a' = x.root b ^ a
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a < 0⊢ x.root b' ^ a' = x.root b ^ aa:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a = 0⊢ x.root b' ^ a' = x.root b ^ a
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a < 0⊢ x.root b' ^ a' = x.root b ^ a replace hq : ((-a:ℤ)/b:ℚ) = ((-a':ℤ)/b':ℚ) := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a < 0⊢ -↑a / ↑b = -↑a' / ↑b'; a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0x:Realhx:x > 0ha✝:a ≤ 0ha:a < 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a * (↑b)⁻¹ = ↑a' * (↑b')⁻¹ → a > 0 → x.root b' ^ a' = x.root b ^ ahq:↑a * (↑b)⁻¹ = ↑a' * (↑b')⁻¹⊢ -(↑a * (↑b)⁻¹) = -(↑a' * (↑b')⁻¹); All goals completed! 🐙
specialize this hb hb' hq (a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a < 0hq:↑(-_fvar.65683) / ↑_fvar.65685 = ↑(-_fvar.65684) / ↑_fvar.65686 :=
Eq.mpr
(id
(congr (congrArg (fun x => Eq (x / ↑_fvar.65685)) (Int.cast_neg _fvar.65683))
(congrArg (fun x => x / ↑_fvar.65686) (Int.cast_neg _fvar.65684))))
(Eq.mpr
(id
(congr
(congrArg Eq
(Eq.trans
(Mathlib.Tactic.Ring.div_congr
(Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.65683)
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (↑_fvar.65683) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.atom_pf ↑_fvar.65685)
(Mathlib.Tactic.Ring.div_pf
(Mathlib.Tactic.Ring.inv_single
(Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑_fvar.65685)⁻¹)
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)))))
(Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.65685)⁻¹ (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.65683) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.65685)⁻¹ (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast)))
(Mathlib.Tactic.Ring.mul_zero (↑_fvar.65683 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast))
(Mathlib.Tactic.Ring.add_pf_add_zero
(↑_fvar.65683 ^ Nat.rawCast 1 * ((↑_fvar.65685)⁻¹ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) +
0)))
(Mathlib.Tactic.Ring.zero_mul ((↑_fvar.65685)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero
(↑_fvar.65683 ^ Nat.rawCast 1 * ((↑_fvar.65685)⁻¹ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) +
0)))))
(Eq.trans
(congrArg (fun x => x + 0)
(Eq.trans
(congr
(congrArg HMul.hMul
(Eq.trans (congrArg (HPow.hPow ↑_fvar.65683) Mathlib.Tactic.RingNF.nat_rawCast_1)
(pow_one ↑_fvar.65683)))
(Eq.trans
(Eq.trans
(congr
(congrArg HMul.hMul
(Eq.trans (congrArg (HPow.hPow (↑_fvar.65685)⁻¹) Mathlib.Tactic.RingNF.nat_rawCast_1)
(pow_one (↑_fvar.65685)⁻¹)))
(Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg
(congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1)))
(Mathlib.Tactic.RingNF.mul_neg (↑_fvar.65685)⁻¹ 1))
(congrArg Neg.neg (mul_one (↑_fvar.65685)⁻¹))))
(Mathlib.Tactic.RingNF.mul_neg (↑_fvar.65683) (↑_fvar.65685)⁻¹)))
(add_zero (-(↑_fvar.65683 * (↑_fvar.65685)⁻¹))))))
(Eq.trans
(Mathlib.Tactic.Ring.div_congr
(Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.65684)
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (↑_fvar.65684) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.atom_pf ↑_fvar.65686)
(Mathlib.Tactic.Ring.div_pf
(Mathlib.Tactic.Ring.inv_single
(Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑_fvar.65686)⁻¹)
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)))))
(Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.65686)⁻¹ (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.65684) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.65686)⁻¹ (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast)))
(Mathlib.Tactic.Ring.mul_zero (↑_fvar.65684 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast))
(Mathlib.Tactic.Ring.add_pf_add_zero
(↑_fvar.65684 ^ Nat.rawCast 1 * ((↑_fvar.65686)⁻¹ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))
(Mathlib.Tactic.Ring.zero_mul ((↑_fvar.65686)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero
(↑_fvar.65684 ^ Nat.rawCast 1 * ((↑_fvar.65686)⁻¹ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))))
(Eq.trans
(congrArg (fun x => x + 0)
(Eq.trans
(congr
(congrArg HMul.hMul
(Eq.trans (congrArg (HPow.hPow ↑_fvar.65684) Mathlib.Tactic.RingNF.nat_rawCast_1)
(pow_one ↑_fvar.65684)))
(Eq.trans
(Eq.trans
(congr
(congrArg HMul.hMul
(Eq.trans (congrArg (HPow.hPow (↑_fvar.65686)⁻¹) Mathlib.Tactic.RingNF.nat_rawCast_1)
(pow_one (↑_fvar.65686)⁻¹)))
(Eq.trans Mathlib.Tactic.RingNF.int_rawCast_neg
(congrArg Neg.neg Mathlib.Tactic.RingNF.nat_rawCast_1)))
(Mathlib.Tactic.RingNF.mul_neg (↑_fvar.65686)⁻¹ 1))
(congrArg Neg.neg (mul_one (↑_fvar.65686)⁻¹))))
(Mathlib.Tactic.RingNF.mul_neg (↑_fvar.65684) (↑_fvar.65686)⁻¹)))
(add_zero (-(↑_fvar.65684 * (↑_fvar.65686)⁻¹)))))))
(of_eq_true
(Eq.trans
(congrArg (fun x => -x = -(↑_fvar.65684 * (↑_fvar.65686)⁻¹))
(Eq.mp
(congr
(congrArg Eq
(Eq.trans
(Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.65683)
(Mathlib.Tactic.Ring.atom_pf ↑_fvar.65685)
(Mathlib.Tactic.Ring.div_pf
(Mathlib.Tactic.Ring.inv_single
(Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑_fvar.65685)⁻¹)
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)))))
(Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.65685)⁻¹ (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.65683) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.65685)⁻¹ (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))
(Mathlib.Tactic.Ring.mul_zero (↑_fvar.65683 ^ Nat.rawCast 1 * Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero
(↑_fvar.65683 ^ Nat.rawCast 1 * ((↑_fvar.65685)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))
(Mathlib.Tactic.Ring.zero_mul ((↑_fvar.65685)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero
(↑_fvar.65683 ^ Nat.rawCast 1 * ((↑_fvar.65685)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))))
(Eq.trans
(congrArg (fun x => x + 0)
(congr
(congrArg HMul.hMul
(Eq.trans (congrArg (HPow.hPow ↑_fvar.65683) Mathlib.Tactic.RingNF.nat_rawCast_1)
(pow_one ↑_fvar.65683)))
(Eq.trans
(congr
(congrArg HMul.hMul
(Eq.trans (congrArg (HPow.hPow (↑_fvar.65685)⁻¹) Mathlib.Tactic.RingNF.nat_rawCast_1)
(pow_one (↑_fvar.65685)⁻¹)))
Mathlib.Tactic.RingNF.nat_rawCast_1)
(mul_one (↑_fvar.65685)⁻¹))))
(add_zero (↑_fvar.65683 * (↑_fvar.65685)⁻¹)))))
(Eq.trans
(Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.65684)
(Mathlib.Tactic.Ring.atom_pf ↑_fvar.65686)
(Mathlib.Tactic.Ring.div_pf
(Mathlib.Tactic.Ring.inv_single
(Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑_fvar.65686)⁻¹)
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1)))))
(Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.65686)⁻¹ (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.65684) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.65686)⁻¹ (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))
(Mathlib.Tactic.Ring.mul_zero (↑_fvar.65684 ^ Nat.rawCast 1 * Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero
(↑_fvar.65684 ^ Nat.rawCast 1 * ((↑_fvar.65686)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))
(Mathlib.Tactic.Ring.zero_mul ((↑_fvar.65686)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero
(↑_fvar.65684 ^ Nat.rawCast 1 * ((↑_fvar.65686)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))))
(Eq.trans
(congrArg (fun x => x + 0)
(congr
(congrArg HMul.hMul
(Eq.trans (congrArg (HPow.hPow ↑_fvar.65684) Mathlib.Tactic.RingNF.nat_rawCast_1)
(pow_one ↑_fvar.65684)))
(Eq.trans
(congr
(congrArg HMul.hMul
(Eq.trans (congrArg (HPow.hPow (↑_fvar.65686)⁻¹) Mathlib.Tactic.RingNF.nat_rawCast_1)
(pow_one (↑_fvar.65686)⁻¹)))
Mathlib.Tactic.RingNF.nat_rawCast_1)
(mul_one (↑_fvar.65686)⁻¹))))
(add_zero (↑_fvar.65684 * (↑_fvar.65686)⁻¹)))))
_fvar.65689))
(eq_self (-(↑_fvar.65684 * (↑_fvar.65686)⁻¹))))))⊢ -a > 0 All goals completed! 🐙)
All goals completed! 🐙
have : a' = 0 := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a All goals completed! 🐙
All goals completed! 🐙
have : a' > 0 := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a All goals completed! 🐙
x:Realhx:x > 0a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0ha:a > 0this:_fvar.65746 > 0 := ?_mvar.132179hq:↑a * ↑b' = ↑a' * ↑b⊢ x.root b' ^ a' = x.root b ^ a
lift a to ℕ using x:Realhx:x > 0a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0ha:a > 0this:_fvar.65746 > 0 := sorryhq:↑a * ↑b' = ↑a' * ↑b⊢ 0 ≤ a All goals completed! 🐙
lift a' to ℕ using x:Realhx:x > 0a':ℤb:ℕb':ℕhb:b > 0hb':b' > 0this:_fvar.65746 > 0 := sorrya:ℕha:↑a > 0hq:↑↑a * ↑b' = ↑a' * ↑b⊢ 0 ≤ a' All goals completed! 🐙
x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * b⊢ x.root b' ^ a' = x.root b ^ a
x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)⊢ x.root b' ^ a' = x.root b ^ a
have h1 : y = (x.root b').root a := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)⊢ b' ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)⊢ a ≥ 1 x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)⊢ b' ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)⊢ a ≥ 1 All goals completed! 🐙
have h2 : y = (x.root b).root a' := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891⊢ b ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891⊢ a' ≥ 1 x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891⊢ b ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891⊢ a' ≥ 1 All goals completed! 🐙
have h3 : y^a = x.root b' := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954⊢ (x.root b').root a ^ a = x.root b'; x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954⊢ a ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954⊢ b' ≥ 1 x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954⊢ a ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954⊢ b' ≥ 1 All goals completed! 🐙
have h4 : y^a' = x.root b := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954h3:_fvar.149744 ^ _fvar.140840 = Chapter5.Real.root _fvar.65690 _fvar.65748 := ?_mvar.178249⊢ (x.root b).root a' ^ a' = x.root b; x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954h3:_fvar.149744 ^ _fvar.140840 = Chapter5.Real.root _fvar.65690 _fvar.65748 := ?_mvar.178249⊢ a' ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954h3:_fvar.149744 ^ _fvar.140840 = Chapter5.Real.root _fvar.65690 _fvar.65748 := ?_mvar.178249⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954h3:_fvar.149744 ^ _fvar.140840 = Chapter5.Real.root _fvar.65690 _fvar.65748 := ?_mvar.178249⊢ b ≥ 1 x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954h3:_fvar.149744 ^ _fvar.140840 = Chapter5.Real.root _fvar.65690 _fvar.65748 := ?_mvar.178249⊢ a' ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954h3:_fvar.149744 ^ _fvar.140840 = Chapter5.Real.root _fvar.65690 _fvar.65748 := ?_mvar.178249⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = a' * by:Chapter5.Real := Chapter5.Real.root _fvar.65690 (_fvar.140840 * _fvar.65748)h1:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65748).root _fvar.140840 := ?_mvar.149891h2:_fvar.149744 = (Chapter5.Real.root _fvar.65690 _fvar.65747).root _fvar.144763 := ?_mvar.163954h3:_fvar.149744 ^ _fvar.140840 = Chapter5.Real.root _fvar.65690 _fvar.65748 := ?_mvar.178249⊢ b ≥ 1 All goals completed! 🐙
All goals completed! 🐙theorem Real.ratPow_def {x:Real} (hx: x > 0) (a:ℤ) {b:ℕ} (hb: b > 0) : x^(a/b:ℚ) = (x.root b)^a := x:Realhx:x > 0a:ℤb:ℕhb:b > 0⊢ x ^ (↑a / ↑b) = x.root b ^ a
x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132⊢ x ^ q = x.root b ^ a
x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132⊢ q.den > 0x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132⊢ ↑a / ↑b = ↑q.num / ↑q.den
x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132⊢ q.den > 0 x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132this:?_mvar.209520 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ q.den > 0; All goals completed! 🐙
All goals completed! 🐙theorem Real.ratPow_eq_root {x:Real} (hx: x > 0) {n:ℕ} (hn: n ≥ 1) : x^(1/n:ℚ) = x.root n := x:Realhx:x > 0n:ℕhn:n ≥ 1⊢ x ^ (1 / ↑n) = x.root n All goals completed! 🐙theorem Real.ratPow_eq_pow {x:Real} (hx: x > 0) (n:ℤ) : x^(n:ℚ) = x^n := x:Realhx:x > 0n:ℤ⊢ x ^ ↑n = x ^ n All goals completed! 🐙Lemma 5.6.9(a) / Exercise 5.6.2
theorem Real.ratPow_nonneg {x:Real} (hx: x > 0) (q:ℚ) : x^q > 0 := x:Realhx:x > 0q:ℚ⊢ x ^ q > 0
All goals completed! 🐙Lemma 5.6.9(b) / Exercise 5.6.2
theorem Real.ratPow_add {x:Real} (hx: x > 0) (q r:ℚ) : x^(q+r) = x^q * x^r := x:Realhx:x > 0q:ℚr:ℚ⊢ x ^ (q + r) = x ^ q * x ^ r
All goals completed! 🐙Lemma 5.6.9(b) / Exercise 5.6.2
theorem Real.ratPow_ratPow {x:Real} (hx: x > 0) (q r:ℚ) : (x^q)^r = x^(q*r) := x:Realhx:x > 0q:ℚr:ℚ⊢ (x ^ q) ^ r = x ^ (q * r)
All goals completed! 🐙Lemma 5.6.9(c) / Exercise 5.6.2
theorem Real.ratPow_neg {x:Real} (hx: x > 0) (q:ℚ) : x^(-q) = 1 / x^q := x:Realhx:x > 0q:ℚ⊢ x ^ (-q) = 1 / x ^ q
All goals completed! 🐙Lemma 5.6.9(d) / Exercise 5.6.2
theorem Real.ratPow_mono {x y:Real} (hx: x > 0) (hy: y > 0) {q:ℚ} (h: q > 0) : x > y ↔ x^q > y^q := x:Realy:Realhx:x > 0hy:y > 0q:ℚh:q > 0⊢ x > y ↔ x ^ q > y ^ q
All goals completed! 🐙Lemma 5.6.9(e) / Exercise 5.6.2
theorem Real.ratPow_mono_of_gt_one {x:Real} (hx: x > 1) {q r:ℚ} : x^q > x^r ↔ q > r := x:Realhx:x > 1q:ℚr:ℚ⊢ x ^ q > x ^ r ↔ q > r
All goals completed! 🐙Lemma 5.6.9(e) / Exercise 5.6.2
theorem Real.ratPow_mono_of_lt_one {x:Real} (hx0: 0 < x) (hx: x < 1) {q r:ℚ} : x^q > x^r ↔ q < r := x:Realhx0:0 < xhx:x < 1q:ℚr:ℚ⊢ x ^ q > x ^ r ↔ q < r
All goals completed! 🐙Lemma 5.6.9(f) / Exercise 5.6.2
theorem Real.ratPow_mul {x y:Real} (hx: x > 0) (hy: y > 0) (q:ℚ) : (x*y)^q = x^q * y^q := x:Realy:Realhx:x > 0hy:y > 0q:ℚ⊢ (x * y) ^ q = x ^ q * y ^ q
All goals completed! 🐙Exercise 5.6.3
theorem Real.pow_even (x:Real) {n:ℕ} (hn: Even n) : x^n ≥ 0 := x:Realn:ℕhn:Even n⊢ x ^ n ≥ 0 All goals completed! 🐙Exercise 5.6.5
theorem Real.max_ratPow {x y:Real} (hx: x > 0) (hy: y > 0) {q:ℚ} (hq: q > 0) :
max (x^q) y^q = (max x y)^q := x:Realy:Realhx:x > 0hy:y > 0q:ℚhq:q > 0⊢ max (x ^ q) y ^ q = max x y ^ q
All goals completed! 🐙Exercise 5.6.5
theorem Real.min_ratPow {x y:Real} (hx: x > 0) (hy: y > 0) {q:ℚ} (hq: q > 0) :
min (x^q) y^q = (min x y)^q := x:Realy:Realhx:x > 0hy:y > 0q:ℚhq:q > 0⊢ min (x ^ q) y ^ q = min x y ^ q
All goals completed! 🐙-- Final part of Exercise 5.6.5: state and prove versions of the above lemmas covering the case of negative q.
end Chapter5