Ordering the reals
Analysis I, Section 5.4: Ordering the reals
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:
-
Ordering on the real line
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 Chapter5Definition 5.4.1 (sequences bounded away from zero with sign). Sequences are indexed to start from zero as this is more convenient for Mathlib purposes.
abbrev BoundedAwayPos (a:ℕ → ℚ) : Prop :=
∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ cDefinition 5.4.1 (sequences bounded away from zero with sign).
abbrev BoundedAwayNeg (a:ℕ → ℚ) : Prop :=
∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -cDefinition 5.4.1 (sequences bounded away from zero with sign).
theorem boundedAwayPos_def (a:ℕ → ℚ) : BoundedAwayPos a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c := a:ℕ → ℚ⊢ BoundedAwayPos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c
All goals completed! 🐙Definition 5.4.1 (sequences bounded away from zero with sign).
theorem boundedAwayNeg_def (a:ℕ → ℚ) : BoundedAwayNeg a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c := a:ℕ → ℚ⊢ BoundedAwayNeg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c
All goals completed! 🐙Examples 5.4.2
example : BoundedAwayPos (fun n ↦ 1 + 10^(-(n:ℤ)-1)) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), (fun n => 1 + 10 ^ (-↑n - 1)) n ≥ 1 n✝:ℕ⊢ (fun n => 1 + 10 ^ (-↑n - 1)) n✝ ≥ 1; n✝:ℕ⊢ 0 ≤ 10 ^ (-↑n✝ - 1); All goals completed! 🐙 ⟩Examples 5.4.2
example : BoundedAwayNeg (fun n ↦ -1 - 10^(-(n:ℤ)-1)) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), (fun n => -1 - 10 ^ (-↑n - 1)) n ≤ -1 n✝:ℕ⊢ (fun n => -1 - 10 ^ (-↑n - 1)) n✝ ≤ -1; n✝:ℕ⊢ 0 ≤ 10 ^ (-↑n✝ - 1); All goals completed! 🐙 ⟩Examples 5.4.2
example : ¬ BoundedAwayPos (fun n ↦ (-1)^n) := ⊢ ¬BoundedAwayPos fun n => (-1) ^ n
c:ℚh1:c > 0h2:∀ (n : ℕ), (fun n => (-1) ^ n) n ≥ c⊢ False; c:ℚh1:c > 0h2:(fun n => (-1) ^ n) 1 ≥ c⊢ False; All goals completed! 🐙Examples 5.4.2
example : ¬ BoundedAwayNeg (fun n ↦ (-1)^n) := ⊢ ¬BoundedAwayNeg fun n => (-1) ^ n
c:ℚh1:c > 0h2:∀ (n : ℕ), (fun n => (-1) ^ n) n ≤ -c⊢ False; c:ℚh1:c > 0h2:(fun n => (-1) ^ n) 0 ≤ -c⊢ False; All goals completed! 🐙Examples 5.4.2
example : BoundedAwayZero (fun n ↦ (-1)^n) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), |(fun n => (-1) ^ n) n| ≥ 1 n✝:ℕ⊢ |(fun n => (-1) ^ n) n✝| ≥ 1; All goals completed! 🐙 ⟩theorem BoundedAwayZero.boundedAwayPos {a:ℕ → ℚ} (ha: BoundedAwayPos a) : BoundedAwayZero a := a:ℕ → ℚha:BoundedAwayPos a⊢ BoundedAwayZero a
a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ |a n| ≥ c; rwa [abs_of_nonneg (a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ 0 ≤ a n All goals completed! 🐙)a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ a n ≥ ctheorem BoundedAwayZero.boundedAwayNeg {a:ℕ → ℚ} (ha: BoundedAwayNeg a) : BoundedAwayZero a := a:ℕ → ℚha:BoundedAwayNeg a⊢ BoundedAwayZero a
a:ℕ → ℚha:BoundedAwayNeg ac:ℚh1:c > 0n:ℕh2:a n ≤ -c⊢ |a n| ≥ c; a:ℕ → ℚha:BoundedAwayNeg ac:ℚh1:c > 0n:ℕh2:a n ≤ -c⊢ -a n ≥ c; All goals completed! 🐙theorem not_boundedAwayPos_boundedAwayNeg {a:ℕ → ℚ} : ¬ (BoundedAwayPos a ∧ BoundedAwayNeg a) := a:ℕ → ℚ⊢ ¬(BoundedAwayPos a ∧ BoundedAwayNeg a)
a:ℕ → ℚw✝¹:ℚleft✝¹:w✝¹ > 0h2:∀ (n : ℕ), a n ≥ w✝¹w✝:ℚleft✝:w✝ > 0h4:∀ (n : ℕ), a n ≤ -w✝⊢ False; All goals completed! 🐙abbrev Real.IsPos (x:Real) : Prop :=
∃ a:ℕ → ℚ, BoundedAwayPos a ∧ (a:Sequence).IsCauchy ∧ x = LIM aabbrev Real.IsNeg (x:Real) : Prop :=
∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM atheorem Real.isPos_def (x:Real) :
IsPos x ↔ ∃ a:ℕ → ℚ, BoundedAwayPos a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := x:Real⊢ x.IsPos ↔ ∃ a, BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a All goals completed! 🐙theorem Real.isNeg_def (x:Real) :
IsNeg x ↔ ∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := x:Real⊢ x.IsNeg ↔ ∃ a, BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem declaration uses `sorry`Real.trichotomous (x:Real) : x = 0 ∨ x.IsPos ∨ x.IsNeg := x:Real⊢ x = 0 ∨ x.IsPos ∨ x.IsNeg All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem declaration uses `sorry`Real.not_zero_pos (x:Real) : ¬(x = 0 ∧ x.IsPos) := x:Real⊢ ¬(x = 0 ∧ x.IsPos) All goals completed! 🐙theorem Real.nonzero_of_pos {x:Real} (hx: x.IsPos) : x ≠ 0 := x:Realhx:x.IsPos⊢ x ≠ 0
x:Realhx:x.IsPosthis:¬(x = 0 ∧ x.IsPos) := not_zero_pos x⊢ x ≠ 0
All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem declaration uses `sorry`Real.not_zero_neg (x:Real) : ¬(x = 0 ∧ x.IsNeg) := x:Real⊢ ¬(x = 0 ∧ x.IsNeg) All goals completed! 🐙theorem Real.nonzero_of_neg {x:Real} (hx: x.IsNeg) : x ≠ 0 := x:Realhx:x.IsNeg⊢ x ≠ 0
x:Realhx:x.IsNegthis:¬(x = 0 ∧ x.IsNeg) := not_zero_neg x⊢ x ≠ 0
All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem declaration uses `sorry`Real.not_pos_neg (x:Real) : ¬(x.IsPos ∧ x.IsNeg) := x:Real⊢ ¬(x.IsPos ∧ x.IsNeg) All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
@[simp]
theorem declaration uses `sorry`Real.neg_iff_pos_of_neg (x:Real) : x.IsNeg ↔ (-x).IsPos := x:Real⊢ x.IsNeg ↔ (-x).IsPos All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem declaration uses `sorry`Real.pos_add {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x+y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x + y).IsPos All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem declaration uses `sorry`Real.pos_mul {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x*y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x * y).IsPos All goals completed! 🐙theorem declaration uses `sorry`Real.pos_of_coe (q:ℚ) : (q:Real).IsPos ↔ q > 0 := q:ℚ⊢ (↑q).IsPos ↔ q > 0 All goals completed! 🐙theorem declaration uses `sorry`Real.neg_of_coe (q:ℚ) : (q:Real).IsNeg ↔ q < 0 := q:ℚ⊢ (↑q).IsNeg ↔ q < 0 All goals completed! 🐙open Classical in
/-- Need to use classical logic here because isPos and isNeg are not decidable -/
noncomputable abbrev Real.abs (x:Real) : Real := if x.IsPos then x else (if x.IsNeg then -x else 0)Definition 5.4.5 (absolute value)
@[simp]
theorem Real.abs_of_pos (x:Real) (hx: x.IsPos) : abs x = x := x:Realhx:x.IsPos⊢ x.abs = x
All goals completed! 🐙Definition 5.4.5 (absolute value)
@[simp]
theorem Real.abs_of_neg (x:Real) (hx: x.IsNeg) : abs x = -x := x:Realhx:x.IsNeg⊢ x.abs = -x
have : ¬x.IsPos := x:Realhx:x.IsNeg⊢ x.abs = -x x:Realhx:x.IsNegthis:¬(x.IsPos ∧ x.IsNeg) := not_pos_neg x⊢ ¬x.IsPos; All goals completed! 🐙
All goals completed! 🐙Definition 5.4.5 (absolute value)
@[simp]
theorem Real.abs_of_zero : abs 0 = 0 := ⊢ abs 0 = 0
have hpos: ¬(0:Real).IsPos := ⊢ abs 0 = 0 this:¬(0 = 0 ∧ IsPos 0) := not_zero_pos 0⊢ ¬IsPos 0; All goals completed! 🐙
have hneg: ¬(0:Real).IsNeg := ⊢ abs 0 = 0 hpos:¬IsPos 0 :=
have this := not_zero_pos 0;
Eq.mpr
(id
(Eq.trans not_exists._simp_1
(forall_congr fun x =>
Eq.trans not_and._simp_1
(Eq.trans (Eq.trans (implies_congr (Eq.refl (BoundedAwayPos x)) not_and._simp_1) forall_exists_index._simp_1)
(forall_congr fun x_1 =>
Eq.trans
(implies_congr (congr (congrArg And gt_iff_lt._simp_1) (forall_congr fun n => ge_iff_le._simp_1))
(Eq.refl ((↑x).IsCauchy → ¬0 = LIM x)))
and_imp._simp_1)))))
(Eq.mp
(Eq.trans
(Eq.trans (congrArg Not (Eq.trans (congrFun' (congrArg And (eq_self 0)) (IsPos 0)) (true_and (IsPos 0))))
not_exists._simp_1)
(forall_congr fun x =>
Eq.trans not_and._simp_1
(Eq.trans (Eq.trans (implies_congr (Eq.refl (BoundedAwayPos x)) not_and._simp_1) forall_exists_index._simp_1)
(forall_congr fun x_1 =>
Eq.trans
(implies_congr (congr (congrArg And gt_iff_lt._simp_1) (forall_congr fun n => ge_iff_le._simp_1))
(Eq.refl ((↑x).IsCauchy → ¬0 = LIM x)))
and_imp._simp_1))))
this)this:¬(0 = 0 ∧ IsNeg 0) := not_zero_neg 0⊢ ¬IsNeg 0; All goals completed! 🐙
All goals completed! 🐙Definition 5.4.6 (Ordering of the reals)
instance Real.instLE : LE Real where
le x y := (x < y) ∨ (x = y)theorem Real.lt_iff (x y:Real) : x < y ↔ (x-y).IsNeg := x:Realy:Real⊢ x < y ↔ (x - y).IsNeg All goals completed! 🐙theorem Real.le_iff (x y:Real) : x ≤ y ↔ (x < y) ∨ (x = y) := x:Realy:Real⊢ x ≤ y ↔ x < y ∨ x = y All goals completed! 🐙theorem declaration uses `sorry`Real.gt_iff (x y:Real) : x > y ↔ (x-y).IsPos := x:Realy:Real⊢ x > y ↔ (x - y).IsPos All goals completed! 🐙theorem declaration uses `sorry`Real.ge_iff (x y:Real) : x ≥ y ↔ (x > y) ∨ (x = y) := x:Realy:Real⊢ x ≥ y ↔ x > y ∨ x = y All goals completed! 🐙theorem declaration uses `sorry`Real.lt_of_coe (q q':ℚ): q < q' ↔ (q:Real) < (q':Real) := q:ℚq':ℚ⊢ q < q' ↔ ↑q < ↑q' All goals completed! 🐙theorem Real.gt_of_coe (q q':ℚ): q > q' ↔ (q:Real) > (q':Real) := Real.lt_of_coe _ _theorem declaration uses `sorry`Real.isPos_iff (x:Real) : x.IsPos ↔ x > 0 := x:Real⊢ x.IsPos ↔ x > 0 All goals completed! 🐙theorem declaration uses `sorry`Real.isNeg_iff (x:Real) : x.IsNeg ↔ x < 0 := x:Real⊢ x.IsNeg ↔ x < 0 All goals completed! 🐙Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2
theorem declaration uses `sorry`Real.trichotomous' (x y:Real) : x > y ∨ x < y ∨ x = y := x:Realy:Real⊢ x > y ∨ x < y ∨ x = y All goals completed! 🐙Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2
theorem declaration uses `sorry`Real.not_gt_and_lt (x y:Real) : ¬ (x > y ∧ x < y):= x:Realy:Real⊢ ¬(x > y ∧ x < y) All goals completed! 🐙Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2
theorem declaration uses `sorry`Real.not_gt_and_eq (x y:Real) : ¬ (x > y ∧ x = y):= x:Realy:Real⊢ ¬(x > y ∧ x = y) All goals completed! 🐙Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2
theorem declaration uses `sorry`Real.not_lt_and_eq (x y:Real) : ¬ (x < y ∧ x = y):= x:Realy:Real⊢ ¬(x < y ∧ x = y) All goals completed! 🐙Proposition 5.4.7(b) (order is anti-symmetric) / Exercise 5.4.2
theorem declaration uses `sorry`Real.antisymm (x y:Real) : x < y ↔ y > x := x:Realy:Real⊢ x < y ↔ y > x All goals completed! 🐙Proposition 5.4.7(c) (order is transitive) / Exercise 5.4.2
theorem declaration uses `sorry`Real.lt_trans {x y z:Real} (hxy: x < y) (hyz: y < z) : x < z := x:Realy:Realz:Realhxy:x < yhyz:y < z⊢ x < z All goals completed! 🐙Proposition 5.4.7(d) (addition preserves order) / Exercise 5.4.2
theorem declaration uses `sorry`Real.add_lt_add_right {x y:Real} (z:Real) (hxy: x < y) : x + z < y + z := x:Realy:Realz:Realhxy:x < y⊢ x + z < y + z All goals completed! 🐙Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2
theorem Real.mul_lt_mul_right {x y z:Real} (hxy: x < y) (hz: z.IsPos) : x * z < y * z := x:Realy:Realz:Realhxy:x < yhz:z.IsPos⊢ x * z < y * z
x:Realy:Realz:Realhxy:(y - x).IsPoshz:z.IsPos⊢ (y * z - x * z).IsPos; x:Realy:Realz:Realhxy:(y - x).IsPoshz:z.IsPos⊢ y * z - x * z = (y - x) * z; All goals completed! 🐙Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2
theorem declaration uses `sorry`Real.mul_le_mul_left {x y z:Real} (hxy: x ≤ y) (hz: z.IsPos) : z * x ≤ z * y := x:Realy:Realz:Realhxy:x ≤ yhz:z.IsPos⊢ z * x ≤ z * y All goals completed! 🐙theorem declaration uses `sorry`Real.mul_pos_neg {x y:Real} (hx: x.IsPos) (hy: y.IsNeg) : (x * y).IsNeg := x:Realy:Realhx:x.IsPoshy:y.IsNeg⊢ (x * y).IsNeg
All goals completed! 🐙open Classical in
/--
(Not from textbook) Real has the structure of a linear ordering. The order is not computable,
and so classical logic is required to impose decidability.
-/
noncomputable instance declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`Real.instLinearOrder : LinearOrder Real where
le_refl := sorry
le_trans := sorry
lt_iff_le_not_ge := sorry
le_antisymm := sorry
le_total := sorry
toDecidableLE := Classical.decRel _(Not from textbook) Linear Orders come with a definition of absolute value |.| Show that it agrees with our earlier definition.
theorem declaration uses `sorry`Real.abs_eq_abs (x:Real) : |x| = abs x := x:Real⊢ |x| = x.abs All goals completed! 🐙Proposition 5.4.8
theorem Real.inv_of_pos {x:Real} (hx: x.IsPos) : x⁻¹.IsPos := x:Realhx:x.IsPos⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1⊢ x⁻¹.IsPos
have hinv_non: x⁻¹ ≠ 0 := x:Realhx:x.IsPos⊢ x⁻¹.IsPos x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ = 0⊢ x⁻¹ * x ≠ 1; All goals completed! 🐙
have hnonneg : ¬x⁻¹.IsNeg := x:Realhx:x.IsPos⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:x⁻¹ ≠ 0 :=
Mathlib.Tactic.Contrapose.contrapose₃
(id fun hident =>
of_eq_true
(Eq.trans (congrFun' (congrArg Ne (Eq.trans (congrFun' (congrArg HMul.hMul hident) x) (zero_mul x))) 1)
(Eq.trans (congrArg Not zero_ne_one._simp_1) not_false_eq_true)))
hidenth:x⁻¹.IsNeg⊢ False
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:x⁻¹ ≠ 0 :=
Mathlib.Tactic.Contrapose.contrapose₃
(id fun hident =>
of_eq_true
(Eq.trans (congrFun' (congrArg Ne (Eq.trans (congrFun' (congrArg HMul.hMul hident) x) (zero_mul x))) 1)
(Eq.trans (congrArg Not zero_ne_one._simp_1) not_false_eq_true)))
hidenth:x⁻¹.IsNegthis:(x * x⁻¹).IsNeg⊢ False
have id : -(1:Real) = (-1:ℚ) := x:Realhx:x.IsPos⊢ x⁻¹.IsPos All goals completed! 🐙
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:x⁻¹ ≠ 0 :=
Mathlib.Tactic.Contrapose.contrapose₃
(id fun hident =>
of_eq_true
(Eq.trans (congrFun' (congrArg Ne (Eq.trans (congrFun' (congrArg HMul.hMul hident) x) (zero_mul x))) 1)
(Eq.trans (congrArg Not zero_ne_one._simp_1) not_false_eq_true)))
hidenth:x⁻¹.IsNegid:-1 = ↑(-1) := of_eq_true (Eq.trans (congrArg (Eq (-1)) (Eq.trans (Rat.cast_neg 1) (congrArg Neg.neg Rat.cast_one))) (eq_self (-1)))this:-1 > 0⊢ False
All goals completed! 🐙
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:x⁻¹ ≠ 0 :=
Mathlib.Tactic.Contrapose.contrapose₃
(id fun hident =>
of_eq_true
(Eq.trans (congrFun' (congrArg Ne (Eq.trans (congrFun' (congrArg HMul.hMul hident) x) (zero_mul x))) 1)
(Eq.trans (congrArg Not zero_ne_one._simp_1) not_false_eq_true)))
hidenthnonneg:¬x⁻¹.IsNeg :=
fun h =>
have id :=
of_eq_true
(Eq.trans (congrArg (Eq (-1)) (Eq.trans (Rat.cast_neg 1) (congrArg Neg.neg Rat.cast_one))) (eq_self (-1)));
False.elim
(Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Tactic.Ring.neg_add
(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.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Tactic.Ring.neg_add
(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.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(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.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Tactic.Linarith.sub_neg_of_lt
(Eq.mp
(Eq.trans (Eq.trans (congrArg IsNeg (self_mul_inv hnon)) (neg_iff_pos_of_neg._simp_1 1))
(Eq.trans (congrArg IsPos id) (inv_of_pos._simp_1 (-1))))
(mul_pos_neg hx h))))))trich:x⁻¹ = 0 ∨ x⁻¹.IsPos ∨ x⁻¹.IsNeg := trichotomous x⁻¹⊢ x⁻¹.IsPos
All goals completed! 🐙theorem declaration uses `sorry`Real.div_of_pos {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x/y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x / y).IsPos All goals completed! 🐙theorem Real.inv_of_gt {x y:Real} (hx: x.IsPos) (hy: y.IsPos) (hxy: x > y) : x⁻¹ < y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > y⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPos⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPosthis:y⁻¹ ≤ x⁻¹⊢ False
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPosthis✝:y⁻¹ ≤ x⁻¹this:1 > 1 :=
Trans.trans
(Trans.trans (Trans.trans (Eq.symm (self_mul_inv hxnon)) (mul_lt_mul_right hxy hxinv)) (mul_le_mul_left this✝ hy))
(self_mul_inv hynon)⊢ False
All goals completed! 🐙(Not from textbook) Real has the structure of a strict ordered ring.
instance declaration uses `sorry`Real.instIsStrictOrderedRing : IsStrictOrderedRing Real where
add_le_add_left := ⊢ ∀ (a b : Real), a ≤ b → ∀ (c : Real), a + c ≤ b + c All goals completed! 🐙
add_le_add_right := ⊢ ∀ (a b : Real), a ≤ b → ∀ (c : Real), c + a ≤ c + b All goals completed! 🐙
mul_lt_mul_of_pos_left := ⊢ ∀ ⦃a : Real⦄, 0 < a → ∀ ⦃b c : Real⦄, b < c → a * b < a * c All goals completed! 🐙
mul_lt_mul_of_pos_right := ⊢ ∀ ⦃c : Real⦄, 0 < c → ∀ ⦃a b : Real⦄, a < b → a * c < b * c All goals completed! 🐙
le_of_add_le_add_left := ⊢ ∀ (a b c : Real), a + b ≤ a + c → b ≤ c All goals completed! 🐙
zero_le_one := ⊢ 0 ≤ 1 All goals completed! 🐙Proposition 5.4.9 (The non-negative reals are closed)
theorem Real.LIM_of_nonneg {a: ℕ → ℚ} (ha: ∀ n, a n ≥ 0) (hcauchy: (a:Sequence).IsCauchy) :
LIM a ≥ 0 := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
-- This proof is written to follow the structure of the original text.
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyhlim:LIM a < 0⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ahlim:x < 0⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ahlim:∃ a, BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a⊢ False; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb:BoundedAwayNeg bhb_cauchy:(↑b).IsCauchyhlim:x = LIM b⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb:∃ c > 0, ∀ (n : ℕ), b n ≤ -chb_cauchy:(↑b).IsCauchyhlim:x = LIM b⊢ False; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -c⊢ False
have claim1 : ∀ n, ¬ (c/2).Close (a n) (b n) := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cn:ℕ⊢ ¬(c / 2).Close (a n) (b n); a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cn:ℕha:a n ≥ 0⊢ ¬(c / 2).Close (a n) (b n); a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ ¬(c / 2).Close (a n) (b n)
a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c / 2 < |a n - b n|
calc
_ < c := a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c / 2 < c All goals completed! 🐙
_ ≤ a n - b n := a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c ≤ a n - b n All goals completed! 🐙
_ ≤ _ := le_abs_self _
have claim2 : ¬(c/2).EventuallyClose (a:Sequence) (b:Sequence) := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:(c / 2).EventuallyClose ↑a ↑b⊢ ∃ n, (c / 2).Close (a n) (b n); a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∃ N, ∀ n ≥ N, |a n - b n| ≤ c / 2⊢ ∃ n, (c / 2).Close (a n) (b n); a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1✝:∃ N, ∀ n ≥ N, |a n - b n| ≤ c / 2N:ℕclaim1:∀ n ≥ N, |a n - b n| ≤ c / 2⊢ (c / 2).Close (a N) (b N); All goals completed! 🐙
have claim3 : ¬Sequence.Equiv a b := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0 a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(c / 2).Close (a n) (b n) :=
fun n =>
Eq.mpr (id (Eq.trans (congrArg Not (LIM_of_nonneg._simp_1 (c / 2) (a n) (b n))) not_le._simp_1))
(Trans.trans
(Trans.trans
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_zero_add (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))
(Mathlib.Tactic.Ring.zero_mul (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
(Mathlib.Tactic.Ring.zero_mul (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_add_overlap
(Mathlib.Tactic.Ring.add_overlap_pf c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 2))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(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.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt cpos)
(Eq.mp
(congrArg (fun _a => _a ≤ 0)
(Mathlib.Tactic.CancelDenoms.sub_subst rfl
(Mathlib.Tactic.CancelDenoms.div_subst rfl
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))
(Eq.refl (Nat.mul 2 1)) (Eq.refl 2))))))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)) (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))))
(Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)) (Eq.refl false)))))))
(le_of_not_gt fun a_1 =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf (a n))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (a n) (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.add_pf_zero_add (a n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (b n))
(Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Eq.refl (Int.ofNat 1)))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_lt (b n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_zero_add (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_lt (a n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
(Mathlib.Tactic.Ring.add_pf_zero_add
(b n ^ Nat.rawCast 1 * Nat.rawCast 1 + (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (a n))
(Mathlib.Tactic.Ring.atom_pf (b n))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (b n) (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.add_pf_add_lt (a n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_zero_add
(b n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_add_lt (a n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_lt (b n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
(Mathlib.Tactic.Ring.add_pf_zero_add (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (a n) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(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.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (b n) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_le_of_neg
(Mathlib.Tactic.Linarith.add_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (ha n))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (hb n)))
(Mathlib.Tactic.Linarith.sub_neg_of_lt a_1)))))
(le_abs_self (a n - b n)))claim2:Sequence.Equiv a b⊢ (c / 2).EventuallyClose ↑a ↑b; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(c / 2).Close (a n) (b n) :=
fun n =>
Eq.mpr (id (Eq.trans (congrArg Not (LIM_of_nonneg._simp_1 (c / 2) (a n) (b n))) not_le._simp_1))
(Trans.trans
(Trans.trans
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_zero_add (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))
(Mathlib.Tactic.Ring.zero_mul (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
(Mathlib.Tactic.Ring.zero_mul (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_add_overlap
(Mathlib.Tactic.Ring.add_overlap_pf c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 2))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(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.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt cpos)
(Eq.mp
(congrArg (fun _a => _a ≤ 0)
(Mathlib.Tactic.CancelDenoms.sub_subst rfl
(Mathlib.Tactic.CancelDenoms.div_subst rfl
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))
(Eq.refl (Nat.mul 2 1)) (Eq.refl 2))))))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)) (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))))
(Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)) (Eq.refl false)))))))
(le_of_not_gt fun a_1 =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf (a n))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (a n) (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.add_pf_zero_add (a n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (b n))
(Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Eq.refl (Int.ofNat 1)))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_lt (b n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_zero_add (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_lt (a n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
(Mathlib.Tactic.Ring.add_pf_zero_add
(b n ^ Nat.rawCast 1 * Nat.rawCast 1 + (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (a n))
(Mathlib.Tactic.Ring.atom_pf (b n))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (b n) (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.add_pf_add_lt (a n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_zero_add
(b n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_add_lt (a n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_lt (b n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
(Mathlib.Tactic.Ring.add_pf_zero_add (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (a n) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(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.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (b n) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_le_of_neg
(Mathlib.Tactic.Linarith.add_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (ha n))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (hb n)))
(Mathlib.Tactic.Linarith.sub_neg_of_lt a_1)))))
(le_abs_self (a n - b n)))claim2:∀ ε > 0, ε.EventuallyClose ↑a ↑b⊢ (c / 2).EventuallyClose ↑a ↑b; All goals completed! 🐙
simp_rw a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Real := LIM ab:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(c / 2).Close (a n) (b n) :=
fun n =>
Eq.mpr (id (Eq.trans (congrArg Not (LIM_of_nonneg._simp_1 (c / 2) (a n) (b n))) not_le._simp_1))
(Trans.trans
(Trans.trans
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_zero_add (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))
(Mathlib.Tactic.Ring.zero_mul (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
(Mathlib.Tactic.Ring.zero_mul (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_add_overlap
(Mathlib.Tactic.Ring.add_overlap_pf c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 2))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(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.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt cpos)
(Eq.mp
(congrArg (fun _a => _a ≤ 0)
(Mathlib.Tactic.CancelDenoms.sub_subst rfl
(Mathlib.Tactic.CancelDenoms.div_subst rfl
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))
(Eq.refl (Nat.mul 2 1)) (Eq.refl 2))))))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)) (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2))))))
(Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)) (Eq.refl false)))))))
(le_of_not_gt fun a_1 =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))
(Mathlib.Tactic.Ring.atom_pf (a n))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (a n) (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.add_pf_zero_add (a n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (b n))
(Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1))
(Eq.refl (Int.ofNat 1)))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_lt (b n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_zero_add (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_lt (a n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
(Mathlib.Tactic.Ring.add_pf_zero_add
(b n ^ Nat.rawCast 1 * Nat.rawCast 1 + (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (a n))
(Mathlib.Tactic.Ring.atom_pf (b n))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (b n) (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.add_pf_add_lt (a n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_zero_add
(b n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
(Mathlib.Tactic.Ring.atom_pf c)
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul c (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.add_pf_add_lt (a n ^ Nat.rawCast 1 * Nat.rawCast 1)
(Mathlib.Tactic.Ring.add_pf_add_lt (b n ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
(Mathlib.Tactic.Ring.add_pf_zero_add (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (a n) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(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.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (b n) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℚ 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℚ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 0)))))
(Mathlib.Tactic.Linarith.add_lt_of_le_of_neg
(Mathlib.Tactic.Linarith.add_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (ha n))
(Mathlib.Tactic.Linarith.sub_nonpos_of_le (hb n)))
(Mathlib.Tactic.Linarith.sub_neg_of_lt a_1)))))
(le_abs_self (a n - b n)))claim2:¬(c / 2).EventuallyClose ↑a ↑b :=
Mathlib.Tactic.Contrapose.contrapose₃
(Eq.mpr
(id
(implies_congr (Eq.refl ((c / 2).EventuallyClose ↑a ↑b))
(Eq.trans (Mathlib.Tactic.Push.not_forall_eq fun n => ¬(c / 2).Close (a n) (b n))
(congrArg Exists (funext fun n => Classical.not_not._simp_2)))))
fun claim1 =>
Exists.imp (fun N claim1 => LIM_of_nonneg._proof_2 b c N claim1)
(Eq.mp (congrArg (fun _a => _a) (propext (Rat.eventuallyClose_iff (c / 2) a b))) claim1))
claim1claim3:¬Sequence.Equiv a b :=
Mathlib.Tactic.Contrapose.contrapose₄
(fun claim2 => Eq.mp (congrArg (fun _a => _a) (propext (Sequence.equiv_def a b))) claim2 (c / 2) (half_pos cpos))
claim2⊢ Falsex, LIM_eq_LIM hcauchy hb_cauchy] at hlim
All goals completed! 🐙Corollary 5.4.10
theorem Real.LIM_mono {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy)
(hmono: ∀ n, a n ≤ b n) :
LIM a ≤ LIM b := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b n⊢ LIM a ≤ LIM b
-- This proof is written to follow the structure of the original text.
have := LIM_of_nonneg (a := b - a) (a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b n⊢ ∀ (n : ℕ), (b - a) n ≥ 0 a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b nn:ℕ⊢ (b - a) n ≥ 0; All goals completed! 🐙) (Sequence.IsCauchy.sub hb ha)
a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b nthis:LIM b - LIM a ≥ 0⊢ LIM a ≤ LIM b; All goals completed! 🐙Remark 5.4.11 -
theorem declaration uses `sorry`Real.LIM_mono_fail :
∃ (a b:ℕ → ℚ), (a:Sequence).IsCauchy
∧ (b:Sequence).IsCauchy
∧ (∀ n, a n > b n)
∧ ¬LIM a > LIM b := ⊢ ∃ a b, (↑a).IsCauchy ∧ (↑b).IsCauchy ∧ (∀ (n : ℕ), a n > b n) ∧ ¬LIM a > LIM b
⊢ ∃ b,
(↑fun n => 1 + 1 / (↑n + 1)).IsCauchy ∧
(↑b).IsCauchy ∧ (∀ (n : ℕ), (fun n => 1 + 1 / (↑n + 1)) n > b n) ∧ ¬(LIM fun n => 1 + 1 / (↑n + 1)) > LIM b
⊢ (↑fun n => 1 + 1 / (↑n + 1)).IsCauchy ∧
(↑fun n => 1 - 1 / (↑n + 1)).IsCauchy ∧
(∀ (n : ℕ), 1 + 1 / (↑n + 1) > (fun n => 1 - 1 / (↑n + 1)) n) ∧
¬(LIM fun n => 1 + 1 / (↑n + 1)) > LIM fun n => 1 - 1 / (↑n + 1)
All goals completed! 🐙Proposition 5.4.12 (Bounding reals by rationals)
theorem Real.exists_rat_le_and_nat_gt {x:Real} (hx: x.IsPos) :
(∃ q:ℚ, q > 0 ∧ (q:Real) ≤ x) ∧ ∃ N:ℕ, x < (N:Real) := x:Realhx:x.IsPos⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
-- This proof is written to follow the structure of the original text.
x:Realhx:∃ a, BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhbound:BoundedAwayPos ahcauchy:(↑a).IsCauchyheq:x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhbound:∃ c > 0, ∀ (n : ℕ), a n ≥ chcauchy:(↑a).IsCauchyheq:x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ q⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qthis:(↑a).IsBounded := Sequence.isBounded_of_isCauchy hcauchy⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qthis:∃ M ≥ 0, (↑a).BoundedBy M⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:(↑a).BoundedBy r⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q ≤ xx:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q ≤ x x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q = LIM fun x => q
All goals completed! 🐙
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x < ↑N
calc
x ≤ r := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x ≤ ↑r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x ≤ LIM fun x => r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ∀ (n : ℕ), a n ≤ r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑Nn:ℕ⊢ a n ≤ r; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0N:ℕhN:r < ↑Nn:ℕthis:|if 0 ≤ ↑n then a (↑n).toNat else 0| ≤ r⊢ a n ≤ r; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0N:ℕhN:r < ↑Nn:ℕthis:|a n| ≤ r⊢ a n ≤ r
All goals completed! 🐙
_ < ((N:ℚ):Real) := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ↑r < ↑↑N All goals completed! 🐙
_ = N := rflCorollary 5.4.13 (Archimedean property )
theorem Real.le_mul {ε:Real} (hε: ε.IsPos) (x:Real) : ∃ M:ℕ, M > 0 ∧ M * ε > x := ε:Realhε:ε.IsPosx:Real⊢ ∃ M > 0, ↑M * ε > x
-- This proof is written to follow the structure of the original text.
ε:Realhε:ε.IsPos⊢ ∃ M > 0, ↑M * ε > 0ε:Realhε:ε.IsPosx:Realhx:x.IsPos⊢ ∃ M > 0, ↑M * ε > xε:Realhε:ε.IsPosx:Realhx:x.IsNeg⊢ ∃ M > 0, ↑M * ε > x
ε:Realhε:ε.IsPos⊢ ∃ M > 0, ↑M * ε > 0 ε:Realhε:ε.IsPos⊢ 1 > 0 ∧ ↑1 * ε > 0; All goals completed! 🐙
ε:Realhε:ε.IsPosx:Realhx:x.IsPos⊢ ∃ M > 0, ↑M * ε > x ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑N⊢ ∃ M > 0, ↑M * ε > x
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := N + 1⊢ ∃ M > 0, ↑M * ε > x; refine ⟨ M, ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := N + 1⊢ M > 0 All goals completed! 🐙, ?_ ⟩
replace hN : x/ε < M := hN.trans (ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := N + 1⊢ ↑N < ↑M All goals completed! 🐙)
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕM:ℕ := N + 1hN:x / ε < ↑M :=
LT.lt.trans _fvar.1089667
(of_eq_true
(Eq.trans
(Eq.trans (congrArg (LT.lt ↑N) (Eq.trans (Nat.cast_add N 1) (congrArg (HAdd.hAdd ↑N) Nat.cast_one)))
(lt_add_iff_pos_right._simp_1 ↑N))
zero_lt_one._simp_1))⊢ x < ↑M * ε
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕM:ℕ := N + 1hN:x / ε < ↑M :=
LT.lt.trans _fvar.1089667
(of_eq_true
(Eq.trans
(Eq.trans (congrArg (LT.lt ↑N) (Eq.trans (Nat.cast_add N 1) (congrArg (HAdd.hAdd ↑N) Nat.cast_one)))
(lt_add_iff_pos_right._simp_1 ↑N))
zero_lt_one._simp_1))⊢ x = x / ε * ε
ε:Realhε:ε > 0x:Realhx:x.IsPosN:ℕM:ℕ := N + 1hN:x / ε < ↑M⊢ x = x / ε * ε; All goals completed! 🐙
ε:Realhε:ε.IsPosx:Realhx:x.IsNeg⊢ 1 > 0 ∧ ↑1 * ε > x; ε:Realx:Realhε:0 < εhx:x < 0⊢ x < ε; All goals completed! 🐙Proposition 5.4.14 / Exercise 5.4.5
theorem declaration uses `sorry`Real.rat_between {x y:Real} (hxy: x < y) : ∃ q:ℚ, x < (q:Real) ∧ (q:Real) < y := x:Realy:Realhxy:x < y⊢ ∃ q, x < ↑q ∧ ↑q < y All goals completed! 🐙Exercise 5.4.3
theorem declaration uses `sorry`Real.floor_exist (x:Real) : ∃! n:ℤ, (n:Real) ≤ x ∧ x < (n:Real)+1 := x:Real⊢ ∃! n, ↑n ≤ x ∧ x < ↑n + 1 All goals completed! 🐙Exercise 5.4.4
theorem declaration uses `sorry`Real.exist_inv_nat_le {x:Real} (hx: x.IsPos) : ∃ N:ℤ, N>0 ∧ (N:Real)⁻¹ < x := x:Realhx:x.IsPos⊢ ∃ N > 0, (↑N)⁻¹ < x All goals completed! 🐙Exercise 5.4.6
theorem declaration uses `sorry`Real.dist_lt_iff (ε x y:Real) : |x-y| < ε ↔ y-ε < x ∧ x < y+ε := ε:Realx:Realy:Real⊢ |x - y| < ε ↔ y - ε < x ∧ x < y + ε All goals completed! 🐙Exercise 5.4.6
theorem declaration uses `sorry`Real.dist_le_iff (ε x y:Real) : |x-y| ≤ ε ↔ y-ε ≤ x ∧ x ≤ y+ε := ε:Realx:Realy:Real⊢ |x - y| ≤ ε ↔ y - ε ≤ x ∧ x ≤ y + ε All goals completed! 🐙Exercise 5.4.7
theorem declaration uses `sorry`Real.le_add_eps_iff (x y:Real) : (∀ ε > 0, x ≤ y+ε) ↔ x ≤ y := x:Realy:Real⊢ (∀ ε > 0, x ≤ y + ε) ↔ x ≤ y All goals completed! 🐙Exercise 5.4.7
theorem declaration uses `sorry`Real.dist_le_eps_iff (x y:Real) : (∀ ε > 0, |x-y| ≤ ε) ↔ x = y := x:Realy:Real⊢ (∀ ε > 0, |x - y| ≤ ε) ↔ x = y All goals completed! 🐙Exercise 5.4.8
theorem declaration uses `sorry`Real.LIM_of_le {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∀ n, a n ≤ x) :
LIM a ≤ x := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyh:∀ (n : ℕ), ↑(a n) ≤ x⊢ LIM a ≤ x All goals completed! 🐙Exercise 5.4.8
theorem declaration uses `sorry`Real.LIM_of_ge {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∀ n, a n ≥ x) :
LIM a ≥ x := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyh:∀ (n : ℕ), ↑(a n) ≥ x⊢ LIM a ≥ x All goals completed! 🐙theorem Real.max_eq (x y:Real) : max x y = if x ≥ y then x else y := max_def' x ytheorem Real.min_eq (x y:Real) : min x y = if x ≤ y then x else y := rflExercise 5.4.9
theorem declaration uses `sorry`Real.neg_max (x y:Real) : max x y = - min (-x) (-y) := x:Realy:Real⊢ max x y = -min (-x) (-y) All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.neg_min (x y:Real) : min x y = - max (-x) (-y) := x:Realy:Real⊢ min x y = -max (-x) (-y) All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.max_comm (x y:Real) : max x y = max y x := x:Realy:Real⊢ max x y = max y x All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.max_self (x:Real) : max x x = x := x:Real⊢ max x x = x All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.max_add (x y z:Real) : max (x + z) (y + z) = max x y + z := x:Realy:Realz:Real⊢ max (x + z) (y + z) = max x y + z All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.max_mul (x y :Real) {z:Real} (hz: z.IsPos) : max (x * z) (y * z) = max x y * z := x:Realy:Realz:Realhz:z.IsPos⊢ max (x * z) (y * z) = max x y * z
All goals completed! 🐙/- Additional exercise: What happens if z is negative? -/Exercise 5.4.9
theorem declaration uses `sorry`Real.min_comm (x y:Real) : min x y = min y x := x:Realy:Real⊢ min x y = min y x All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.min_self (x:Real) : min x x = x := x:Real⊢ min x x = x All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.min_add (x y z:Real) : min (x + z) (y + z) = min x y + z := x:Realy:Realz:Real⊢ min (x + z) (y + z) = min x y + z All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.min_mul (x y :Real) {z:Real} (hz: z.IsPos) : min (x * z) (y * z) = min x y * z := x:Realy:Realz:Realhz:z.IsPos⊢ min (x * z) (y * z) = min x y * z
All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.inv_max {x y :Real} (hx:x.IsPos) (hy:y.IsPos) : (max x y)⁻¹ = min x⁻¹ y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (max x y)⁻¹ = min x⁻¹ y⁻¹ All goals completed! 🐙Exercise 5.4.9
theorem declaration uses `sorry`Real.inv_min {x y :Real} (hx:x.IsPos) (hy:y.IsPos) : (min x y)⁻¹ = max x⁻¹ y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (min x y)⁻¹ = max x⁻¹ y⁻¹ All goals completed! 🐙Not from textbook: the rationals map as an ordered ring homomorphism into the reals.
abbrev declaration uses `sorry`Real.ratCast_ordered_hom : ℚ →+*o Real where
toRingHom := ratCast_hom
monotone' := ⊢ Monotone (↑↑ratCast_hom).toFun All goals completed! 🐙end Chapter5