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

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

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  /  n of the nth term.

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

Hypotheses
Ref Expression
ax-caucvg.n  |-  N  = 
|^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
ax-caucvg.f  |-  ( ph  ->  F : N --> RR )
ax-caucvg.cau  |-  ( ph  ->  A. n  e.  N  A. k  e.  N  ( n  <RR  k  -> 
( ( F `  n )  <RR  ( ( F `  k )  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  /\  ( F `  k )  <RR  ( ( F `  n )  +  (
iota_ r  e.  RR  ( n  x.  r
)  =  1 ) ) ) ) )
Assertion
Ref Expression
ax-caucvg  |-  ( ph  ->  E. y  e.  RR  A. x  e.  RR  (
0  <RR  x  ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  ->  ( ( F `  k )  <RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) ) ) ) )
Distinct variable groups:    j, F, k, n    x, F, y, j, k    j, N, k, n    x, N, y    ph, j, k, n   
k, r, n    ph, x
Allowed substitution hints:    ph( y, r)    F( r)    N( r)

Detailed syntax breakdown of Axiom ax-caucvg
StepHypRef Expression
1 wph . 2  wff  ph
2 cc0 7294 . . . . . 6  class  0
3 vx . . . . . . 7  setvar  x
43cv 1286 . . . . . 6  class  x
5 cltrr 7298 . . . . . 6  class  <RR
62, 4, 5wbr 3820 . . . . 5  wff  0  <RR  x
7 vj . . . . . . . . . 10  setvar  j
87cv 1286 . . . . . . . . 9  class  j
9 vk . . . . . . . . . 10  setvar  k
109cv 1286 . . . . . . . . 9  class  k
118, 10, 5wbr 3820 . . . . . . . 8  wff  j  <RR  k
12 cF . . . . . . . . . . 11  class  F
1310, 12cfv 4981 . . . . . . . . . 10  class  ( F `
 k )
14 vy . . . . . . . . . . . 12  setvar  y
1514cv 1286 . . . . . . . . . . 11  class  y
16 caddc 7297 . . . . . . . . . . 11  class  +
1715, 4, 16co 5613 . . . . . . . . . 10  class  ( y  +  x )
1813, 17, 5wbr 3820 . . . . . . . . 9  wff  ( F `
 k )  <RR  ( y  +  x )
1913, 4, 16co 5613 . . . . . . . . . 10  class  ( ( F `  k )  +  x )
2015, 19, 5wbr 3820 . . . . . . . . 9  wff  y  <RR  ( ( F `  k
)  +  x )
2118, 20wa 102 . . . . . . . 8  wff  ( ( F `  k ) 
<RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) )
2211, 21wi 4 . . . . . . 7  wff  ( j 
<RR  k  ->  ( ( F `  k ) 
<RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) ) )
23 cN . . . . . . 7  class  N
2422, 9, 23wral 2355 . . . . . 6  wff  A. k  e.  N  ( j  <RR  k  ->  ( ( F `  k )  <RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) ) )
2524, 7, 23wrex 2356 . . . . 5  wff  E. j  e.  N  A. k  e.  N  ( j  <RR  k  ->  ( ( F `  k )  <RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) ) )
266, 25wi 4 . . . 4  wff  ( 0 
<RR  x  ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  ->  ( ( F `  k )  <RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) ) ) )
27 cr 7293 . . . 4  class  RR
2826, 3, 27wral 2355 . . 3  wff  A. x  e.  RR  ( 0  <RR  x  ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  -> 
( ( F `  k )  <RR  ( y  +  x )  /\  y  <RR  ( ( F `
 k )  +  x ) ) ) )
2928, 14, 27wrex 2356 . 2  wff  E. y  e.  RR  A. x  e.  RR  ( 0  <RR  x  ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  -> 
( ( F `  k )  <RR  ( y  +  x )  /\  y  <RR  ( ( F `
 k )  +  x ) ) ) )
301, 29wi 4 1  wff  ( ph  ->  E. y  e.  RR  A. x  e.  RR  (
0  <RR  x  ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  ->  ( ( F `  k )  <RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) ) ) ) )
Colors of variables: wff set class
This axiom is referenced by:  caucvgre  10309
  Copyright terms: Public domain W3C validator