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

Theorem axcaucvglemcau 7583
Description: Lemma for axcaucvg 7585. 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 7542 . . . . . . . . . 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 273 . . . . . . . . 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 3879 . . . . . . . . . . 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 5353 . . . . . . . . . . . . . 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 5721 . . . . . . . . . . . . 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 3887 . . . . . . . . . . . 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 3885 . . . . . . . . . . . 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 460 . . . . . . . . . . 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 3878 . . . . . . . . . . . . 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 5353 . . . . . . . . . . . . . . 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 5713 . . . . . . . . . . . . . . . . . 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 2108 . . . . . . . . . . . . . . . . 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 5664 . . . . . . . . . . . . . . . 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 5722 . . . . . . . . . . . . . . 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 3888 . . . . . . . . . . . . . 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 5724 . . . . . . . . . . . . . . 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 3887 . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . 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 2396 . . . . . . . . . . 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 3878 . . . . . . . . . . . . . . 15  |-  ( n  =  a  ->  (
n  <RR  k  <->  a  <RR  k ) )
24 fveq2 5353 . . . . . . . . . . . . . . . . 17  |-  ( n  =  a  ->  ( F `  n )  =  ( F `  a ) )
25 oveq1 5713 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  a  ->  (
n  x.  r )  =  ( a  x.  r ) )
2625eqeq1d 2108 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  a  ->  (
( n  x.  r
)  =  1  <->  (
a  x.  r )  =  1 ) )
2726riotabidv 5664 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  a  ->  ( iota_ r  e.  RR  (
n  x.  r )  =  1 )  =  ( iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )
2827oveq2d 5722 . . . . . . . . . . . . . . . . 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 3888 . . . . . . . . . . . . . . . 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 5724 . . . . . . . . . . . . . . . . 17  |-  ( n  =  a  ->  (
( F `  n
)  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  =  ( ( F `  a )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) )
3130breq2d 3887 . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . 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 3879 . . . . . . . . . . . . . . 15  |-  ( k  =  b  ->  (
a  <RR  k  <->  a  <RR  b ) )
35 fveq2 5353 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  b  ->  ( F `  k )  =  ( F `  b ) )
3635oveq1d 5721 . . . . . . . . . . . . . . . . 17  |-  ( k  =  b  ->  (
( F `  k
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  =  ( ( F `  b )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) )
3736breq2d 3887 . . . . . . . . . . . . . . . 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 3885 . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . 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 2620 . . . . . . . . . . . . 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 479 . . . . . . . . . . 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 7535 . . . . . . . . . . . . 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, 45syl6eleqr 2193 . . . . . . . . . . . 12  |-  ( n  e.  N.  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. n ,  1o >. ]  ~Q  } ,  { u  |  [ <. n ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  N )
4746ad3antlr 480 . . . . . . . . . . 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 2749 . . . . . . . . . 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 7535 . . . . . . . . . . . 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, 45syl6eleqr 2193 . . . . . . . . . . 11  |-  ( k  e.  N.  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. k ,  1o >. ]  ~Q  } ,  { u  |  [ <. k ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  N )
5150ad2antlr 476 . . . . . . . . . 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 2749 . . . . . . . . 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 7582 . . . . . . . 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 475 . . . . . . 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 7582 . . . . . . . . . . 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 464 . . . . . . . . . 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 272 . . . . . . . . 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 7575 . . . . . . . . . 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 480 . . . . . . . . 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 5724 . . . . . . . 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 7581 . . . . . . . . . . 11  |-  ( ph  ->  G : N. --> R. )
6665ad3antrrr 479 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  G : N.
--> R. )
67 simplr 500 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  k  e.  N. )
6866, 67ffvelrnd 5488 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( G `  k )  e.  R. )
69 recnnpr 7257 . . . . . . . . . . 11  |-  ( n  e.  N.  ->  <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  e.  P. )
70 prsrcl 7479 . . . . . . . . . . 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 480 . . . . . . . . 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 7524 . . . . . . . . 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 406 . . . . . . . 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 2132 . . . . . . 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 3904 . . . . . 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 7526 . . . . . 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 5724 . . . . . . . 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 504 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  n  e.  N. )
8266, 81ffvelrnd 5488 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( G `  n )  e.  R. )
83 addresr 7524 . . . . . . . . 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 406 . . . . . . . 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 2132 . . . . . . 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 3904 . . . . . 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 7526 . . . . . 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 302 . . . 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 2464 . 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 2464 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 1299    e. wcel 1448   {cab 2086   A.wral 2375   <.cop 3477   |^|cint 3718   class class class wbr 3875    |-> cmpt 3929   -->wf 5055   ` cfv 5059   iota_crio 5661  (class class class)co 5706   1oc1o 6236   [cec 6357   N.cnpi 6981    <N clti 6984    ~Q ceq 6988   *Qcrq 6993    <Q cltq 6994   P.cnp 7000   1Pc1p 7001    +P. cpp 7002    ~R cer 7005   R.cnr 7006   0Rc0r 7007    +R cplr 7010    <R cltr 7012   RRcr 7499   1c1 7501    + caddc 7503    <RR cltrr 7504    x. cmul 7505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-coll 3983  ax-sep 3986  ax-nul 3994  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-iinf 4440
This theorem depends on definitions:  df-bi 116  df-dc 787  df-3or 931  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-ral 2380  df-rex 2381  df-reu 2382  df-rmo 2383  df-rab 2384  df-v 2643  df-sbc 2863  df-csb 2956  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-nul 3311  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-int 3719  df-iun 3762  df-br 3876  df-opab 3930  df-mpt 3931  df-tr 3967  df-eprel 4149  df-id 4153  df-po 4156  df-iso 4157  df-iord 4226  df-on 4228  df-suc 4231  df-iom 4443  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066  df-fv 5067  df-riota 5662  df-ov 5709  df-oprab 5710  df-mpo 5711  df-1st 5969  df-2nd 5970  df-recs 6132  df-irdg 6197  df-1o 6243  df-2o 6244  df-oadd 6247  df-omul 6248  df-er 6359  df-ec 6361  df-qs 6365  df-ni 7013  df-pli 7014  df-mi 7015  df-lti 7016  df-plpq 7053  df-mpq 7054  df-enq 7056  df-nqqs 7057  df-plqqs 7058  df-mqqs 7059  df-1nqqs 7060  df-rq 7061  df-ltnqqs 7062  df-enq0 7133  df-nq0 7134  df-0nq0 7135  df-plq0 7136  df-mq0 7137  df-inp 7175  df-i1p 7176  df-iplp 7177  df-imp 7178  df-iltp 7179  df-enr 7422  df-nr 7423  df-plr 7424  df-mr 7425  df-ltr 7426  df-0r 7427  df-1r 7428  df-m1r 7429  df-c 7506  df-0 7507  df-1 7508  df-r 7510  df-add 7511  df-mul 7512  df-lt 7513
This theorem is referenced by:  axcaucvglemres  7584
  Copyright terms: Public domain W3C validator