Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-caucvg Unicode 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 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 notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.)
Hypotheses
Ref Expression
ax-caucvg.n
ax-caucvg.f
ax-caucvg.cau
Assertion
Ref Expression
ax-caucvg
Distinct variable groups:   ,,,   ,,,,   ,,,   ,,   ,,,   ,,   ,   ,
Allowed substitution hints:   (,)   ()   ()

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