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

Theorem caucvgsr 7040
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 6964 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 7039).

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

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

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

5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7038). (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 1pi 6567 . . . . . . . . . . 11  |-  1o  e.  N.
4 breq1 3796 . . . . . . . . . . . . . 14  |-  ( n  =  1o  ->  (
n  <N  k  <->  1o  <N  k ) )
5 fveq2 5209 . . . . . . . . . . . . . . . 16  |-  ( n  =  1o  ->  ( F `  n )  =  ( F `  1o ) )
6 opeq1 3578 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  1o  ->  <. n ,  1o >.  =  <. 1o ,  1o >. )
76eceq1d 6208 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  1o  ->  [ <. n ,  1o >. ]  ~Q  =  [ <. 1o ,  1o >. ]  ~Q  )
87fveq2d 5213 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  1o  ->  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  =  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) )
98breq2d 3805 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  1o  ->  (
l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <->  l  <Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) ) )
109abbidv 2197 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  1o  ->  { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) }  =  { l  |  l  <Q  ( *Q
`  [ <. 1o ,  1o >. ]  ~Q  ) } )
118breq1d 3803 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  1o  ->  (
( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u  <->  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u ) )
1211abbidv 2197 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  1o  ->  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u }  =  {
u  |  ( *Q
`  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } )
1310, 12opeq12d 3586 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 } >. )
1413oveq1d 5558 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) )
1514opeq1d 3584 . . . . . . . . . . . . . . . . . 18  |-  ( 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 >. )
1615eceq1d 6208 . . . . . . . . . . . . . . . . 17  |-  ( 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  )
1716oveq2d 5559 . . . . . . . . . . . . . . . 16  |-  ( 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  ) )
185, 17breq12d 3806 . . . . . . . . . . . . . . 15  |-  ( 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  ) ) )
195, 16oveq12d 5561 . . . . . . . . . . . . . . . 16  |-  ( 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  ) )
2019breq2d 3805 . . . . . . . . . . . . . . 15  |-  ( 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  ) ) )
2118, 20anbi12d 457 . . . . . . . . . . . . . 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 `  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  ) ) ) )
224, 21imbi12d 232 . . . . . . . . . . . . 13  |-  ( 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  ) ) ) ) )
2322ralbidv 2369 . . . . . . . . . . . 12  |-  ( 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  ) ) ) ) )
2423rspcv 2698 . . . . . . . . . . 11  |-  ( 1o  e.  N.  ->  ( 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  ) ) )  ->  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  ) ) ) ) )
253, 2, 24mpsyl 64 . . . . . . . . . 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 107 . . . . . . . . . . . 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 2427 . . . . . . . . . 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 3797 . . . . . . . . . . 11  |-  ( k  =  m  ->  ( 1o  <N  k  <->  1o  <N  m ) )
31 fveq2 5209 . . . . . . . . . . . . 13  |-  ( k  =  m  ->  ( F `  k )  =  ( F `  m ) )
3231oveq1d 5558 . . . . . . . . . . . 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 3805 . . . . . . . . . . 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 232 . . . . . . . . . 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 2698 . . . . . . . . 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 275 . . . . . . . 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 6603 . . . . . . . . . . . . . . . . . . . 20  |-  1Q  =  [ <. 1o ,  1o >. ]  ~Q
3837fveq2i 5212 . . . . . . . . . . . . . . . . . . 19  |-  ( *Q
`  1Q )  =  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )
39 rec1nq 6647 . . . . . . . . . . . . . . . . . . 19  |-  ( *Q
`  1Q )  =  1Q
4038, 39eqtr3i 2104 . . . . . . . . . . . . . . . . . 18  |-  ( *Q
`  [ <. 1o ,  1o >. ]  ~Q  )  =  1Q
4140breq2i 3801 . . . . . . . . . . . . . . . . 17  |-  ( l 
<Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <->  l  <Q  1Q )
4241abbii 2195 . . . . . . . . . . . . . . . 16  |-  { l  |  l  <Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) }  =  { l  |  l  <Q  1Q }
4340breq1i 3800 . . . . . . . . . . . . . . . . 17  |-  ( ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u  <->  1Q  <Q  u )
4443abbii 2195 . . . . . . . . . . . . . . . 16  |-  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u }  =  {
u  |  1Q  <Q  u }
4542, 44opeq12i 3583 . . . . . . . . . . . . . . 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 6719 . . . . . . . . . . . . . . 15  |-  1P  =  <. { l  |  l 
<Q  1Q } ,  {
u  |  1Q  <Q  u } >.
4745, 46eqtr4i 2105 . . . . . . . . . . . . . 14  |-  <. { l  |  l  <Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } >.  =  1P
4847oveq1i 5553 . . . . . . . . . . . . 13  |-  ( <. { l  |  l 
<Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P )  =  ( 1P  +P.  1P )
4948opeq1i 3581 . . . . . . . . . . . 12  |-  <. ( <. { l  |  l 
<Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >.  =  <. ( 1P  +P.  1P ) ,  1P >.
50 eceq1 6207 . . . . . . . . . . . 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 7 . . . . . . . . . . 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 6971 . . . . . . . . . . 11  |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
5351, 52eqtr4i 2105 . . . . . . . . . 10  |-  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. 1o ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  =  1R
5453oveq2i 5554 . . . . . . . . 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 3801 . . . . . . . 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 159 . . . . . . 7  |-  ( (
ph  /\  m  e.  N. )  ->  ( 1o 
<N  m  ->  ( F `
 1o )  <R 
( ( F `  m )  +R  1R ) ) )
5756imp 122 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  1o  <N  m )  ->  ( F `  1o )  <R  ( ( F `  m )  +R  1R ) )
581adantr 270 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  N. )  ->  F : N.
--> R. )
593a1i 9 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  N. )  ->  1o  e.  N. )
6058, 59ffvelrnd 5335 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  N. )  ->  ( F `
 1o )  e. 
R. )
61 ltadd1sr 7015 . . . . . . . . 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 270 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  N. )  /\  1o  =  m )  ->  ( F `  1o )  <R  ( ( F `  1o )  +R  1R )
)
64 fveq2 5209 . . . . . . . . 9  |-  ( 1o  =  m  ->  ( F `  1o )  =  ( F `  m ) )
6564oveq1d 5558 . . . . . . . 8  |-  ( 1o  =  m  ->  (
( F `  1o )  +R  1R )  =  ( ( F `  m )  +R  1R ) )
6665adantl 271 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  N. )  /\  1o  =  m )  ->  (
( F `  1o )  +R  1R )  =  ( ( F `  m )  +R  1R ) )
6763, 66breqtrd 3817 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  1o  =  m )  ->  ( F `  1o )  <R  ( ( F `  m )  +R  1R ) )
68 nlt1pig 6593 . . . . . . . . 9  |-  ( m  e.  N.  ->  -.  m  <N  1o )
6968adantl 271 . . . . . . . 8  |-  ( (
ph  /\  m  e.  N. )  ->  -.  m  <N  1o )
7069pm2.21d 582 . . . . . . 7  |-  ( (
ph  /\  m  e.  N. )  ->  ( m 
<N  1o  ->  ( F `  1o )  <R  (
( F `  m
)  +R  1R )
) )
7170imp 122 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  m  <N  1o )  ->  ( F `  1o )  <R  ( ( F `  m )  +R  1R ) )
72 pitri3or 6574 . . . . . . . 8  |-  ( ( 1o  e.  N.  /\  m  e.  N. )  ->  ( 1o  <N  m  \/  1o  =  m  \/  m  <N  1o )
)
733, 72mpan 415 . . . . . . 7  |-  ( m  e.  N.  ->  ( 1o  <N  m  \/  1o  =  m  \/  m  <N  1o ) )
7473adantl 271 . . . . . 6  |-  ( (
ph  /\  m  e.  N. )  ->  ( 1o 
<N  m  \/  1o  =  m  \/  m  <N  1o ) )
7557, 67, 71, 74mpjao3dan 1239 . . . . 5  |-  ( (
ph  /\  m  e.  N. )  ->  ( F `
 1o )  <R 
( ( F `  m )  +R  1R ) )
76 ltasrg 7009 . . . . . . 7  |-  ( ( f  e.  R.  /\  g  e.  R.  /\  h  e.  R. )  ->  (
f  <R  g  <->  ( h  +R  f )  <R  (
h  +R  g ) ) )
7776adantl 271 . . . . . 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 5334 . . . . . . 7  |-  ( (
ph  /\  m  e.  N. )  ->  ( F `
 m )  e. 
R. )
79 1sr 6990 . . . . . . 7  |-  1R  e.  R.
80 addclsr 6992 . . . . . . 7  |-  ( ( ( F `  m
)  e.  R.  /\  1R  e.  R. )  -> 
( ( F `  m )  +R  1R )  e.  R. )
8178, 79, 80sylancl 404 . . . . . 6  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  m )  +R  1R )  e. 
R. )
82 m1r 6991 . . . . . . 7  |-  -1R  e.  R.
8382a1i 9 . . . . . 6  |-  ( (
ph  /\  m  e.  N. )  ->  -1R  e.  R. )
84 addcomsrg 6994 . . . . . . 7  |-  ( ( f  e.  R.  /\  g  e.  R. )  ->  ( f  +R  g
)  =  ( g  +R  f ) )
8584adantl 271 . . . . . 6  |-  ( ( ( ph  /\  m  e.  N. )  /\  (
f  e.  R.  /\  g  e.  R. )
)  ->  ( f  +R  g )  =  ( g  +R  f ) )
8677, 60, 81, 83, 85caovord2d 5701 . . . . 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 145 . . . 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 6995 . . . . . 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 1170 . . . . 5  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( ( F `  m
)  +R  1R )  +R  -1R )  =  ( ( F `  m
)  +R  ( 1R 
+R  -1R ) ) )
91 addcomsrg 6994 . . . . . . . . 9  |-  ( ( 1R  e.  R.  /\  -1R  e.  R. )  -> 
( 1R  +R  -1R )  =  ( -1R  +R 
1R ) )
9279, 82, 91mp2an 417 . . . . . . . 8  |-  ( 1R 
+R  -1R )  =  ( -1R  +R  1R )
93 m1p1sr 6999 . . . . . . . 8  |-  ( -1R 
+R  1R )  =  0R
9492, 93eqtri 2102 . . . . . . 7  |-  ( 1R 
+R  -1R )  =  0R
9594oveq2i 5554 . . . . . 6  |-  ( ( F `  m )  +R  ( 1R  +R  -1R ) )  =  ( ( F `  m
)  +R  0R )
96 0idsr 7006 . . . . . . 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 2126 . . . . 5  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  m )  +R  ( 1R  +R  -1R ) )  =  ( F `  m ) )
9990, 98eqtrd 2114 . . . 4  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( ( F `  m
)  +R  1R )  +R  -1R )  =  ( F `  m ) )
10087, 99breqtrd 3817 . . 3  |-  ( (
ph  /\  m  e.  N. )  ->  ( ( F `  1o )  +R  -1R )  <R 
( F `  m
) )
101100ralrimiva 2435 . 2  |-  ( ph  ->  A. m  e.  N.  ( ( F `  1o )  +R  -1R )  <R  ( F `  m
) )
1021, 2, 101caucvgsrlembnd 7039 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 102    <-> wb 103    \/ w3o 919    /\ w3a 920    = wceq 1285    e. wcel 1434   {cab 2068   A.wral 2349   E.wrex 2350   <.cop 3409   class class class wbr 3793   -->wf 4928   ` cfv 4932  (class class class)co 5543   1oc1o 6058   [cec 6170   N.cnpi 6524    <N clti 6527    ~Q ceq 6531   1Qc1q 6533   *Qcrq 6536    <Q cltq 6537   1Pc1p 6544    +P. cpp 6545    ~R cer 6548   R.cnr 6549   0Rc0r 6550   1Rc1r 6551   -1Rcm1r 6552    +R cplr 6553    <R cltr 6555
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-coll 3901  ax-sep 3904  ax-nul 3912  ax-pow 3956  ax-pr 3972  ax-un 4196  ax-setind 4288  ax-iinf 4337
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1687  df-eu 1945  df-mo 1946  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ne 2247  df-ral 2354  df-rex 2355  df-reu 2356  df-rmo 2357  df-rab 2358  df-v 2604  df-sbc 2817  df-csb 2910  df-dif 2976  df-un 2978  df-in 2980  df-ss 2987  df-nul 3259  df-pw 3392  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-int 3645  df-iun 3688  df-br 3794  df-opab 3848  df-mpt 3849  df-tr 3884  df-eprel 4052  df-id 4056  df-po 4059  df-iso 4060  df-iord 4129  df-on 4131  df-suc 4134  df-iom 4340  df-xp 4377  df-rel 4378  df-cnv 4379  df-co 4380  df-dm 4381  df-rn 4382  df-res 4383  df-ima 4384  df-iota 4897  df-fun 4934  df-fn 4935  df-f 4936  df-f1 4937  df-fo 4938  df-f1o 4939  df-fv 4940  df-riota 5499  df-ov 5546  df-oprab 5547  df-mpt2 5548  df-1st 5798  df-2nd 5799  df-recs 5954  df-irdg 6019  df-1o 6065  df-2o 6066  df-oadd 6069  df-omul 6070  df-er 6172  df-ec 6174  df-qs 6178  df-ni 6556  df-pli 6557  df-mi 6558  df-lti 6559  df-plpq 6596  df-mpq 6597  df-enq 6599  df-nqqs 6600  df-plqqs 6601  df-mqqs 6602  df-1nqqs 6603  df-rq 6604  df-ltnqqs 6605  df-enq0 6676  df-nq0 6677  df-0nq0 6678  df-plq0 6679  df-mq0 6680  df-inp 6718  df-i1p 6719  df-iplp 6720  df-imp 6721  df-iltp 6722  df-enr 6965  df-nr 6966  df-plr 6967  df-mr 6968  df-ltr 6969  df-0r 6970  df-1r 6971  df-m1r 6972
This theorem is referenced by:  axcaucvglemres  7127
  Copyright terms: Public domain W3C validator