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

Axiom ax-caucvg 7931
Description: Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 7899.

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 10990 (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 7811 . . . . . 6 class 0
3 vx . . . . . . 7 setvar π‘₯
43cv 1352 . . . . . 6 class π‘₯
5 cltrr 7815 . . . . . 6 class <ℝ
62, 4, 5wbr 4004 . . . . 5 wff 0 <ℝ π‘₯
7 vj . . . . . . . . . 10 setvar 𝑗
87cv 1352 . . . . . . . . 9 class 𝑗
9 vk . . . . . . . . . 10 setvar π‘˜
109cv 1352 . . . . . . . . 9 class π‘˜
118, 10, 5wbr 4004 . . . . . . . 8 wff 𝑗 <ℝ π‘˜
12 cF . . . . . . . . . . 11 class 𝐹
1310, 12cfv 5217 . . . . . . . . . 10 class (πΉβ€˜π‘˜)
14 vy . . . . . . . . . . . 12 setvar 𝑦
1514cv 1352 . . . . . . . . . . 11 class 𝑦
16 caddc 7814 . . . . . . . . . . 11 class +
1715, 4, 16co 5875 . . . . . . . . . 10 class (𝑦 + π‘₯)
1813, 17, 5wbr 4004 . . . . . . . . 9 wff (πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯)
1913, 4, 16co 5875 . . . . . . . . . 10 class ((πΉβ€˜π‘˜) + π‘₯)
2015, 19, 5wbr 4004 . . . . . . . . 9 wff 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)
2118, 20wa 104 . . . . . . . 8 wff ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯))
2211, 21wi 4 . . . . . . 7 wff (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))
23 cN . . . . . . 7 class 𝑁
2422, 9, 23wral 2455 . . . . . 6 wff βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))
2524, 7, 23wrex 2456 . . . . 5 wff βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))
266, 25wi 4 . . . 4 wff (0 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯))))
27 cr 7810 . . . 4 class ℝ
2826, 3, 27wral 2455 . . 3 wff βˆ€π‘₯ ∈ ℝ (0 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯))))
2928, 14, 27wrex 2456 . 2 wff βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ ℝ (0 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯))))
301, 29wi 4 1 wff (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ ℝ (0 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))))
Colors of variables: wff set class
This axiom is referenced by:  caucvgre  10990
  Copyright terms: Public domain W3C validator