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

Theorem axcaucvglemcau 7718
Description: Lemma for axcaucvg 7720. The result of mapping to  N. and  R. satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.)
Hypotheses
Ref Expression
axcaucvg.n  |-  N  = 
|^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
axcaucvg.f  |-  ( ph  ->  F : N --> RR )
axcaucvg.cau  |-  ( ph  ->  A. n  e.  N  A. k  e.  N  ( n  <RR  k  -> 
( ( F `  n )  <RR  ( ( F `  k )  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  /\  ( F `  k )  <RR  ( ( F `  n )  +  (
iota_ r  e.  RR  ( n  x.  r
)  =  1 ) ) ) ) )
axcaucvg.g  |-  G  =  ( j  e.  N.  |->  ( iota_ z  e.  R.  ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. j ,  1o >. ]  ~Q  } ,  { u  |  [ <. j ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. z ,  0R >. )
)
Assertion
Ref Expression
axcaucvglemcau  |-  ( ph  ->  A. n  e.  N.  A. k  e.  N.  (
n  <N  k  ->  (
( G `  n
)  <R  ( ( G `
 k )  +R 
[ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )  /\  ( G `  k )  <R  (
( G `  n
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ) ) )
Distinct variable groups:    k, F, n, z, j    k, N, n    z, G    k,
l, r, u, n   
j, l, u, z    ph, j, k, n    y,
l, u    x, y    j, n, z, k
Allowed substitution hints:    ph( x, y, z, u, r, l)    F( x, y, u, r, l)    G( x, y, u, j, k, n, r, l)    N( x, y, z, u, j, r, l)

Proof of Theorem axcaucvglemcau
Dummy variables  a  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrenn 7675 . . . . . . . . . 10  |-  ( n 
<N  k  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
21adantl 275 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
3 breq2 3933 . . . . . . . . . . 11  |-  ( b  =  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  b  <->  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. ) )
4 fveq2 5421 . . . . . . . . . . . . . 14  |-  ( b  =  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( F `  b )  =  ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. ) )
54oveq1d 5789 . . . . . . . . . . . . 13  |-  ( b  =  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  =  ( ( F `
 <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) )
65breq2d 3941 . . . . . . . . . . . 12  |-  ( b  =  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  <-> 
( F `  <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) )
74breq1d 3939 . . . . . . . . . . . 12  |-  ( b  =  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  b )  <RR  ( ( F `  <. [ <. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  <-> 
( F `  <. [
<. ( <. { l  |  l  <Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) )
86, 7anbi12d 464 . . . . . . . . . . 11  |-  ( b  =  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( (
( F `  <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  b )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) )  <->  ( ( F `
 <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  <. [ <. ( <. { l  |  l  <Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) ) )
93, 8imbi12d 233 . . . . . . . . . 10  |-  ( b  =  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( <. [ <. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  b  ->  (
( F `  <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  b )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) )  <->  ( <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  <. [ <. ( <. { l  |  l  <Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) ) ) )
10 breq1 3932 . . . . . . . . . . . . 13  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( a  <RR  b  <->  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  b ) )
11 fveq2 5421 . . . . . . . . . . . . . . 15  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( F `  a )  =  ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. ) )
12 oveq1 5781 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( a  x.  r )  =  (
<. [ <. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r ) )
1312eqeq1d 2148 . . . . . . . . . . . . . . . . 17  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( (
a  x.  r )  =  1  <->  ( <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )
1413riotabidv 5732 . . . . . . . . . . . . . . . 16  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( iota_ r  e.  RR  ( a  x.  r )  =  1 )  =  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )
1514oveq2d 5790 . . . . . . . . . . . . . . 15  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  b )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  =  ( ( F `  b
)  +  ( iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) )
1611, 15breq12d 3942 . . . . . . . . . . . . . 14  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  a )  <RR  ( ( F `  b )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  <->  ( F `  <. [ <. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) )
1711, 14oveq12d 5792 . . . . . . . . . . . . . . 15  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  a )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  =  ( ( F `  <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) )
1817breq2d 3941 . . . . . . . . . . . . . 14  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  b )  <RR  ( ( F `  a )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  <->  ( F `  b )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) )
1916, 18anbi12d 464 . . . . . . . . . . . . 13  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( (
( F `  a
)  <RR  ( ( F `
 b )  +  ( iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  /\  ( F `
 b )  <RR  ( ( F `  a
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) )  <-> 
( ( F `  <. [ <. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  b )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) ) )
2010, 19imbi12d 233 . . . . . . . . . . . 12  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( (
a  <RR  b  ->  (
( F `  a
)  <RR  ( ( F `
 b )  +  ( iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  /\  ( F `
 b )  <RR  ( ( F `  a
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) )  <->  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  b  ->  (
( F `  <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  b )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) ) ) )
2120ralbidv 2437 . . . . . . . . . . 11  |-  ( a  =  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( A. b  e.  N  (
a  <RR  b  ->  (
( F `  a
)  <RR  ( ( F `
 b )  +  ( iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  /\  ( F `
 b )  <RR  ( ( F `  a
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) )  <->  A. b  e.  N  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  b  ->  (
( F `  <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  b )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) ) ) )
22 axcaucvg.cau . . . . . . . . . . . . 13  |-  ( ph  ->  A. n  e.  N  A. k  e.  N  ( n  <RR  k  -> 
( ( F `  n )  <RR  ( ( F `  k )  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  /\  ( F `  k )  <RR  ( ( F `  n )  +  (
iota_ r  e.  RR  ( n  x.  r
)  =  1 ) ) ) ) )
23 breq1 3932 . . . . . . . . . . . . . . 15  |-  ( n  =  a  ->  (
n  <RR  k  <->  a  <RR  k ) )
24 fveq2 5421 . . . . . . . . . . . . . . . . 17  |-  ( n  =  a  ->  ( F `  n )  =  ( F `  a ) )
25 oveq1 5781 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  a  ->  (
n  x.  r )  =  ( a  x.  r ) )
2625eqeq1d 2148 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  a  ->  (
( n  x.  r
)  =  1  <->  (
a  x.  r )  =  1 ) )
2726riotabidv 5732 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  a  ->  ( iota_ r  e.  RR  (
n  x.  r )  =  1 )  =  ( iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )
2827oveq2d 5790 . . . . . . . . . . . . . . . . 17  |-  ( n  =  a  ->  (
( F `  k
)  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  =  ( ( F `  k )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) )
2924, 28breq12d 3942 . . . . . . . . . . . . . . . 16  |-  ( n  =  a  ->  (
( F `  n
)  <RR  ( ( F `
 k )  +  ( iota_ r  e.  RR  ( n  x.  r
)  =  1 ) )  <->  ( F `  a )  <RR  ( ( F `  k )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) )
3024, 27oveq12d 5792 . . . . . . . . . . . . . . . . 17  |-  ( n  =  a  ->  (
( F `  n
)  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  =  ( ( F `  a )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) )
3130breq2d 3941 . . . . . . . . . . . . . . . 16  |-  ( n  =  a  ->  (
( F `  k
)  <RR  ( ( F `
 n )  +  ( iota_ r  e.  RR  ( n  x.  r
)  =  1 ) )  <->  ( F `  k )  <RR  ( ( F `  a )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) )
3229, 31anbi12d 464 . . . . . . . . . . . . . . 15  |-  ( n  =  a  ->  (
( ( F `  n )  <RR  ( ( F `  k )  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  /\  ( F `  k )  <RR  ( ( F `  n )  +  (
iota_ r  e.  RR  ( n  x.  r
)  =  1 ) ) )  <->  ( ( F `  a )  <RR  ( ( F `  k )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  /\  ( F `
 k )  <RR  ( ( F `  a
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) ) )
3323, 32imbi12d 233 . . . . . . . . . . . . . 14  |-  ( n  =  a  ->  (
( n  <RR  k  -> 
( ( F `  n )  <RR  ( ( F `  k )  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  /\  ( F `  k )  <RR  ( ( F `  n )  +  (
iota_ r  e.  RR  ( n  x.  r
)  =  1 ) ) ) )  <->  ( a  <RR  k  ->  ( ( F `  a )  <RR  ( ( F `  k )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  /\  ( F `
 k )  <RR  ( ( F `  a
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) ) ) )
34 breq2 3933 . . . . . . . . . . . . . . 15  |-  ( k  =  b  ->  (
a  <RR  k  <->  a  <RR  b ) )
35 fveq2 5421 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  b  ->  ( F `  k )  =  ( F `  b ) )
3635oveq1d 5789 . . . . . . . . . . . . . . . . 17  |-  ( k  =  b  ->  (
( F `  k
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  =  ( ( F `  b )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) )
3736breq2d 3941 . . . . . . . . . . . . . . . 16  |-  ( k  =  b  ->  (
( F `  a
)  <RR  ( ( F `
 k )  +  ( iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  <->  ( F `  a )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) )
3835breq1d 3939 . . . . . . . . . . . . . . . 16  |-  ( k  =  b  ->  (
( F `  k
)  <RR  ( ( F `
 a )  +  ( iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  <->  ( F `  b )  <RR  ( ( F `  a )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) )
3937, 38anbi12d 464 . . . . . . . . . . . . . . 15  |-  ( k  =  b  ->  (
( ( F `  a )  <RR  ( ( F `  k )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  /\  ( F `  k )  <RR  ( ( F `  a )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) )  <->  ( ( F `  a )  <RR  ( ( F `  b )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  /\  ( F `
 b )  <RR  ( ( F `  a
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) ) )
4034, 39imbi12d 233 . . . . . . . . . . . . . 14  |-  ( k  =  b  ->  (
( a  <RR  k  -> 
( ( F `  a )  <RR  ( ( F `  k )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  /\  ( F `  k )  <RR  ( ( F `  a )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) ) )  <->  ( a  <RR  b  ->  ( ( F `  a )  <RR  ( ( F `  b )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  /\  ( F `
 b )  <RR  ( ( F `  a
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) ) ) )
4133, 40cbvral2v 2665 . . . . . . . . . . . . 13  |-  ( A. n  e.  N  A. k  e.  N  (
n  <RR  k  ->  (
( F `  n
)  <RR  ( ( F `
 k )  +  ( iota_ r  e.  RR  ( n  x.  r
)  =  1 ) )  /\  ( F `
 k )  <RR  ( ( F `  n
)  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) ) ) )  <->  A. a  e.  N  A. b  e.  N  ( a  <RR  b  -> 
( ( F `  a )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  /\  ( F `  b )  <RR  ( ( F `  a )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) ) ) )
4222, 41sylib 121 . . . . . . . . . . . 12  |-  ( ph  ->  A. a  e.  N  A. b  e.  N  ( a  <RR  b  -> 
( ( F `  a )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  /\  ( F `  b )  <RR  ( ( F `  a )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) ) ) )
4342ad3antrrr 483 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  A. a  e.  N  A. b  e.  N  ( a  <RR  b  ->  ( ( F `  a )  <RR  ( ( F `  b )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )  /\  ( F `
 b )  <RR  ( ( F `  a
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) ) ) ) )
44 pitonn 7668 . . . . . . . . . . . . 13  |-  ( n  e.  N.  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } )
45 axcaucvg.n . . . . . . . . . . . . 13  |-  N  = 
|^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
4644, 45eleqtrrdi 2233 . . . . . . . . . . . 12  |-  ( n  e.  N.  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  N )
4746ad3antlr 484 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  N )
4821, 43, 47rspcdva 2794 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  A. b  e.  N  ( <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  b  ->  (
( F `  <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  b )  +  ( iota_ r  e.  RR  ( <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  b )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) ) )
49 pitonn 7668 . . . . . . . . . . . 12  |-  ( k  e.  N.  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } )
5049, 45eleqtrrdi 2233 . . . . . . . . . . 11  |-  ( k  e.  N.  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  N )
5150ad2antlr 480 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  N )
529, 48, 51rspcdva 2794 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( <. [
<. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  <. [ <. ( <. { l  |  l  <Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) ) )
532, 52mpd 13 . . . . . . . 8  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  /\  ( F `  <. [ <. ( <. { l  |  l  <Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) ) )
5453simpld 111 . . . . . . 7  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( F `  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) )
55 axcaucvg.f . . . . . . . . 9  |-  ( ph  ->  F : N --> RR )
56 axcaucvg.g . . . . . . . . 9  |-  G  =  ( j  e.  N.  |->  ( iota_ z  e.  R.  ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. j ,  1o >. ]  ~Q  } ,  { u  |  [ <. j ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. z ,  0R >. )
)
5745, 55, 22, 56axcaucvglemval 7717 . . . . . . . 8  |-  ( (
ph  /\  n  e.  N. )  ->  ( F `
 <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( G `  n ) ,  0R >. )
5857ad2antrr 479 . . . . . . 7  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( F `  <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( G `  n ) ,  0R >. )
5945, 55, 22, 56axcaucvglemval 7717 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  N. )  ->  ( F `
 <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( G `  k ) ,  0R >. )
6059adantlr 468 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  ->  ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( G `  k ) ,  0R >. )
6160adantr 274 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( F `  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( G `  k ) ,  0R >. )
62 recriota 7710 . . . . . . . . . 10  |-  ( n  e.  N.  ->  ( iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 )  = 
<. [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
6362ad3antlr 484 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l  <Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 )  = 
<. [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
6461, 63oveq12d 5792 . . . . . . . 8  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  =  ( <. ( G `  k ) ,  0R >.  +  <. [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. ) )
6545, 55, 22, 56axcaucvglemf 7716 . . . . . . . . . . 11  |-  ( ph  ->  G : N. --> R. )
6665ad3antrrr 483 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  G : N.
--> R. )
67 simplr 519 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  k  e.  N. )
6866, 67ffvelrnd 5556 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( G `  k )  e.  R. )
69 recnnpr 7368 . . . . . . . . . . 11  |-  ( n  e.  N.  ->  <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  e.  P. )
70 prsrcl 7604 . . . . . . . . . . 11  |-  ( <. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  e.  P.  ->  [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  e.  R. )
7169, 70syl 14 . . . . . . . . . 10  |-  ( n  e.  N.  ->  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  e.  R. )
7271ad3antlr 484 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  [ <. ( <. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  e.  R. )
73 addresr 7657 . . . . . . . . 9  |-  ( ( ( G `  k
)  e.  R.  /\  [
<. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  e.  R. )  ->  ( <.
( G `  k
) ,  0R >.  + 
<. [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( ( G `  k
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >. )
7468, 72, 73syl2anc 408 . . . . . . . 8  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( <. ( G `  k ) ,  0R >.  +  <. [
<. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( ( G `  k
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >. )
7564, 74eqtrd 2172 . . . . . . 7  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  =  <. ( ( G `
 k )  +R 
[ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >. )
7654, 58, 753brtr3d 3959 . . . . . 6  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  <. ( G `
 n ) ,  0R >.  <RR  <. (
( G `  k
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >. )
77 ltresr 7659 . . . . . 6  |-  ( <.
( G `  n
) ,  0R >.  <RR  <. ( ( G `  k )  +R  [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >.  <->  ( G `  n )  <R  (
( G `  k
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) )
7876, 77sylib 121 . . . . 5  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( G `  n )  <R  (
( G `  k
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) )
7953simprd 113 . . . . . . 7  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( F `  <. [ <. ( <. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  <RR  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) ) )
8058, 63oveq12d 5792 . . . . . . . 8  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  =  ( <. ( G `  n ) ,  0R >.  +  <. [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. ) )
81 simpllr 523 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  n  e.  N. )
8266, 81ffvelrnd 5556 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( G `  n )  e.  R. )
83 addresr 7657 . . . . . . . . 9  |-  ( ( ( G `  n
)  e.  R.  /\  [
<. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  e.  R. )  ->  ( <.
( G `  n
) ,  0R >.  + 
<. [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( ( G `  n
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >. )
8482, 72, 83syl2anc 408 . . . . . . . 8  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( <. ( G `  n ) ,  0R >.  +  <. [
<. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( ( G `  n
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >. )
8580, 84eqtrd 2172 . . . . . . 7  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( ( F `  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  +  (
iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 ) )  =  <. ( ( G `
 n )  +R 
[ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >. )
8679, 61, 853brtr3d 3959 . . . . . 6  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  <. ( G `
 k ) ,  0R >.  <RR  <. (
( G `  n
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >. )
87 ltresr 7659 . . . . . 6  |-  ( <.
( G `  k
) ,  0R >.  <RR  <. ( ( G `  n )  +R  [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ,  0R >.  <->  ( G `  k )  <R  (
( G `  n
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) )
8886, 87sylib 121 . . . . 5  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( G `  k )  <R  (
( G `  n
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) )
8978, 88jca 304 . . . 4  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( ( G `  n )  <R  ( ( G `  k )  +R  [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )  /\  ( G `  k
)  <R  ( ( G `
 n )  +R 
[ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ) )
9089ex 114 . . 3  |-  ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  ->  (
n  <N  k  ->  (
( G `  n
)  <R  ( ( G `
 k )  +R 
[ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )  /\  ( G `  k )  <R  (
( G `  n
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ) ) )
9190ralrimiva 2505 . 2  |-  ( (
ph  /\  n  e.  N. )  ->  A. k  e.  N.  ( n  <N  k  ->  ( ( G `
 n )  <R 
( ( G `  k )  +R  [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )  /\  ( G `  k
)  <R  ( ( G `
 n )  +R 
[ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ) ) )
9291ralrimiva 2505 1  |-  ( ph  ->  A. n  e.  N.  A. k  e.  N.  (
n  <N  k  ->  (
( G `  n
)  <R  ( ( G `
 k )  +R 
[ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )  /\  ( G `  k )  <R  (
( G `  n
)  +R  [ <. (
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1331    e. wcel 1480   {cab 2125   A.wral 2416   <.cop 3530   |^|cint 3771   class class class wbr 3929    |-> cmpt 3989   -->wf 5119   ` cfv 5123   iota_crio 5729  (class class class)co 5774   1oc1o 6306   [cec 6427   N.cnpi 7092    <N clti 7095    ~Q ceq 7099   *Qcrq 7104    <Q cltq 7105   P.cnp 7111   1Pc1p 7112    +P. cpp 7113    ~R cer 7116   R.cnr 7117   0Rc0r 7118    +R cplr 7121    <R cltr 7123   RRcr 7631   1c1 7633    + caddc 7635    <RR cltrr 7636    x. cmul 7637
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-eprel 4211  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-1o 6313  df-2o 6314  df-oadd 6317  df-omul 6318  df-er 6429  df-ec 6431  df-qs 6435  df-ni 7124  df-pli 7125  df-mi 7126  df-lti 7127  df-plpq 7164  df-mpq 7165  df-enq 7167  df-nqqs 7168  df-plqqs 7169  df-mqqs 7170  df-1nqqs 7171  df-rq 7172  df-ltnqqs 7173  df-enq0 7244  df-nq0 7245  df-0nq0 7246  df-plq0 7247  df-mq0 7248  df-inp 7286  df-i1p 7287  df-iplp 7288  df-imp 7289  df-iltp 7290  df-enr 7546  df-nr 7547  df-plr 7548  df-mr 7549  df-ltr 7550  df-0r 7551  df-1r 7552  df-m1r 7553  df-c 7638  df-0 7639  df-1 7640  df-r 7642  df-add 7643  df-mul 7644  df-lt 7645
This theorem is referenced by:  axcaucvglemres  7719
  Copyright terms: Public domain W3C validator