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

Theorem caucvgsr 7574
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 7484 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 7573).

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

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

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

5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7572). (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.
StepHypRef 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 3900 . . . . . . . . . . . . 13  |-  ( n  =  1o  ->  (
n  <N  k  <->  1o  <N  k ) )
4 fveq2 5387 . . . . . . . . . . . . . . 15  |-  ( n  =  1o  ->  ( F `  n )  =  ( F `  1o ) )
5 opeq1 3673 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  1o  ->  <. n ,  1o >.  =  <. 1o ,  1o >. )
65eceq1d 6431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  1o  ->  [ <. n ,  1o >. ]  ~Q  =  [ <. 1o ,  1o >. ]  ~Q  )
76fveq2d 5391 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  1o  ->  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  =  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) )
87breq2d 3909 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  1o  ->  (
l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <->  l  <Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) ) )
98abbidv 2233 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1o  ->  { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) }  =  { l  |  l  <Q  ( *Q
`  [ <. 1o ,  1o >. ]  ~Q  ) } )
107breq1d 3907 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  1o  ->  (
( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u  <->  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u ) )
1110abbidv 2233 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1o  ->  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u }  =  {
u  |  ( *Q
`  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } )
129, 11opeq12d 3681 . . . . . . . . . . . . . . . . . . 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 } >. )
1312oveq1d 5755 . . . . . . . . . . . . . . . . . 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 ) )
1413opeq1d 3679 . . . . . . . . . . . . . . . . 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 >. )
1514eceq1d 6431 . . . . . . . . . . . . . . . 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  )
1615oveq2d 5756 . . . . . . . . . . . . . . 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  ) )
174, 16breq12d 3910 . . . . . . . . . . . . . 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  ) ) )
184, 15oveq12d 5758 . . . . . . . . . . . . . . 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  ) )
1918breq2d 3909 . . . . . . . . . . . . . 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  ) ) )
2017, 19anbi12d 462 . . . . . . . . . . . . 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  ) ) ) )
213, 20imbi12d 233 . . . . . . . . . . . 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  ) ) ) ) )
2221ralbidv 2412 . . . . . . . . . . 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 7087 . . . . . . . . . . . 12  |-  1o  e.  N.
2423a1i 9 . . . . . . . . . . 11  |-  ( ph  ->  1o  e.  N. )
2522, 2, 24rspcdva 2766 . . . . . . . . . 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 108 . . . . . . . . . . . 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  )
)
2726imim2i 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  ) ) )
2827ralimi 2470 . . . . . . . . . 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  ) ) )
2925, 28syl 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 3901 . . . . . . . . . . 11  |-  ( k  =  m  ->  ( 1o  <N  k  <->  1o  <N  m ) )
31 fveq2 5387 . . . . . . . . . . . . 13  |-  ( k  =  m  ->  ( F `  k )  =  ( F `  m ) )
3231oveq1d 5755 . . . . . . . . . . . 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  ) )
3332breq2d 3909 . . . . . . . . . . 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  ) ) )
3430, 33imbi12d 233 . . . . . . . . . 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  ) ) ) )
3534rspcv 2757 . . . . . . . . 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  )
) ) )
3629, 35mpan9 277 . . . . . . . 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 7123 . . . . . . . . . . . . . . . . . . . 20  |-  1Q  =  [ <. 1o ,  1o >. ]  ~Q
3837fveq2i 5390 . . . . . . . . . . . . . . . . . . 19  |-  ( *Q
`  1Q )  =  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )
39 rec1nq 7167 . . . . . . . . . . . . . . . . . . 19  |-  ( *Q
`  1Q )  =  1Q
4038, 39eqtr3i 2138 . . . . . . . . . . . . . . . . . 18  |-  ( *Q
`  [ <. 1o ,  1o >. ]  ~Q  )  =  1Q
4140breq2i 3905 . . . . . . . . . . . . . . . . 17  |-  ( l 
<Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <->  l  <Q  1Q )
4241abbii 2231 . . . . . . . . . . . . . . . 16  |-  { l  |  l  <Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) }  =  { l  |  l  <Q  1Q }
4340breq1i 3904 . . . . . . . . . . . . . . . . 17  |-  ( ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u  <->  1Q  <Q  u )
4443abbii 2231 . . . . . . . . . . . . . . . 16  |-  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u }  =  {
u  |  1Q  <Q  u }
4542, 44opeq12i 3678 . . . . . . . . . . . . . . 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 7239 . . . . . . . . . . . . . . 15  |-  1P  =  <. { l  |  l 
<Q  1Q } ,  {
u  |  1Q  <Q  u } >.
4745, 46eqtr4i 2139 . . . . . . . . . . . . . 14  |-  <. { l  |  l  <Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } >.  =  1P
4847oveq1i 5750 . . . . . . . . . . . . 13  |-  ( <. { l  |  l 
<Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P )  =  ( 1P  +P.  1P )
4948opeq1i 3676 . . . . . . . . . . . 12  |-  <. ( <. { l  |  l 
<Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >.  =  <. ( 1P  +P.  1P ) ,  1P >.
50 eceq1 6430 . . . . . . . . . . . 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  )
5149, 50ax-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 7504 . . . . . . . . . . 11  |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
5351, 52eqtr4i 2139 . . . . . . . . . 10  |-  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  =  1R
5453oveq2i 5751 . . . . . . . . 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 )
5554breq2i 3905 . . . . . . . 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 ) )
5636, 55syl6ib 160 . . . . . . 7  |-  ( (
ph  /\  m  e.  N. )  ->  ( 1o 
<N  m  ->  ( F `
 1o )  <R 
( ( F `  m )  +R  1R ) ) )
5756imp 123 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  1o  <N  m )  ->  ( F `  1o )  <R  ( ( F `  m )  +R  1R ) )
581adantr 272 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  N. )  ->  F : N.
--> R. )
5923a1i 9 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  N. )  ->  1o  e.  N. )
6058, 59ffvelrnd 5522 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  N. )  ->  ( F `
 1o )  e. 
R. )
61 ltadd1sr 7548 . . . . . . . . 9  |-  ( ( F `  1o )  e.  R.  ->  ( F `  1o )  <R  ( ( F `  1o )  +R  1R )
)
6260, 61syl 14 . . . . . . . 8  |-  ( (
ph  /\  m  e.  N. )  ->  ( F `
 1o )  <R 
( ( F `  1o )  +R  1R )
)
6362adantr 272 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  N. )  /\  1o  =  m )  ->  ( F `  1o )  <R  ( ( F `  1o )  +R  1R )
)
64 fveq2 5387 . . . . . . . . 9  |-  ( 1o  =  m  ->  ( F `  1o )  =  ( F `  m ) )
6564oveq1d 5755 . . . . . . . 8  |-  ( 1o  =  m  ->  (
( F `  1o )  +R  1R )  =  ( ( F `  m )  +R  1R ) )
6665adantl 273 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  N. )  /\  1o  =  m )  ->  (
( F `  1o )  +R  1R )  =  ( ( F `  m )  +R  1R ) )
6763, 66breqtrd 3922 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  1o  =  m )  ->  ( F `  1o )  <R  ( ( F `  m )  +R  1R ) )
68 nlt1pig 7113 . . . . . . . . 9  |-  ( m  e.  N.  ->  -.  m  <N  1o )
6968adantl 273 . . . . . . . 8  |-  ( (
ph  /\  m  e.  N. )  ->  -.  m  <N  1o )
7069pm2.21d 591 . . . . . . 7  |-  ( (
ph  /\  m  e.  N. )  ->  ( m 
<N  1o  ->  ( F `  1o )  <R  (
( F `  m
)  +R  1R )
) )
7170imp 123 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  m  <N  1o )  ->  ( F `  1o )  <R  ( ( F `  m )  +R  1R ) )
72 pitri3or 7094 . . . . . . . 8  |-  ( ( 1o  e.  N.  /\  m  e.  N. )  ->  ( 1o  <N  m  \/  1o  =  m  \/  m  <N  1o )
)
7323, 72mpan 418 . . . . . . 7  |-  ( m  e.  N.  ->  ( 1o  <N  m  \/  1o  =  m  \/  m  <N  1o ) )
7473adantl 273 . . . . . 6  |-  ( (
ph  /\  m  e.  N. )  ->  ( 1o 
<N  m  \/  1o  =  m  \/  m  <N  1o ) )
7557, 67, 71, 74mpjao3dan 1268 . . . . 5  |-  ( (
ph  /\  m  e.  N. )  ->  ( F `
 1o )  <R 
( ( F `  m )  +R  1R ) )
76 ltasrg 7542 . . . . . . 7  |-  ( ( f  e.  R.  /\  g  e.  R.  /\  h  e.  R. )  ->  (
f  <R  g  <->  ( h  +R  f )  <R  (
h  +R  g ) ) )
7776adantl 273 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  (
f  e.  R.  /\  g  e.  R.  /\  h  e.  R. ) )  -> 
( f  <R  g  <->  ( h  +R  f ) 
<R  ( h  +R  g
) ) )
781ffvelrnda 5521 . . . . . . 7  |-  ( (
ph  /\  m  e.  N. )  ->  ( F `
 m )  e. 
R. )
79 1sr 7523 . . . . . . 7  |-  1R  e.  R.
80 addclsr 7525 . . . . . . 7  |-  ( ( ( F `  m
)  e.  R.  /\  1R  e.  R. )  -> 
( ( F `  m )  +R  1R )  e.  R. )
8178, 79, 80sylancl 407 . . . . . 6  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  m )  +R  1R )  e. 
R. )
82 m1r 7524 . . . . . . 7  |-  -1R  e.  R.
8382a1i 9 . . . . . 6  |-  ( (
ph  /\  m  e.  N. )  ->  -1R  e.  R. )
84 addcomsrg 7527 . . . . . . 7  |-  ( ( f  e.  R.  /\  g  e.  R. )  ->  ( f  +R  g
)  =  ( g  +R  f ) )
8584adantl 273 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  (
f  e.  R.  /\  g  e.  R. )
)  ->  ( f  +R  g )  =  ( g  +R  f ) )
8677, 60, 81, 83, 85caovord2d 5906 . . . . 5  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  1o ) 
<R  ( ( F `  m )  +R  1R ) 
<->  ( ( F `  1o )  +R  -1R )  <R  ( ( ( F `
 m )  +R 
1R )  +R  -1R ) ) )
8775, 86mpbid 146 . . . 4  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  1o )  +R  -1R )  <R 
( ( ( F `
 m )  +R 
1R )  +R  -1R ) )
8879a1i 9 . . . . . 6  |-  ( (
ph  /\  m  e.  N. )  ->  1R  e.  R. )
89 addasssrg 7528 . . . . . 6  |-  ( ( ( F `  m
)  e.  R.  /\  1R  e.  R.  /\  -1R  e.  R. )  ->  (
( ( F `  m )  +R  1R )  +R  -1R )  =  ( ( F `  m )  +R  ( 1R  +R  -1R ) ) )
9078, 88, 83, 89syl3anc 1199 . . . . 5  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( ( F `  m
)  +R  1R )  +R  -1R )  =  ( ( F `  m
)  +R  ( 1R 
+R  -1R ) ) )
91 addcomsrg 7527 . . . . . . . . 9  |-  ( ( 1R  e.  R.  /\  -1R  e.  R. )  -> 
( 1R  +R  -1R )  =  ( -1R  +R 
1R ) )
9279, 82, 91mp2an 420 . . . . . . . 8  |-  ( 1R 
+R  -1R )  =  ( -1R  +R  1R )
93 m1p1sr 7532 . . . . . . . 8  |-  ( -1R 
+R  1R )  =  0R
9492, 93eqtri 2136 . . . . . . 7  |-  ( 1R 
+R  -1R )  =  0R
9594oveq2i 5751 . . . . . 6  |-  ( ( F `  m )  +R  ( 1R  +R  -1R ) )  =  ( ( F `  m
)  +R  0R )
96 0idsr 7539 . . . . . . 7  |-  ( ( F `  m )  e.  R.  ->  (
( F `  m
)  +R  0R )  =  ( F `  m ) )
9778, 96syl 14 . . . . . 6  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  m )  +R  0R )  =  ( F `  m
) )
9895, 97syl5eq 2160 . . . . 5  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  m )  +R  ( 1R  +R  -1R ) )  =  ( F `  m ) )
9990, 98eqtrd 2148 . . . 4  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( ( F `  m
)  +R  1R )  +R  -1R )  =  ( F `  m ) )
10087, 99breqtrd 3922 . . 3  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  1o )  +R  -1R )  <R 
( F `  m
) )
101100ralrimiva 2480 . 2  |-  ( ph  ->  A. m  e.  N.  ( ( F `  1o )  +R  -1R )  <R  ( F `  m
) )
1021, 2, 101caucvgsrlembnd 7573 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 ) ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ w3o 944    /\ w3a 945    = wceq 1314    e. wcel 1463   {cab 2101   A.wral 2391   E.wrex 2392   <.cop 3498   class class class wbr 3897   -->wf 5087   ` cfv 5091  (class class class)co 5740   1oc1o 6272   [cec 6393   N.cnpi 7044    <N clti 7047    ~Q ceq 7051   1Qc1q 7053   *Qcrq 7056    <Q cltq 7057   1Pc1p 7064    +P. cpp 7065    ~R cer 7068   R.cnr 7069   0Rc0r 7070   1Rc1r 7071   -1Rcm1r 7072    +R cplr 7073    <R cltr 7075
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-eprel 4179  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-1o 6279  df-2o 6280  df-oadd 6283  df-omul 6284  df-er 6395  df-ec 6397  df-qs 6401  df-ni 7076  df-pli 7077  df-mi 7078  df-lti 7079  df-plpq 7116  df-mpq 7117  df-enq 7119  df-nqqs 7120  df-plqqs 7121  df-mqqs 7122  df-1nqqs 7123  df-rq 7124  df-ltnqqs 7125  df-enq0 7196  df-nq0 7197  df-0nq0 7198  df-plq0 7199  df-mq0 7200  df-inp 7238  df-i1p 7239  df-iplp 7240  df-imp 7241  df-iltp 7242  df-enr 7498  df-nr 7499  df-plr 7500  df-mr 7501  df-ltr 7502  df-0r 7503  df-1r 7504  df-m1r 7505
This theorem is referenced by:  axcaucvglemres  7671
  Copyright terms: Public domain W3C validator