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

Theorem axcaucvglemcau 7674
Description: Lemma for axcaucvg 7676. 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 7631 . . . . . . . . . 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 3903 . . . . . . . . . . 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 5389 . . . . . . . . . . . . . 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 5757 . . . . . . . . . . . . 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 3911 . . . . . . . . . . . 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 3909 . . . . . . . . . . . 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 3902 . . . . . . . . . . . . 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 5389 . . . . . . . . . . . . . . 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 5749 . . . . . . . . . . . . . . . . . 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 2126 . . . . . . . . . . . . . . . . 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 5700 . . . . . . . . . . . . . . . 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 5758 . . . . . . . . . . . . . . 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 3912 . . . . . . . . . . . . . 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 5760 . . . . . . . . . . . . . . 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 3911 . . . . . . . . . . . . . 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 2414 . . . . . . . . . . 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 3902 . . . . . . . . . . . . . . 15  |-  ( n  =  a  ->  (
n  <RR  k  <->  a  <RR  k ) )
24 fveq2 5389 . . . . . . . . . . . . . . . . 17  |-  ( n  =  a  ->  ( F `  n )  =  ( F `  a ) )
25 oveq1 5749 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  a  ->  (
n  x.  r )  =  ( a  x.  r ) )
2625eqeq1d 2126 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  a  ->  (
( n  x.  r
)  =  1  <->  (
a  x.  r )  =  1 ) )
2726riotabidv 5700 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  a  ->  ( iota_ r  e.  RR  (
n  x.  r )  =  1 )  =  ( iota_ r  e.  RR  ( a  x.  r
)  =  1 ) )
2827oveq2d 5758 . . . . . . . . . . . . . . . . 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 3912 . . . . . . . . . . . . . . . 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 5760 . . . . . . . . . . . . . . . . 17  |-  ( n  =  a  ->  (
( F `  n
)  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) )  =  ( ( F `  a )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) )
3130breq2d 3911 . . . . . . . . . . . . . . . 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 3903 . . . . . . . . . . . . . . 15  |-  ( k  =  b  ->  (
a  <RR  k  <->  a  <RR  b ) )
35 fveq2 5389 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  b  ->  ( F `  k )  =  ( F `  b ) )
3635oveq1d 5757 . . . . . . . . . . . . . . . . 17  |-  ( k  =  b  ->  (
( F `  k
)  +  ( iota_ r  e.  RR  ( a  x.  r )  =  1 ) )  =  ( ( F `  b )  +  (
iota_ r  e.  RR  ( a  x.  r
)  =  1 ) ) )
3736breq2d 3911 . . . . . . . . . . . . . . . 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 3909 . . . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . . 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 7624 . . . . . . . . . . . . 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 2211 . . . . . . . . . . . 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 2768 . . . . . . . . . 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 7624 . . . . . . . . . . . 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 2211 . . . . . . . . . . 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 2768 . . . . . . . . 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 7673 . . . . . . . 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 7673 . . . . . . . . . . 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 7666 . . . . . . . . . 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 5760 . . . . . . . 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 7672 . . . . . . . . . . 11  |-  ( ph  ->  G : N. --> R. )
6665ad3antrrr 483 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  G : N.
--> R. )
67 simplr 504 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  k  e.  N. )
6866, 67ffvelrnd 5524 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( G `  k )  e.  R. )
69 recnnpr 7324 . . . . . . . . . . 11  |-  ( n  e.  N.  ->  <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  e.  P. )
70 prsrcl 7560 . . . . . . . . . . 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 7613 . . . . . . . . 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 2150 . . . . . . 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 3929 . . . . . 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 7615 . . . . . 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 5760 . . . . . . . 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 508 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  n  e.  N. )
8266, 81ffvelrnd 5524 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  N. )  /\  k  e.  N. )  /\  n  <N  k
)  ->  ( G `  n )  e.  R. )
83 addresr 7613 . . . . . . . . 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 2150 . . . . . . 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 3929 . . . . . 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 7615 . . . . . 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 2482 . 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 2482 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 1316    e. wcel 1465   {cab 2103   A.wral 2393   <.cop 3500   |^|cint 3741   class class class wbr 3899    |-> cmpt 3959   -->wf 5089   ` cfv 5093   iota_crio 5697  (class class class)co 5742   1oc1o 6274   [cec 6395   N.cnpi 7048    <N clti 7051    ~Q ceq 7055   *Qcrq 7060    <Q cltq 7061   P.cnp 7067   1Pc1p 7068    +P. cpp 7069    ~R cer 7072   R.cnr 7073   0Rc0r 7074    +R cplr 7077    <R cltr 7079   RRcr 7587   1c1 7589    + caddc 7591    <RR cltrr 7592    x. cmul 7593
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 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-eprel 4181  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-irdg 6235  df-1o 6281  df-2o 6282  df-oadd 6285  df-omul 6286  df-er 6397  df-ec 6399  df-qs 6403  df-ni 7080  df-pli 7081  df-mi 7082  df-lti 7083  df-plpq 7120  df-mpq 7121  df-enq 7123  df-nqqs 7124  df-plqqs 7125  df-mqqs 7126  df-1nqqs 7127  df-rq 7128  df-ltnqqs 7129  df-enq0 7200  df-nq0 7201  df-0nq0 7202  df-plq0 7203  df-mq0 7204  df-inp 7242  df-i1p 7243  df-iplp 7244  df-imp 7245  df-iltp 7246  df-enr 7502  df-nr 7503  df-plr 7504  df-mr 7505  df-ltr 7506  df-0r 7507  df-1r 7508  df-m1r 7509  df-c 7594  df-0 7595  df-1 7596  df-r 7598  df-add 7599  df-mul 7600  df-lt 7601
This theorem is referenced by:  axcaucvglemres  7675
  Copyright terms: Public domain W3C validator