Axiom ax-caucvg 7926

Description: Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 7894.

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 10981 (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

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		cc0 7806	. . . . . 6 class 0
3		vx	. . . . . . 7 setvar x
4	3	cv 1352	. . . . . 6 class x
5		cltrr 7810	. . . . . 6 class <RR
6	2, 4, 5	wbr 4001	. . . . 5 wff 0 <RR x
7		vj	. . . . . . . . . 10 setvar j
8	7	cv 1352	. . . . . . . . 9 class j
9		vk	. . . . . . . . . 10 setvar k
10	9	cv 1352	. . . . . . . . 9 class k
11	8, 10, 5	wbr 4001	. . . . . . . 8 wff j <RR k
12		cF	. . . . . . . . . . 11 class F
13	10, 12	cfv 5213	. . . . . . . . . 10 class ( F ` k )
14		vy	. . . . . . . . . . . 12 setvar y
15	14	cv 1352	. . . . . . . . . . 11 class y
16		caddc 7809	. . . . . . . . . . 11 class +
17	15, 4, 16	co 5870	. . . . . . . . . 10 class ( y + x )
18	13, 17, 5	wbr 4001	. . . . . . . . 9 wff ( F ` k ) <RR ( y + x )
19	13, 4, 16	co 5870	. . . . . . . . . 10 class ( ( F ` k ) + x )
20	15, 19, 5	wbr 4001	. . . . . . . . 9 wff y <RR ( ( F ` k ) + x )
21	18, 20	wa 104	. . . . . . . 8 wff ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) )
22	11, 21	wi 4	. . . . . . 7 wff ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) )
23		cN	. . . . . . 7 class N
24	22, 9, 23	wral 2455	. . . . . 6 wff A. k e. N ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) )
25	24, 7, 23	wrex 2456	. . . . 5 wff E. j e. N A. k e. N ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) )
26	6, 25	wi 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 7805	. . . 4 class RR
28	26, 3, 27	wral 2455	. . 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 ) ) ) )
29	28, 14, 27	wrex 2456	. 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 ) ) ) )
30	1, 29	wi 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 ) ) ) ) )

This axiom is referenced by:  caucvgre  10981