Theorem caucvgsr 7915

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 7825 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 7914).

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 7910).

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 7825 to get a limit (see caucvgsrlemgt1 7908).

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

5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7913). (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 4047	. . . . . . . . . . . . 13 |- ( n = 1o -> ( n <N k <-> 1o <N k ) )
4		fveq2 5576	. . . . . . . . . . . . . . 15 |- ( n = 1o -> ( F ` n ) = ( F ` 1o ) )
5		opeq1 3819	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = 1o -> <. n , 1o >. = <. 1o , 1o >. )
6	5	eceq1d 6656	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = 1o -> [ <. n , 1o >. ] ~Q = [ <. 1o , 1o >. ] ~Q )
7	6	fveq2d 5580	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = 1o -> ( *Q ` [ <. n , 1o >. ] ~Q ) = ( *Q ` [ <. 1o , 1o >. ] ~Q ) )
8	7	breq2d 4056	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = 1o -> ( l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) <-> l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) ) )
9	8	abbidv 2323	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1o -> { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } = { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } )
10	7	breq1d 4054	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = 1o -> ( ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u <-> ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u ) )
11	10	abbidv 2323	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1o -> { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } = { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } )
12	9, 11	opeq12d 3827	. . . . . . . . . . . . . . . . . . 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 5959	. . . . . . . . . . . . . . . . . 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 3825	. . . . . . . . . . . . . . . . 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 6656	. . . . . . . . . . . . . . . 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 5960	. . . . . . . . . . . . . . 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 4057	. . . . . . . . . . . . . 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 5962	. . . . . . . . . . . . . . 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 4056	. . . . . . . . . . . . . 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 2506	. . . . . . . . . . 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 7428	. . . . . . . . . . . 12 |- 1o e. N.
24	23	a1i 9	. . . . . . . . . . 11 |- ( ph -> 1o e. N. )
25	22, 2, 24	rspcdva 2882	. . . . . . . . . 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 2569	. . . . . . . . . 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 4048	. . . . . . . . . . 11 |- ( k = m -> ( 1o <N k <-> 1o <N m ) )
31		fveq2 5576	. . . . . . . . . . . . 13 |- ( k = m -> ( F ` k ) = ( F ` m ) )
32	31	oveq1d 5959	. . . . . . . . . . . 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 4056	. . . . . . . . . . 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 2873	. . . . . . . . 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 7464	. . . . . . . . . . . . . . . . . . . 20 |- 1Q = [ <. 1o , 1o >. ] ~Q
38	37	fveq2i 5579	. . . . . . . . . . . . . . . . . . 19 |- ( *Q ` 1Q ) = ( *Q ` [ <. 1o , 1o >. ] ~Q )
39		rec1nq 7508	. . . . . . . . . . . . . . . . . . 19 |- ( *Q ` 1Q ) = 1Q
40	38, 39	eqtr3i 2228	. . . . . . . . . . . . . . . . . 18 |- ( *Q ` [ <. 1o , 1o >. ] ~Q ) = 1Q
41	40	breq2i 4052	. . . . . . . . . . . . . . . . 17 |- ( l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) <-> l <Q 1Q )
42	41	abbii 2321	. . . . . . . . . . . . . . . 16 |- { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } = { l | l <Q 1Q }
43	40	breq1i 4051	. . . . . . . . . . . . . . . . 17 |- ( ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u <-> 1Q <Q u )
44	43	abbii 2321	. . . . . . . . . . . . . . . 16 |- { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } = { u | 1Q <Q u }
45	42, 44	opeq12i 3824	. . . . . . . . . . . . . . 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 7580	. . . . . . . . . . . . . . 15 |- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
47	45, 46	eqtr4i 2229	. . . . . . . . . . . . . 14 |- <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. = 1P
48	47	oveq1i 5954	. . . . . . . . . . . . 13 |- ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) = ( 1P +P. 1P )
49	48	opeq1i 3822	. . . . . . . . . . . 12 |- <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. = <. ( 1P +P. 1P ) , 1P >.
50		eceq1 6655	. . . . . . . . . . . 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 7845	. . . . . . . . . . 11 |- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
53	51, 52	eqtr4i 2229	. . . . . . . . . 10 |- [ <. ( <. { l | l <Q ( *Q ` [ <. 1o , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. 1o , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R = 1R
54	53	oveq2i 5955	. . . . . . . . 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 4052	. . . . . . . 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 5716	. . . . . . . . 9 |- ( ( ph /\ m e. N. ) -> ( F ` 1o ) e. R. )
61		ltadd1sr 7889	. . . . . . . . 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 5576	. . . . . . . . 9 |- ( 1o = m -> ( F ` 1o ) = ( F ` m ) )
65	64	oveq1d 5959	. . . . . . . 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 4070	. . . . . 6 |- ( ( ( ph /\ m e. N. ) /\ 1o = m ) -> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) )
68		nlt1pig 7454	. . . . . . . . 9 |- ( m e. N. -> -. m <N 1o )
69	68	adantl 277	. . . . . . . 8 |- ( ( ph /\ m e. N. ) -> -. m <N 1o )
70	69	pm2.21d 620	. . . . . . 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 7435	. . . . . . . 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 1320	. . . . 5 |- ( ( ph /\ m e. N. ) -> ( F ` 1o ) <R ( ( F ` m ) +R 1R ) )
76		ltasrg 7883	. . . . . . 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 5715	. . . . . . 7 |- ( ( ph /\ m e. N. ) -> ( F ` m ) e. R. )
79		1sr 7864	. . . . . . 7 |- 1R e. R.
80		addclsr 7866	. . . . . . 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 7865	. . . . . . 7 |- -1R e. R.
83	82	a1i 9	. . . . . 6 |- ( ( ph /\ m e. N. ) -> -1R e. R. )
84		addcomsrg 7868	. . . . . . 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 6116	. . . . 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 7869	. . . . . 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 1250	. . . . 5 |- ( ( ph /\ m e. N. ) -> ( ( ( F ` m ) +R 1R ) +R -1R ) = ( ( F ` m ) +R ( 1R +R -1R ) ) )
91		addcomsrg 7868	. . . . . . . . 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 7873	. . . . . . . 8 |- ( -1R +R 1R ) = 0R
94	92, 93	eqtri 2226	. . . . . . 7 |- ( 1R +R -1R ) = 0R
95	94	oveq2i 5955	. . . . . 6 |- ( ( F ` m ) +R ( 1R +R -1R ) ) = ( ( F ` m ) +R 0R )
96		0idsr 7880	. . . . . . 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 2250	. . . . 5 |- ( ( ph /\ m e. N. ) -> ( ( F ` m ) +R ( 1R +R -1R ) ) = ( F ` m ) )
99	90, 98	eqtrd 2238	. . . 4 |- ( ( ph /\ m e. N. ) -> ( ( ( F ` m ) +R 1R ) +R -1R ) = ( F ` m ) )
100	87, 99	breqtrd 4070	. . 3 |- ( ( ph /\ m e. N. ) -> ( ( F ` 1o ) +R -1R ) <R ( F ` m ) )
101	100	ralrimiva 2579	. 2 |- ( ph -> A. m e. N. ( ( F ` 1o ) +R -1R ) <R ( F ` m ) )
102	1, 2, 101	caucvgsrlembnd 7914	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 980   /\ w3a 981   = wceq 1373   e. wcel 2176   {cab 2191   A.wral 2484   E.wrex 2485   <.cop 3636   class class class wbr 4044   -->wf 5267   ` cfv 5271  (class class class)co 5944   1oc1o 6495   [cec 6618   N.cnpi 7385   <N clti 7388   ~Q ceq 7392   1Qc1q 7394   *Qcrq 7397   <Q cltq 7398   1Pc1p 7405   +P. cpp 7406   ~R cer 7409   R.cnr 7410   0Rc0r 7411   1Rc1r 7412   -1Rcm1r 7413   +R cplr 7414   <R cltr 7416

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 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-coll 4159  ax-sep 4162  ax-nul 4170  ax-pow 4218  ax-pr 4253  ax-un 4480  ax-setind 4585  ax-iinf 4636

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-ral 2489  df-rex 2490  df-reu 2491  df-rmo 2492  df-rab 2493  df-v 2774  df-sbc 2999  df-csb 3094  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3461  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-int 3886  df-iun 3929  df-br 4045  df-opab 4106  df-mpt 4107  df-tr 4143  df-eprel 4336  df-id 4340  df-po 4343  df-iso 4344  df-iord 4413  df-on 4415  df-suc 4418  df-iom 4639  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-res 4687  df-ima 4688  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-riota 5899  df-ov 5947  df-oprab 5948  df-mpo 5949  df-1st 6226  df-2nd 6227  df-recs 6391  df-irdg 6456  df-1o 6502  df-2o 6503  df-oadd 6506  df-omul 6507  df-er 6620  df-ec 6622  df-qs 6626  df-ni 7417  df-pli 7418  df-mi 7419  df-lti 7420  df-plpq 7457  df-mpq 7458  df-enq 7460  df-nqqs 7461  df-plqqs 7462  df-mqqs 7463  df-1nqqs 7464  df-rq 7465  df-ltnqqs 7466  df-enq0 7537  df-nq0 7538  df-0nq0 7539  df-plq0 7540  df-mq0 7541  df-inp 7579  df-i1p 7580  df-iplp 7581  df-imp 7582  df-iltp 7583  df-enr 7839  df-nr 7840  df-plr 7841  df-mr 7842  df-ltr 7843  df-0r 7844  df-1r 7845  df-m1r 7846

This theorem is referenced by:  axcaucvglemres  8012