ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-caucvg GIF version

Axiom ax-caucvg 7004
Description: Completeness. Axiom for real and complex numbers, justified by theorem axcaucvg 6974.

A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / 𝑛 of the nth term.

This axiom should not be used directly; instead use caucvgre 9580 (which is the same, but stated in terms of the and 1 / 𝑛 notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.)

Hypotheses
Ref Expression
ax-caucvg.n 𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
ax-caucvg.f (𝜑𝐹:𝑁⟶ℝ)
ax-caucvg.cau (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))
Assertion
Ref Expression
ax-caucvg (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))
Distinct variable groups:   𝑗,𝐹,𝑘,𝑛   𝑥,𝐹,𝑗,𝑘,𝑦   𝑗,𝑁,𝑘,𝑛   𝑦,𝑁,𝑥   𝜑,𝑗,𝑘,𝑛   𝑘,𝑟,𝑛   𝜑,𝑥   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑦,𝑟)   𝐹(𝑟)   𝑁(𝑟)

Detailed syntax breakdown of Axiom ax-caucvg
StepHypRef Expression
1 wph . 2 wff 𝜑
2 cc0 6889 . . . . . 6 class 0
3 vx . . . . . . 7 setvar 𝑥
43cv 1242 . . . . . 6 class 𝑥
5 cltrr 6893 . . . . . 6 class <
62, 4, 5wbr 3764 . . . . 5 wff 0 < 𝑥
7 vj . . . . . . . . . 10 setvar 𝑗
87cv 1242 . . . . . . . . 9 class 𝑗
9 vk . . . . . . . . . 10 setvar 𝑘
109cv 1242 . . . . . . . . 9 class 𝑘
118, 10, 5wbr 3764 . . . . . . . 8 wff 𝑗 < 𝑘
12 cF . . . . . . . . . . 11 class 𝐹
1310, 12cfv 4902 . . . . . . . . . 10 class (𝐹𝑘)
14 vy . . . . . . . . . . . 12 setvar 𝑦
1514cv 1242 . . . . . . . . . . 11 class 𝑦
16 caddc 6892 . . . . . . . . . . 11 class +
1715, 4, 16co 5512 . . . . . . . . . 10 class (𝑦 + 𝑥)
1813, 17, 5wbr 3764 . . . . . . . . 9 wff (𝐹𝑘) < (𝑦 + 𝑥)
1913, 4, 16co 5512 . . . . . . . . . 10 class ((𝐹𝑘) + 𝑥)
2015, 19, 5wbr 3764 . . . . . . . . 9 wff 𝑦 < ((𝐹𝑘) + 𝑥)
2118, 20wa 97 . . . . . . . 8 wff ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥))
2211, 21wi 4 . . . . . . 7 wff (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))
23 cN . . . . . . 7 class 𝑁
2422, 9, 23wral 2306 . . . . . 6 wff 𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))
2524, 7, 23wrex 2307 . . . . 5 wff 𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))
266, 25wi 4 . . . 4 wff (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥))))
27 cr 6888 . . . 4 class
2826, 3, 27wral 2306 . . 3 wff 𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥))))
2928, 14, 27wrex 2307 . 2 wff 𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥))))
301, 29wi 4 1 wff (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))
Colors of variables: wff set class
This axiom is referenced by:  caucvgre  9580
  Copyright terms: Public domain W3C validator