Real exponentiation, part I

Аналіз I, Розділ 5.6: Піднесення дійсних чисел до степеня, частина I

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

Піднесення дійсних чисел до степеня натуральних та цілих чисел.
Коріння n-го рівня.
Піднесення дійсного числа до раціонального.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

(Додайте підказку тут)

namespace Chapter5

Визначення 5.6.1 (Піднесення дійсного числа до степеня натурального числа). Тут ми використовуємо визначення Mathlib, взяте з Monoid.{u} (M : Type u) : Type uMonoid.

lemma Real.pow_zero (x: Real) : x ^ 0 = 1 := rfl

lemma Real.pow_succ (x: Real) (n:ℕ) : x ^ (n+1) = (x ^ n) * x := rfl

lemma Real.pow_of_coe (q: ℚ) (n:ℕ) : (q:Real) ^ n = (q ^ n:ℚ) := byq:ℚn:ℕ⊢ ↑q ^ n = ↑(q ^ n) induction' n with n hnzeroq:ℚ⊢ ↑q ^ 0 = ↑(q ^ 0)succq:ℚn:ℕhn:↑q ^ n = ↑(q ^ n)⊢ ↑q ^ (n + 1) = ↑(q ^ (n + 1)) <;>zeroq:ℚ⊢ ↑q ^ 0 = ↑(q ^ 0)succq:ℚn:ℕhn:↑q ^ n = ↑(q ^ n)⊢ ↑q ^ (n + 1) = ↑(q ^ (n + 1)) simpAll goals completed! 🐙

/- Твердження нижче можуть бути легко опрацьовані за допомогою наявного API Mathlib (оскільки вже відомо,
  що `Real` є `Field`), але суть вправ полягає в тому, щоб адаптувати доведення твердження 4.3.10, які ви
  встановили раніше. -/

Аналог Твердження 4.3.10(a)

theorem declaration uses 'sorry'Real.pow_add (x:Real) (m n:ℕ) : x^n * x^m = x^(n+m) := byx:Realm:ℕn:ℕ⊢ x ^ n * x ^ m = x ^ (n + m) sorryAll goals completed! 🐙

Аналог Твердження 4.3.10(a)

theorem declaration uses 'sorry'Real.pow_mul (x:Real) (m n:ℕ) : (x^n)^m = x^(n*m) := byx:Realm:ℕn:ℕ⊢ (x ^ n) ^ m = x ^ (n * m) sorryAll goals completed! 🐙

Аналог Твердження 4.3.10(a)

theorem declaration uses 'sorry'Real.mul_pow (x y:Real) (n:ℕ) : (x*y)^n = x^n * y^n := byx:Realy:Realn:ℕ⊢ (x * y) ^ n = x ^ n * y ^ n sorryAll goals completed! 🐙

Аналог Твердження 4.3.10(b)

theorem declaration uses 'sorry'Real.pow_eq_zero (x:Real) (n:ℕ) (hn : 0 < n) : x^n = 0 ↔ x = 0 := byx:Realn:ℕhn:0 < n⊢ x ^ n = 0 ↔ x = 0 sorryAll goals completed! 🐙

Аналог Твердження 4.3.10(c)

theorem declaration uses 'sorry'Real.pow_nonneg {x:Real} (n:ℕ) (hx: x ≥ 0) : x^n ≥ 0 := byx:Realn:ℕhx:x ≥ 0⊢ x ^ n ≥ 0 sorryAll goals completed! 🐙

Аналог Твердження 4.3.10(c)

theorem declaration uses 'sorry'Real.pow_pos {x:Real} (n:ℕ) (hx: x > 0) : x^n > 0 := byx:Realn:ℕhx:x > 0⊢ x ^ n > 0 sorryAll goals completed! 🐙

Аналог Твердження 4.3.10(c)

theorem declaration uses 'sorry'Real.pow_ge_pow (x y:Real) (n:ℕ) (hxy: x ≥ y) (hy: y ≥ 0) : x^n ≥ y^n := byx:Realy:Realn:ℕhxy:x ≥ yhy:y ≥ 0⊢ x ^ n ≥ y ^ n sorryAll goals completed! 🐙

Аналог Твердження 4.3.10(c)

theorem declaration uses 'sorry'Real.pow_gt_pow (x y:Real) (n:ℕ) (hxy: x > y) (hy: y ≥ 0) (hn: n > 0) : x^n > y^n := byx:Realy:Realn:ℕhxy:x > yhy:y ≥ 0hn:n > 0⊢ x ^ n > y ^ n sorryAll goals completed! 🐙

Аналог Твердження 4.3.10(d)

theorem declaration uses 'sorry'Real.pow_abs (x:Real) (n:ℕ) : |x|^n = |x^n| := byx:Realn:ℕ⊢ |x| ^ n = |x ^ n| sorryAll goals completed! 🐙

Визначення 5.6.2 (Піднесення дійсного числа до цілого степеня). Тут ми використовуємо визначення Mathlib, що походить від DivInvMonoid.{u} (G : Type u) : Type uDivInvMonoid.

lemma Real.pow_eq_pow (x: Real) (n:ℕ): x ^ (n:ℤ) = x ^ n := byx:Realn:ℕ⊢ x ^ ↑n = x ^ n rflAll goals completed! 🐙

@[simp]
lemma Real.zpow_zero (x: Real) : x ^ (0:ℤ) = 1 := byx:Real⊢ x ^ 0 = 1 rflAll goals completed! 🐙

lemma Real.zpow_neg {x:Real} (n:ℕ) : x^(-n:ℤ) = 1 / (x^n) := byx:Realn:ℕ⊢ x ^ (-↑n) = 1 / x ^ n simpAll goals completed! 🐙

Аналог Твердження 4.3.12(a)

theorem declaration uses 'sorry'Real.zpow_add (x:Real) (n m:ℤ) (hx: x ≠ 0): x^n * x^m = x^(n+m) := byx:Realn:ℤm:ℤhx:x ≠ 0⊢ x ^ n * x ^ m = x ^ (n + m) sorryAll goals completed! 🐙

Аналог Твердження 4.3.12(a)

theorem declaration uses 'sorry'Real.zpow_mul (x:Real) (n m:ℤ) : (x^n)^m = x^(n*m) := byx:Realn:ℤm:ℤ⊢ (x ^ n) ^ m = x ^ (n * m) sorryAll goals completed! 🐙

Аналог Твердження 4.3.12(a)

theorem declaration uses 'sorry'Real.mul_zpow (x y:Real) (n:ℤ) : (x*y)^n = x^n * y^n := byx:Realy:Realn:ℤ⊢ (x * y) ^ n = x ^ n * y ^ n sorryAll goals completed! 🐙

Аналог Твердження 4.3.12(b)

theorem declaration uses 'sorry'Real.zpow_pos {x:Real} (n:ℤ) (hx: x > 0) : x^n > 0 := byx:Realn:ℤhx:x > 0⊢ x ^ n > 0 sorryAll goals completed! 🐙

Аналог Твердження 4.3.12(b)

theorem declaration uses 'sorry'Real.zpow_ge_zpow {x y:Real} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n > 0): x^n ≥ y^n := byx:Realy:Realn:ℤhxy:x ≥ yhy:y > 0hn:n > 0⊢ x ^ n ≥ y ^ n sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.zpow_ge_zpow_ofneg {x y:Real} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n < 0) : x^n ≤ y^n := byx:Realy:Realn:ℤhxy:x ≥ yhy:y > 0hn:n < 0⊢ x ^ n ≤ y ^ n
  sorryAll goals completed! 🐙

Аналог Твердження 4.3.12(c)

theorem declaration uses 'sorry'Real.zpow_inj {x y:Real} {n:ℤ} (hx: x > 0) (hy : y > 0) (hn: n ≠ 0) (hxy: x^n = y^n) : x = y := byx:Realy:Realn:ℤhx:x > 0hy:y > 0hn:n ≠ 0hxy:x ^ n = y ^ n⊢ x = y
  sorryAll goals completed! 🐙

Аналог Твердження 4.3.12(d)

theorem declaration uses 'sorry'Real.zpow_abs (x:Real) (n:ℤ) : |x|^n = |x^n| := byx:Realn:ℤ⊢ |x| ^ n = |x ^ n| sorryAll goals completed! 🐙

Визначення 5.6.2. Ми допускаємо , коли Unknown identifier `x`x є від’ємним або Unknown identifier `n`n дорівнює нулю.

noncomputable abbrev Real.root (x:Real) (n:ℕ) : Real := sSup { y:Real | y ≥ 0 ∧ y^n ≤ x }

noncomputable abbrev Real.sqrt (x:Real) := x.root 2

Лема 5.6.5 (Існування коренів n-го степеня)

theorem declaration uses 'sorry'Real.rootset_nonempty {x:Real} (hx: x ≥ 0) (n:ℕ) (hn: n ≥ 1) : { y:Real | y ≥ 0 ∧ y^n ≤ x }.Nonempty := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ {y | y ≥ 0 ∧ y ^ n ≤ x}.Nonempty
  use 0hx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ 0 ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.rootset_bddAbove {x:Real} (n:ℕ) (hn: n ≥ 1) : BddAbove { y:Real | y ≥ 0 ∧ y^n ≤ x } := byx:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
  -- Доведення написане так, щоб відповідати структурі оригінального тексту.
  rw [_root_.bddAbove_def]x:Realn:ℕhn:n ≥ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1
  obtain h | h := le_or_gt x 1inlx:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1inrx:Realn:ℕhn:n ≥ 1h:1 < x⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1
  .inlx:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1 use 1hx:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ 1; intro y hyhx:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}⊢ y ≤ 1; simp at hyhx:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:0 ≤ y ∧ y ^ n ≤ x⊢ y ≤ 1
    by_contra! hy'hx:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:0 ≤ y ∧ y ^ n ≤ xhy':1 < y⊢ False
    replace hy' : 1 < y^n := byx:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
      sorryAll goals completed! 🐙
    linarithAll goals completed! 🐙
  use xhx:Realn:ℕhn:n ≥ 1h:1 < x⊢ ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x; intro y hyhx:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}⊢ y ≤ x; simp at hyhx:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:0 ≤ y ∧ y ^ n ≤ x⊢ y ≤ x
  by_contra! hy'hx:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:0 ≤ y ∧ y ^ n ≤ xhy':x < y⊢ False
  replace hy' : x < y^n := byx:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
    sorryAll goals completed! 🐙
  linarithAll goals completed! 🐙

Лема 5.6.6 (ab) / Вправа 5.6.1

theorem declaration uses 'sorry'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 := byx:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ y = x.root n ↔ y ^ n = x sorryAll goals completed! 🐙

Лема 5.6.6 (c) / Вправа 5.6.1

theorem declaration uses 'sorry'Real.root_nonneg {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) : x.root n ≥ 0 := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n ≥ 0 sorryAll goals completed! 🐙

Лема 5.6.6 (c) / Вправа 5.6.1

theorem declaration uses 'sorry'Real.root_pos {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) : x.root n > 0 ↔ x > 0 := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n > 0 ↔ x > 0 sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.pow_of_root {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) :
  (x.root n)^n = x := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n ^ n = x sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.root_of_pow {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) :
  (x^n).root n = x := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ (x ^ n).root n = x sorryAll goals completed! 🐙

Лема 5.6.6 (d) / Вправа 5.6.1

theorem declaration uses 'sorry'Real.root_mono {x y:Real} (hx: x ≥ 0) (hy: y ≥ 0) {n:ℕ} (hn: n ≥ 1) : x > y ↔ x.root n > y.root n := byx:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ x > y ↔ x.root n > y.root n sorryAll goals completed! 🐙

Лема 5.6.6 (e) / Вправа 5.6.1

theorem declaration uses 'sorry'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 := byx:Realhx:x > 1k:ℕl:ℕhkl:k > lhl:l ≥ 1⊢ x.root k < x.root l sorryAll goals completed! 🐙

Лема 5.6.6 (e) / Вправа 5.6.1

theorem declaration uses 'sorry'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 := byx:Realhx0:0 < xhx:x < 1k:ℕl:ℕhkl:k > lhl:l ≥ 1⊢ x.root k > x.root l sorryAll goals completed! 🐙

Лема 5.6.6 (e) / Вправа 5.6.1

theorem declaration uses 'sorry'Real.root_of_one {k: ℕ} (hk: k ≥ 1): (1:Real).root k = 1 := byk:ℕhk:k ≥ 1⊢ root 1 k = 1 sorryAll goals completed! 🐙

Лема 5.6.6 (f) / Вправа 5.6.1

theorem declaration uses 'sorry'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) := byx:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ (x * y).root n = x.root n * y.root n sorryAll goals completed! 🐙

Лема 5.6.6 (g) / Вправа 5.6.1

theorem declaration uses 'sorry'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) := byx:Realhx:x ≥ 0n:ℕm:ℕhn:n ≥ 1hm:m ≥ 1⊢ (x.root n).root m = x.root (n * m) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.root_one {x:Real} (hx: x > 0): x.root 1 = x := byx:Realhx:x > 0⊢ x.root 1 = x sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.pow_cancel {y z:Real} (hy: y > 0) (hz: z > 0) {n:ℕ} (hn: n ≥ 1)
  (h: y^n = z^n) : y = z := byy:Realz:Realhy:y > 0hz:z > 0n:ℕhn:n ≥ 1h:y ^ n = z ^ n⊢ y = z sorryAll goals completed! 🐙

example : ¬(∀ (y:Real) (z:Real) (n:ℕ) (_: n ≥ 1) (_: y^n = z^n), y = z) := by⊢ ¬∀ (y z : Real), ∀ n ≥ 1, y ^ n = z ^ n → y = z
  simp⊢ ∃ x x_1 x_2, 1 ≤ x_2 ∧ x ^ x_2 = x_1 ^ x_2 ∧ ¬x = x_1; refine ⟨ (-3), 3, 2, ?_, ?_, ?_ ⟩refine_1⊢ 1 ≤ 2refine_2⊢ (-3) ^ 2 = 3 ^ 2refine_3⊢ ¬-3 = 3 <;>refine_1⊢ 1 ≤ 2refine_2⊢ (-3) ^ 2 = 3 ^ 2refine_3⊢ ¬-3 = 3 norm_numAll goals completed! 🐙

Визначення 5.6.7

noncomputable abbrev Real.ratPow (x:Real) (q:ℚ) : Real := (x.root q.den)^(q.num)

noncomputable instance Real.instRatPow : Pow Real ℚ where
  pow x q := x.ratPow q

theorem Rat.eq_quot (q:ℚ) : ∃ a:ℤ, ∃ b:ℕ, b > 0 ∧ q = a / b := byq:ℚ⊢ ∃ a, ∃ b > 0, q = ↑a / ↑b
  use q.num, q.denhq:ℚ⊢ q.den > 0 ∧ q = ↑q.num / ↑q.den; have := q.den_nzhq:ℚ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 ⟨ byq:ℚ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 omegaAll goals completed! 🐙, (Rat.num_div_den q).symm ⟩

Лема 5.6.8

theorem declaration uses 'sorry'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) := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a
  -- Доведення написане так, щоб відповідати структурі оригінального тексту.
  wlog ha: a > 0 generalizing a b a' b'inra:ℤ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
  .inra:ℤ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 simp at hainra:ℤ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
    obtain ha | ha := le_iff_lt_or_eq.mp hainr.inla:ℤ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 ^ ainr.inra:ℤ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
    .inr.inla:ℤ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':ℚ) := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a
        push_cast at *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'; ring_nf at *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')⁻¹); simp [hq]All goals completed! 🐙
      specialize this hb hb' hq (bya:ℤ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 linarithAll goals completed! 🐙)
      simpa [zpow_neg] using thisAll goals completed! 🐙
    have : a' = 0 := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a sorryAll goals completed! 🐙
    simp_allAll goals completed! 🐙
  have : a' > 0 := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a sorryAll goals completed! 🐙
  field_simp at hqx: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 byx:Realhx:x > 0a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0ha:a > 0this:_fvar.65746 > 0 := sorryhq:↑a * ↑b' = ↑a' * ↑b⊢ 0 ≤ a orderAll goals completed! 🐙
  lift a' to ℕ using byx:Realhx:x > 0a':ℤb:ℕb':ℕhb:b > 0hb':b' > 0this:_fvar.65746 > 0 := sorrya:ℕha:↑a > 0hq:↑↑a * ↑b' = ↑a' * ↑b⊢ 0 ≤ a' orderAll goals completed! 🐙
  norm_cast at *intro.introx: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
  set y := x.root (a*b')intro.introx: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 := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a rw [root_root, mul_comm]hxx: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 ≥ 0hnx: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' ≥ 1hmx: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 <;>hxx: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 ≥ 0hnx: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' ≥ 1hmx: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 linarithAll goals completed! 🐙
  have h2 : y = (x.root b).root a' := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a rw [root_root, mul_comm, ←hq]hxx: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 ≥ 0hnx: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 ≥ 1hmx: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 <;>hxx: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 ≥ 0hnx: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 ≥ 1hmx: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 linarithAll goals completed! 🐙
  have h3 : y^a = x.root b' := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a rw [h1]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'; apply pow_of_root (root_nonneg _ _)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 linarithAll goals completed! 🐙
  have h4 : y^a' = x.root b := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a rw [h2]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; apply pow_of_root (root_nonneg _ _)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 linarithAll goals completed! 🐙
  rw [←h3, pow_mul, mul_comm, ←pow_mul, h4]All goals completed! 🐙

theorem Real.ratPow_def {x:Real} (hx: x > 0) (a:ℤ) {b:ℕ} (hb: b > 0) : x^(a/b:ℚ) = (x.root b)^a := byx:Realhx:x > 0a:ℤb:ℕhb:b > 0⊢ x ^ (↑a / ↑b) = x.root b ^ a
  set q := (a/b:ℚ)x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132⊢ x ^ q = x.root b ^ a
  convert pow_root_eq_pow_root hb _ _ hxconvert_4x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132⊢ q.den > 0convert_5x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132⊢ ↑a / ↑b = ↑q.num / ↑q.den
  .convert_4x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑_fvar.207131 / ↑_fvar.207132⊢ q.den > 0 have := q.den_nzconvert_4x: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; omegaAll goals completed! 🐙
  rw [Rat.num_div_den q]All goals completed! 🐙

theorem declaration uses 'sorry'Real.ratPow_eq_root {x:Real} (hx: x > 0) {n:ℕ} (hn: n ≥ 1) : x^(1/n:ℚ) = x.root n := byx:Realhx:x > 0n:ℕhn:n ≥ 1⊢ x ^ (1 / ↑n) = x.root n sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.ratPow_eq_pow {x:Real} (hx: x > 0) (n:ℤ) : x^(n:ℚ) = x^n := byx:Realhx:x > 0n:ℤ⊢ x ^ ↑n = x ^ n sorryAll goals completed! 🐙

Лема 5.6.9(a) / Вправа 5.6.2

theorem declaration uses 'sorry'Real.ratPow_pos {x:Real} (hx: x > 0) (q:ℚ) : x^q > 0 := byx:Realhx:x > 0q:ℚ⊢ x ^ q > 0
  sorryAll goals completed! 🐙

Лема 5.6.9(b) / Вправа 5.6.2

theorem declaration uses 'sorry'Real.ratPow_add {x:Real} (hx: x > 0) (q r:ℚ) : x^(q+r) = x^q * x^r := byx:Realhx:x > 0q:ℚr:ℚ⊢ x ^ (q + r) = x ^ q * x ^ r
  sorryAll goals completed! 🐙

Лема 5.6.9(b) / Вправа 5.6.2

theorem declaration uses 'sorry'Real.ratPow_ratPow {x:Real} (hx: x > 0) (q r:ℚ) : (x^q)^r = x^(q*r) := byx:Realhx:x > 0q:ℚr:ℚ⊢ (x ^ q) ^ r = x ^ (q * r)
  sorryAll goals completed! 🐙

Лема 5.6.9(c) / Вправа 5.6.2

theorem declaration uses 'sorry'Real.ratPow_neg {x:Real} (hx: x > 0) (q:ℚ) : x^(-q) = 1 / x^q := byx:Realhx:x > 0q:ℚ⊢ x ^ (-q) = 1 / x ^ q
  sorryAll goals completed! 🐙

Лема 5.6.9(d) / Вправа 5.6.2

theorem declaration uses 'sorry'Real.ratPow_mono {x y:Real} (hx: x > 0) (hy: y > 0) {q:ℚ} (h: q > 0) : x > y ↔ x^q > y^q := byx:Realy:Realhx:x > 0hy:y > 0q:ℚh:q > 0⊢ x > y ↔ x ^ q > y ^ q
  sorryAll goals completed! 🐙

Лема 5.6.9(e) / Вправа 5.6.2

theorem declaration uses 'sorry'Real.ratPow_mono_of_gt_one {x:Real} (hx: x > 1) {q r:ℚ} : x^q > x^r ↔ q > r := byx:Realhx:x > 1q:ℚr:ℚ⊢ x ^ q > x ^ r ↔ q > r
  sorryAll goals completed! 🐙

Лема 5.6.9(e) / Вправа 5.6.2

theorem declaration uses 'sorry'Real.ratPow_mono_of_lt_one {x:Real} (hx0: 0 < x) (hx: x < 1) {q r:ℚ} : x^q > x^r ↔ q < r := byx:Realhx0:0 < xhx:x < 1q:ℚr:ℚ⊢ x ^ q > x ^ r ↔ q < r
  sorryAll goals completed! 🐙

Лема 5.6.9(f) / Вправа 5.6.2

theorem declaration uses 'sorry'Real.ratPow_mul {x y:Real} (hx: x > 0) (hy: y > 0) (q:ℚ) : (x*y)^q = x^q * y^q := byx:Realy:Realhx:x > 0hy:y > 0q:ℚ⊢ (x * y) ^ q = x ^ q * y ^ q
  sorryAll goals completed! 🐙

Вправа 5.6.3

theorem declaration uses 'sorry'Real.pow_even (x:Real) {n:ℕ} (hn: Even n) : x^n ≥ 0 := byx:Realn:ℕhn:Even n⊢ x ^ n ≥ 0 sorryAll goals completed! 🐙

Вправа 5.6.5

theorem declaration uses 'sorry'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 := byx:Realy:Realhx:x > 0hy:y > 0q:ℚhq:q > 0⊢ max (x ^ q) (y ^ q) = max x y ^ q
  sorryAll goals completed! 🐙

Вправа 5.6.5

theorem declaration uses 'sorry'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 := byx:Realy:Realhx:x > 0hy:y > 0q:ℚhq:q > 0⊢ min (x ^ q) (y ^ q) = min x y ^ q
  sorryAll goals completed! 🐙

-- Заключна частина вправи 5.6.5: сформулюйте та доведіть версії наведених вище лем для випадку від’ємних значень q.

end Chapter5