Theorem caucvgsr 8117

Description: A Cauchy sequence of signed reals with a modulus of convergence converges to a signed real. This is basically Corollary 11.2.13 of [HoTT], p. (varies). The HoTT book theorem has a modulus of convergence (that is, a rate of convergence) specified by (11.2.9) in HoTT whereas this theorem fixes the rate of convergence to say that all terms after the nth term must be within 1 / n of the nth term (it should later be able to prove versions of this theorem with a different fixed rate or a modulus of convergence supplied as a hypothesis).

This is similar to caucvgprpr 8027 but is for signed reals rather than positive reals.

Here is an outline of how we prove it:

1. Choose a lower bound for the sequence (see caucvgsrlembnd 8116).

2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 8112).

3. Since a signed real (element of R.) which is greater than zero can be mapped to a positive real (element of P.), perform that mapping on each element of the sequence and invoke caucvgprpr 8027 to get a limit (see caucvgsrlemgt1 8110).

4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 8110).

5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 8115). (Contributed by Jim Kingdon, 20-Jun-2021.)

Hypotheses

Ref	Expression
caucvgsr.f	|- ( ph -> F : N. --> R. )
caucvgsr.cau	|- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )

Assertion

Ref	Expression
caucvgsr	|- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <R ( y +R x ) /\ y <R ( ( F ` k ) +R x ) ) ) ) )

Distinct variable groups:   j, F, k, l, u   n, F, k, l, u   x, F, y, j, k   ph, j, k, x   ph, n

Allowed substitution hints:   ph( y, u, l)

Proof of Theorem caucvgsr

Dummy variables f g h m are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		caucvgsr.f	. 2 |- ( ph -> F : N. --> R. )
2		caucvgsr.cau	. 2 |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )
3		breq1 4112	. . . . . . . . . . . . 13 |- ( n = 1o -> ( n <N k <-> 1o <N k ) )
4		fveq2 5670	. . . . . . . . . . . . . . 15 |- ( n = 1o -> ( F ` n ) = ( F ` 1o ) )
5		opeq1 3883	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = 1o -> <. n , 1o >. = <. 1o , 1o >. )
6	5	eceq1d 6803	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = 1o -> [ <. n , 1o >. ] ~Q = [ <. 1o , 1o >. ] ~Q )
7	6	fveq2d 5674	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = 1o -> ( *Q ` [ <. n , 1o >. ] ~Q ) = ( *Q ` [ <. 1o , 1o >. ] ~Q ) )
8	7	breq2d 4121	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = 1o -> ( l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) <-> l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) ) )
9	8	abbidv 2352	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1o -> { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } = { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } )
10	7	breq1d 4119	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = 1o -> ( ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u <-> ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u ) )
11	10	abbidv 2352	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1o -> { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } = { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } )
12	9, 11	opeq12d 3891	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1o -> <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. = <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. )
13	12	oveq1d 6065	. . . . . . . . . . . . . . . . . 18 |- ( n = 1o -> ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) = ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) )
14	13	opeq1d 3889	. . . . . . . . . . . . . . . . 17 |- ( n = 1o -> <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. = <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. )
15	14	eceq1d 6803	. . . . . . . . . . . . . . . 16 |- ( n = 1o -> [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R = [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R )
16	15	oveq2d 6066	. . . . . . . . . . . . . . 15 |- ( n = 1o -> ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) = ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) )
17	4, 16	breq12d 4122	. . . . . . . . . . . . . 14 |- ( n = 1o -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) <-> ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) )
18	4, 15	oveq12d 6068	. . . . . . . . . . . . . . 15 |- ( n = 1o -> ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) = ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) )
19	18	breq2d 4121	. . . . . . . . . . . . . 14 |- ( n = 1o -> ( ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) <-> ( F ` k ) <R ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) )
20	17, 19	anbi12d 473	. . . . . . . . . . . . 13 |- ( n = 1o -> ( ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) <-> ( ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )
21	3, 20	imbi12d 234	. . . . . . . . . . . 12 |- ( n = 1o -> ( ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) <-> ( 1o <N k -> ( ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) ) )
22	21	ralbidv 2542	. . . . . . . . . . 11 |- ( n = 1o -> ( A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) <-> A. k e. N. ( 1o <N k -> ( ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) ) )
23		1pi 7630	. . . . . . . . . . . 12 |- 1o e. N.
24	23	a1i 9	. . . . . . . . . . 11 |- ( ph -> 1o e. N. )
25	22, 2, 24	rspcdva 2926	. . . . . . . . . 10 |- ( ph -> A. k e. N. ( 1o <N k -> ( ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )
26		simpl 109	. . . . . . . . . . . 12 |- ( ( ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) -> ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) )
27	26	imim2i 12	. . . . . . . . . . 11 |- ( ( 1o <N k -> ( ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) -> ( 1o <N k -> ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) )
28	27	ralimi 2605	. . . . . . . . . 10 |- ( A. k e. N. ( 1o <N k -> ( ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` 1o ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) -> A. k e. N. ( 1o <N k -> ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) )
29	25, 28	syl 14	. . . . . . . . 9 |- ( ph -> A. k e. N. ( 1o <N k -> ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) )
30		breq2 4113	. . . . . . . . . . 11 |- ( k = m -> ( 1o <N k <-> 1o <N m ) )
31		fveq2 5670	. . . . . . . . . . . . 13 |- ( k = m -> ( F ` k ) = ( F ` m ) )
32	31	oveq1d 6065	. . . . . . . . . . . 12 |- ( k = m -> ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) = ( ( F ` m ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) )
33	32	breq2d 4121	. . . . . . . . . . 11 |- ( k = m -> ( ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) <-> ( F ` 1o ) <R ( ( F ` m ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) )
34	30, 33	imbi12d 234	. . . . . . . . . 10 |- ( k = m -> ( ( 1o <N k -> ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) <-> ( 1o <N m -> ( F ` 1o ) <R ( ( F ` m ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )
35	34	rspcv 2917	. . . . . . . . 9 |- ( m e. N. -> ( A. k e. N. ( 1o <N k -> ( F ` 1o ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) -> ( 1o <N m -> ( F ` 1o ) <R ( ( F ` m ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )
36	29, 35	mpan9 281	. . . . . . . 8 |- ( ( ph /\ m e. N. ) -> ( 1o <N m -> ( F ` 1o ) <R ( ( F ` m ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) )
37		df-1nqqs 7666	. . . . . . . . . . . . . . . . . . . 20 |- 1Q = [ <. 1o , 1o >. ] ~Q
38	37	fveq2i 5673	. . . . . . . . . . . . . . . . . . 19 |- ( *Q ` 1Q ) = ( *Q ` [ <. 1o , 1o >. ] ~Q )
39		rec1nq 7710	. . . . . . . . . . . . . . . . . . 19 |- ( *Q ` 1Q ) = 1Q
40	38, 39	eqtr3i 2255	. . . . . . . . . . . . . . . . . 18 |- ( *Q ` [ <. 1o , 1o >. ] ~Q ) = 1Q
41	40	breq2i 4117	. . . . . . . . . . . . . . . . 17 |- ( l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) <-> l <Q 1Q )
42	41	abbii 2348	. . . . . . . . . . . . . . . 16 |- { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } = { l | l <Q 1Q }
43	40	breq1i 4116	. . . . . . . . . . . . . . . . 17 |- ( ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u <-> 1Q <Q u )
44	43	abbii 2348	. . . . . . . . . . . . . . . 16 |- { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } = { u | 1Q <Q u }
45	42, 44	opeq12i 3888	. . . . . . . . . . . . . . 15 |- <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
46		df-i1p 7782	. . . . . . . . . . . . . . 15 |- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
47	45, 46	eqtr4i 2256	. . . . . . . . . . . . . 14 |- <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. = 1P
48	47	oveq1i 6060	. . . . . . . . . . . . 13 |- ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) = ( 1P +P. 1P )
49	48	opeq1i 3886	. . . . . . . . . . . 12 |- <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. = <. ( 1P +P. 1P ) , 1P >.
50		eceq1 6802	. . . . . . . . . . . 12 |- ( <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. = <. ( 1P +P. 1P ) , 1P >. -> [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R )
51	49, 50	ax-mp 5	. . . . . . . . . . 11 |- [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
52		df-1r 8047	. . . . . . . . . . 11 |- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
53	51, 52	eqtr4i 2256	. . . . . . . . . 10 |- [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R = 1R
54	53	oveq2i 6061	. . . . . . . . 9 |- ( ( F ` m ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) = ( ( F ` m ) +R 1R )
55	54	breq2i 4117	. . . . . . . 8 |- ( ( F ` 1o ) <R ( ( F ` m ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) <-> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) )
56	36, 55	imbitrdi 161	. . . . . . 7 |- ( ( ph /\ m e. N. ) -> ( 1o <N m -> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) ) )
57	56	imp 124	. . . . . 6 |- ( ( ( ph /\ m e. N. ) /\ 1o <N m ) -> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) )
58	1	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ m e. N. ) -> F : N. --> R. )
59	23	a1i 9	. . . . . . . . . 10 |- ( ( ph /\ m e. N. ) -> 1o e. N. )
60	58, 59	ffvelcdmd 5813	. . . . . . . . 9 |- ( ( ph /\ m e. N. ) -> ( F ` 1o ) e. R. )
61		ltadd1sr 8091	. . . . . . . . 9 |- ( ( F ` 1o ) e. R. -> ( F ` 1o ) <R ( ( F ` 1o ) +R 1R ) )
62	60, 61	syl 14	. . . . . . . 8 |- ( ( ph /\ m e. N. ) -> ( F ` 1o ) <R ( ( F ` 1o ) +R 1R ) )
63	62	adantr 276	. . . . . . 7 |- ( ( ( ph /\ m e. N. ) /\ 1o = m ) -> ( F ` 1o ) <R ( ( F ` 1o ) +R 1R ) )
64		fveq2 5670	. . . . . . . . 9 |- ( 1o = m -> ( F ` 1o ) = ( F ` m ) )
65	64	oveq1d 6065	. . . . . . . 8 |- ( 1o = m -> ( ( F ` 1o ) +R 1R ) = ( ( F ` m ) +R 1R ) )
66	65	adantl 277	. . . . . . 7 |- ( ( ( ph /\ m e. N. ) /\ 1o = m ) -> ( ( F ` 1o ) +R 1R ) = ( ( F ` m ) +R 1R ) )
67	63, 66	breqtrd 4135	. . . . . 6 |- ( ( ( ph /\ m e. N. ) /\ 1o = m ) -> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) )
68		nlt1pig 7656	. . . . . . . . 9 |- ( m e. N. -> -. m <N 1o )
69	68	adantl 277	. . . . . . . 8 |- ( ( ph /\ m e. N. ) -> -. m <N 1o )
70	69	pm2.21d 624	. . . . . . 7 |- ( ( ph /\ m e. N. ) -> ( m <N 1o -> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) ) )
71	70	imp 124	. . . . . 6 |- ( ( ( ph /\ m e. N. ) /\ m <N 1o ) -> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) )
72		pitri3or 7637	. . . . . . . 8 |- ( ( 1o e. N. /\ m e. N. ) -> ( 1o <N m \/ 1o = m \/ m <N 1o ) )
73	23, 72	mpan 424	. . . . . . 7 |- ( m e. N. -> ( 1o <N m \/ 1o = m \/ m <N 1o ) )
74	73	adantl 277	. . . . . 6 |- ( ( ph /\ m e. N. ) -> ( 1o <N m \/ 1o = m \/ m <N 1o ) )
75	57, 67, 71, 74	mpjao3dan 1344	. . . . 5 |- ( ( ph /\ m e. N. ) -> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) )
76		ltasrg 8085	. . . . . . 7 |- ( ( f e. R. /\ g e. R. /\ h e. R. ) -> ( f <R g <-> ( h +R f ) <R ( h +R g ) ) )
77	76	adantl 277	. . . . . 6 |- ( ( ( ph /\ m e. N. ) /\ ( f e. R. /\ g e. R. /\ h e. R. ) ) -> ( f <R g <-> ( h +R f ) <R ( h +R g ) ) )
78	1	ffvelcdmda 5812	. . . . . . 7 |- ( ( ph /\ m e. N. ) -> ( F ` m ) e. R. )
79		1sr 8066	. . . . . . 7 |- 1R e. R.
80		addclsr 8068	. . . . . . 7 |- ( ( ( F ` m ) e. R. /\ 1R e. R. ) -> ( ( F ` m ) +R 1R ) e. R. )
81	78, 79, 80	sylancl 413	. . . . . 6 |- ( ( ph /\ m e. N. ) -> ( ( F ` m ) +R 1R ) e. R. )
82		m1r 8067	. . . . . . 7 |- -1R e. R.
83	82	a1i 9	. . . . . 6 |- ( ( ph /\ m e. N. ) -> -1R e. R. )
84		addcomsrg 8070	. . . . . . 7 |- ( ( f e. R. /\ g e. R. ) -> ( f +R g ) = ( g +R f ) )
85	84	adantl 277	. . . . . 6 |- ( ( ( ph /\ m e. N. ) /\ ( f e. R. /\ g e. R. ) ) -> ( f +R g ) = ( g +R f ) )
86	77, 60, 81, 83, 85	caovord2d 6224	. . . . 5 |- ( ( ph /\ m e. N. ) -> ( ( F ` 1o ) <R ( ( F ` m ) +R 1R ) <-> ( ( F ` 1o ) +R -1R ) <R ( ( ( F ` m ) +R 1R ) +R -1R ) ) )
87	75, 86	mpbid 147	. . . 4 |- ( ( ph /\ m e. N. ) -> ( ( F ` 1o ) +R -1R ) <R ( ( ( F ` m ) +R 1R ) +R -1R ) )
88	79	a1i 9	. . . . . 6 |- ( ( ph /\ m e. N. ) -> 1R e. R. )
89		addasssrg 8071	. . . . . 6 |- ( ( ( F ` m ) e. R. /\ 1R e. R. /\ -1R e. R. ) -> ( ( ( F ` m ) +R 1R ) +R -1R ) = ( ( F ` m ) +R ( 1R +R -1R ) ) )
90	78, 88, 83, 89	syl3anc 1274	. . . . 5 |- ( ( ph /\ m e. N. ) -> ( ( ( F ` m ) +R 1R ) +R -1R ) = ( ( F ` m ) +R ( 1R +R -1R ) ) )
91		addcomsrg 8070	. . . . . . . . 9 |- ( ( 1R e. R. /\ -1R e. R. ) -> ( 1R +R -1R ) = ( -1R +R 1R ) )
92	79, 82, 91	mp2an 426	. . . . . . . 8 |- ( 1R +R -1R ) = ( -1R +R 1R )
93		m1p1sr 8075	. . . . . . . 8 |- ( -1R +R 1R ) = 0R
94	92, 93	eqtri 2253	. . . . . . 7 |- ( 1R +R -1R ) = 0R
95	94	oveq2i 6061	. . . . . 6 |- ( ( F ` m ) +R ( 1R +R -1R ) ) = ( ( F ` m ) +R 0R )
96		0idsr 8082	. . . . . . 7 |- ( ( F ` m ) e. R. -> ( ( F ` m ) +R 0R ) = ( F ` m ) )
97	78, 96	syl 14	. . . . . 6 |- ( ( ph /\ m e. N. ) -> ( ( F ` m ) +R 0R ) = ( F ` m ) )
98	95, 97	eqtrid 2277	. . . . 5 |- ( ( ph /\ m e. N. ) -> ( ( F ` m ) +R ( 1R +R -1R ) ) = ( F ` m ) )
99	90, 98	eqtrd 2265	. . . 4 |- ( ( ph /\ m e. N. ) -> ( ( ( F ` m ) +R 1R ) +R -1R ) = ( F ` m ) )
100	87, 99	breqtrd 4135	. . 3 |- ( ( ph /\ m e. N. ) -> ( ( F ` 1o ) +R -1R ) <R ( F ` m ) )
101	100	ralrimiva 2615	. 2 |- ( ph -> A. m e. N. ( ( F ` 1o ) +R -1R ) <R ( F ` m ) )
102	1, 2, 101	caucvgsrlembnd 8116	1 |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <R ( y +R x ) /\ y <R ( ( F ` k ) +R x ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ w3o 1004   /\ w3a 1005   = wceq 1398   e. wcel 2203   {cab 2218   A.wral 2520   E.wrex 2521   <.cop 3692   class class class wbr 4109   -->wf 5348   ` cfv 5352  (class class class)co 6050   1oc1o 6640   [cec 6765   N.cnpi 7587   <N clti 7590   ~Q ceq 7594   1Qc1q 7596   *Qcrq 7599   <Q cltq 7600   1Pc1p 7607   +P. cpp 7608   ~R cer 7611   R.cnr 7612   0Rc0r 7613   1Rc1r 7614   -1Rcm1r 7615   +R cplr 7616   <R cltr 7618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4225  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-iinf 4710

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-ral 2525  df-rex 2526  df-reu 2527  df-rmo 2528  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-iun 3993  df-br 4110  df-opab 4172  df-mpt 4173  df-tr 4209  df-eprel 4410  df-id 4414  df-po 4417  df-iso 4418  df-iord 4487  df-on 4489  df-suc 4492  df-iom 4713  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-1st 6334  df-2nd 6335  df-recs 6536  df-irdg 6601  df-1o 6647  df-2o 6648  df-oadd 6651  df-omul 6652  df-er 6767  df-ec 6769  df-qs 6773  df-ni 7619  df-pli 7620  df-mi 7621  df-lti 7622  df-plpq 7659  df-mpq 7660  df-enq 7662  df-nqqs 7663  df-plqqs 7664  df-mqqs 7665  df-1nqqs 7666  df-rq 7667  df-ltnqqs 7668  df-enq0 7739  df-nq0 7740  df-0nq0 7741  df-plq0 7742  df-mq0 7743  df-inp 7781  df-i1p 7782  df-iplp 7783  df-imp 7784  df-iltp 7785  df-enr 8041  df-nr 8042  df-plr 8043  df-mr 8044  df-ltr 8045  df-0r 8046  df-1r 8047  df-m1r 8048

This theorem is referenced by:  axcaucvglemres  8214