Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wallispilem4 Unicode version

Theorem wallispilem4 27828
Description:  F maps to explicit expression for the ratio of two consecutive values of  I (Contributed by Glauco Siliprandi, 30-Jun-2017.)
Hypotheses
Ref Expression
wallispilem4.1  |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) )
wallispilem4.2  |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  z ) ^ n
)  _d z )
wallispilem4.3  |-  G  =  ( n  e.  NN  |->  ( ( I `  ( 2  x.  n
) )  /  (
I `  ( (
2  x.  n )  +  1 ) ) ) )
wallispilem4.4  |-  H  =  ( n  e.  NN  |->  ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  n
) ) ) )
Assertion
Ref Expression
wallispilem4  |-  G  =  H
Distinct variable groups:    z, n    z, F
Allowed substitution hints:    F( k, n)    G( z, k, n)    H( z, k, n)    I( z,
k, n)

Proof of Theorem wallispilem4
Dummy variables  w  y  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 5868 . . . . . . 7  |-  ( x  =  1  ->  (
2  x.  x )  =  ( 2  x.  1 ) )
21fveq2d 5531 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  1 ) ) )
31oveq1d 5875 . . . . . . 7  |-  ( x  =  1  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
43fveq2d 5531 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  1 )  +  1 ) ) )
52, 4oveq12d 5878 . . . . 5  |-  ( x  =  1  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  1 ) )  / 
( I `  (
( 2  x.  1 )  +  1 ) ) ) )
6 fveq2 5527 . . . . . . 7  |-  ( x  =  1  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  1
) )
76oveq2d 5876 . . . . . 6  |-  ( x  =  1  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq  1 (  x.  ,  F ) `  1
) ) )
87oveq2d 5876 . . . . 5  |-  ( x  =  1  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  1 )
) ) )
95, 8eqeq12d 2299 . . . 4  |-  ( x  =  1  ->  (
( ( I `  ( 2  x.  x
) )  /  (
I `  ( (
2  x.  x )  +  1 ) ) )  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq  1 (  x.  ,  F ) `
 x ) ) )  <->  ( ( I `
 ( 2  x.  1 ) )  / 
( I `  (
( 2  x.  1 )  +  1 ) ) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  1 )
) ) ) )
10 oveq2 5868 . . . . . . 7  |-  ( x  =  y  ->  (
2  x.  x )  =  ( 2  x.  y ) )
1110fveq2d 5531 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  y ) ) )
1210oveq1d 5875 . . . . . . 7  |-  ( x  =  y  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  y )  +  1 ) )
1312fveq2d 5531 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
1411, 13oveq12d 5878 . . . . 5  |-  ( x  =  y  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
15 fveq2 5527 . . . . . . 7  |-  ( x  =  y  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  y
) )
1615oveq2d 5876 . . . . . 6  |-  ( x  =  y  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq  1 (  x.  ,  F ) `  y
) ) )
1716oveq2d 5876 . . . . 5  |-  ( x  =  y  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  y )
) ) )
1814, 17eqeq12d 2299 . . . 4  |-  ( x  =  y  ->  (
( ( I `  ( 2  x.  x
) )  /  (
I `  ( (
2  x.  x )  +  1 ) ) )  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq  1 (  x.  ,  F ) `
 x ) ) )  <->  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  y )
) ) ) )
19 oveq2 5868 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
2  x.  x )  =  ( 2  x.  ( y  +  1 ) ) )
2019fveq2d 5531 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  ( y  +  1 ) ) ) )
2119oveq1d 5875 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
2221fveq2d 5531 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
2320, 22oveq12d 5878 . . . . 5  |-  ( x  =  ( y  +  1 )  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  ( y  +  1 ) ) )  / 
( I `  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) ) )
24 fveq2 5527 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  (
y  +  1 ) ) )
2524oveq2d 5876 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq  1 (  x.  ,  F ) `  (
y  +  1 ) ) ) )
2625oveq2d 5876 . . . . 5  |-  ( x  =  ( y  +  1 )  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  ( y  +  1 ) ) ) ) )
2723, 26eqeq12d 2299 . . . 4  |-  ( x  =  ( y  +  1 )  ->  (
( ( I `  ( 2  x.  x
) )  /  (
I `  ( (
2  x.  x )  +  1 ) ) )  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq  1 (  x.  ,  F ) `
 x ) ) )  <->  ( ( I `
 ( 2  x.  ( y  +  1 ) ) )  / 
( I `  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  ( y  +  1 ) ) ) ) ) )
28 oveq2 5868 . . . . . . 7  |-  ( x  =  n  ->  (
2  x.  x )  =  ( 2  x.  n ) )
2928fveq2d 5531 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  n ) ) )
3028oveq1d 5875 . . . . . . 7  |-  ( x  =  n  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  n )  +  1 ) )
3130fveq2d 5531 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  n )  +  1 ) ) )
3229, 31oveq12d 5878 . . . . 5  |-  ( x  =  n  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  n ) )  / 
( I `  (
( 2  x.  n
)  +  1 ) ) ) )
33 fveq2 5527 . . . . . . 7  |-  ( x  =  n  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  n
) )
3433oveq2d 5876 . . . . . 6  |-  ( x  =  n  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq  1 (  x.  ,  F ) `  n
) ) )
3534oveq2d 5876 . . . . 5  |-  ( x  =  n  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  n )
) ) )
3632, 35eqeq12d 2299 . . . 4  |-  ( x  =  n  ->  (
( ( I `  ( 2  x.  x
) )  /  (
I `  ( (
2  x.  x )  +  1 ) ) )  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq  1 (  x.  ,  F ) `
 x ) ) )  <->  ( ( I `
 ( 2  x.  n ) )  / 
( I `  (
( 2  x.  n
)  +  1 ) ) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  n )
) ) ) )
37 2cn 9818 . . . . . . . 8  |-  2  e.  CC
3837mulid1i 8841 . . . . . . 7  |-  ( 2  x.  1 )  =  2
3938fveq2i 5530 . . . . . 6  |-  ( I `
 ( 2  x.  1 ) )  =  ( I `  2
)
4038oveq1i 5870 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
41 2p1e3 9849 . . . . . . . 8  |-  ( 2  +  1 )  =  3
4240, 41eqtri 2305 . . . . . . 7  |-  ( ( 2  x.  1 )  +  1 )  =  3
4342fveq2i 5530 . . . . . 6  |-  ( I `
 ( ( 2  x.  1 )  +  1 ) )  =  ( I `  3
)
4439, 43oveq12i 5872 . . . . 5  |-  ( ( I `  ( 2  x.  1 ) )  /  ( I `  ( ( 2  x.  1 )  +  1 ) ) )  =  ( ( I ` 
2 )  /  (
I `  3 )
)
45 2z 10056 . . . . . . . . . . 11  |-  2  e.  ZZ
46 uzid 10244 . . . . . . . . . . 11  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
4745, 46ax-mp 8 . . . . . . . . . 10  |-  2  e.  ( ZZ>= `  2 )
48 wallispilem4.2 . . . . . . . . . . . 12  |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  z ) ^ n
)  _d z )
4948wallispilem2 27826 . . . . . . . . . . 11  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
2  e.  ( ZZ>= ` 
2 )  ->  (
I `  2 )  =  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  (
2  -  2 ) ) ) ) )
5049simp3i 966 . . . . . . . . . 10  |-  ( 2  e.  ( ZZ>= `  2
)  ->  ( I `  2 )  =  ( ( ( 2  -  1 )  / 
2 )  x.  (
I `  ( 2  -  2 ) ) ) )
5147, 50ax-mp 8 . . . . . . . . 9  |-  ( I `
 2 )  =  ( ( ( 2  -  1 )  / 
2 )  x.  (
I `  ( 2  -  2 ) ) )
52 2m1e1 9843 . . . . . . . . . . 11  |-  ( 2  -  1 )  =  1
5352oveq1i 5870 . . . . . . . . . 10  |-  ( ( 2  -  1 )  /  2 )  =  ( 1  /  2
)
54 subid 9069 . . . . . . . . . . . . 13  |-  ( 2  e.  CC  ->  (
2  -  2 )  =  0 )
5537, 54ax-mp 8 . . . . . . . . . . . 12  |-  ( 2  -  2 )  =  0
5655fveq2i 5530 . . . . . . . . . . 11  |-  ( I `
 ( 2  -  2 ) )  =  ( I `  0
)
5749simp1i 964 . . . . . . . . . . 11  |-  ( I `
 0 )  =  pi
5856, 57eqtri 2305 . . . . . . . . . 10  |-  ( I `
 ( 2  -  2 ) )  =  pi
5953, 58oveq12i 5872 . . . . . . . . 9  |-  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  ( 2  -  2 ) ) )  =  ( ( 1  / 
2 )  x.  pi )
6051, 59eqtri 2305 . . . . . . . 8  |-  ( I `
 2 )  =  ( ( 1  / 
2 )  x.  pi )
61 ax-1cn 8797 . . . . . . . . . . 11  |-  1  e.  CC
62 2ne0 9831 . . . . . . . . . . . 12  |-  2  =/=  0
6337, 62pm3.2i 441 . . . . . . . . . . 11  |-  ( 2  e.  CC  /\  2  =/=  0 )
64 pire 19834 . . . . . . . . . . . 12  |-  pi  e.  RR
6564recni 8851 . . . . . . . . . . 11  |-  pi  e.  CC
6661, 63, 653pm3.2i 1130 . . . . . . . . . 10  |-  ( 1  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 )  /\  pi  e.  CC )
67 div32 9446 . . . . . . . . . 10  |-  ( ( 1  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 )  /\  pi  e.  CC )  ->  ( ( 1  /  2 )  x.  pi )  =  ( 1  x.  ( pi 
/  2 ) ) )
6866, 67ax-mp 8 . . . . . . . . 9  |-  ( ( 1  /  2 )  x.  pi )  =  ( 1  x.  (
pi  /  2 ) )
6965, 37, 62divcli 9504 . . . . . . . . . 10  |-  ( pi 
/  2 )  e.  CC
7069mulid2i 8842 . . . . . . . . 9  |-  ( 1  x.  ( pi  / 
2 ) )  =  ( pi  /  2
)
7168, 70eqtri 2305 . . . . . . . 8  |-  ( ( 1  /  2 )  x.  pi )  =  ( pi  /  2
)
7260, 71eqtri 2305 . . . . . . 7  |-  ( I `
 2 )  =  ( pi  /  2
)
73 3nn 9880 . . . . . . . . . . . 12  |-  3  e.  NN
74 nnz 10047 . . . . . . . . . . . 12  |-  ( 3  e.  NN  ->  3  e.  ZZ )
7573, 74ax-mp 8 . . . . . . . . . . 11  |-  3  e.  ZZ
76 2re 9817 . . . . . . . . . . . . 13  |-  2  e.  RR
77 3re 9819 . . . . . . . . . . . . 13  |-  3  e.  RR
7876, 77pm3.2i 441 . . . . . . . . . . . 12  |-  ( 2  e.  RR  /\  3  e.  RR )
79 2lt3 9889 . . . . . . . . . . . 12  |-  2  <  3
80 ltle 8912 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR  /\  3  e.  RR )  ->  ( 2  <  3  ->  2  <_  3 ) )
8178, 79, 80mp2 17 . . . . . . . . . . 11  |-  2  <_  3
8245, 75, 813pm3.2i 1130 . . . . . . . . . 10  |-  ( 2  e.  ZZ  /\  3  e.  ZZ  /\  2  <_ 
3 )
83 eluz2 10238 . . . . . . . . . 10  |-  ( 3  e.  ( ZZ>= `  2
)  <->  ( 2  e.  ZZ  /\  3  e.  ZZ  /\  2  <_ 
3 ) )
8482, 83mpbir 200 . . . . . . . . 9  |-  3  e.  ( ZZ>= `  2 )
8548wallispilem2 27826 . . . . . . . . . 10  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
3  e.  ( ZZ>= ` 
2 )  ->  (
I `  3 )  =  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  (
3  -  2 ) ) ) ) )
8685simp3i 966 . . . . . . . . 9  |-  ( 3  e.  ( ZZ>= `  2
)  ->  ( I `  3 )  =  ( ( ( 3  -  1 )  / 
3 )  x.  (
I `  ( 3  -  2 ) ) ) )
8784, 86ax-mp 8 . . . . . . . 8  |-  ( I `
 3 )  =  ( ( ( 3  -  1 )  / 
3 )  x.  (
I `  ( 3  -  2 ) ) )
88 eqid 2285 . . . . . . . . . . . . . . . 16  |-  3  =  3
8937, 61, 41addcomli 9006 . . . . . . . . . . . . . . . 16  |-  ( 1  +  2 )  =  3
9088, 89eqtr4i 2308 . . . . . . . . . . . . . . 15  |-  3  =  ( 1  +  2 )
9190eqcomi 2289 . . . . . . . . . . . . . 14  |-  ( 1  +  2 )  =  3
92 3cn 9820 . . . . . . . . . . . . . . . 16  |-  3  e.  CC
9392, 61, 373pm3.2i 1130 . . . . . . . . . . . . . . 15  |-  ( 3  e.  CC  /\  1  e.  CC  /\  2  e.  CC )
94 subadd 9056 . . . . . . . . . . . . . . 15  |-  ( ( 3  e.  CC  /\  1  e.  CC  /\  2  e.  CC )  ->  (
( 3  -  1 )  =  2  <->  (
1  +  2 )  =  3 ) )
9593, 94ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( 3  -  1 )  =  2  <->  ( 1  +  2 )  =  3 )
9691, 95mpbir 200 . . . . . . . . . . . . 13  |-  ( 3  -  1 )  =  2
97 eqcom 2287 . . . . . . . . . . . . 13  |-  ( ( 3  -  1 )  =  2  <->  2  =  ( 3  -  1 ) )
9896, 97mpbi 199 . . . . . . . . . . . 12  |-  2  =  ( 3  -  1 )
9998oveq1i 5870 . . . . . . . . . . 11  |-  ( 2  /  3 )  =  ( ( 3  -  1 )  /  3
)
10092, 37, 61, 41subaddrii 9137 . . . . . . . . . . . . . 14  |-  ( 3  -  2 )  =  1
101100fveq2i 5530 . . . . . . . . . . . . 13  |-  ( I `
 ( 3  -  2 ) )  =  ( I `  1
)
10249simp2i 965 . . . . . . . . . . . . 13  |-  ( I `
 1 )  =  2
103101, 102eqtri 2305 . . . . . . . . . . . 12  |-  ( I `
 ( 3  -  2 ) )  =  2
104 eqcom 2287 . . . . . . . . . . . 12  |-  ( ( I `  ( 3  -  2 ) )  =  2  <->  2  =  ( I `  (
3  -  2 ) ) )
105103, 104mpbi 199 . . . . . . . . . . 11  |-  2  =  ( I `  ( 3  -  2 ) )
10699, 105oveq12i 5872 . . . . . . . . . 10  |-  ( ( 2  /  3 )  x.  2 )  =  ( ( ( 3  -  1 )  / 
3 )  x.  (
I `  ( 3  -  2 ) ) )
107106eqcomi 2289 . . . . . . . . 9  |-  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  ( 3  -  2 ) ) )  =  ( ( 2  / 
3 )  x.  2 )
108 3ne0 9833 . . . . . . . . . . 11  |-  3  =/=  0
10937, 92, 108divcli 9504 . . . . . . . . . 10  |-  ( 2  /  3 )  e.  CC
110109, 37mulcomi 8845 . . . . . . . . 9  |-  ( ( 2  /  3 )  x.  2 )  =  ( 2  x.  (
2  /  3 ) )
111107, 110eqtri 2305 . . . . . . . 8  |-  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  ( 3  -  2 ) ) )  =  ( 2  x.  (
2  /  3 ) )
11287, 111eqtri 2305 . . . . . . 7  |-  ( I `
 3 )  =  ( 2  x.  (
2  /  3 ) )
11372, 112oveq12i 5872 . . . . . 6  |-  ( ( I `  2 )  /  ( I ` 
3 ) )  =  ( ( pi  / 
2 )  /  (
2  x.  ( 2  /  3 ) ) )
114 1z 10055 . . . . . . . . . 10  |-  1  e.  ZZ
115 seq1 11061 . . . . . . . . . 10  |-  ( 1  e.  ZZ  ->  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 ) )
116114, 115ax-mp 8 . . . . . . . . 9  |-  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 )
117 1nn 9759 . . . . . . . . . 10  |-  1  e.  NN
118 oveq2 5868 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
11938a1i 10 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
2  x.  1 )  =  2 )
120118, 119eqtrd 2317 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
2  x.  k )  =  2 )
121118oveq1d 5875 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
12238oveq1i 5870 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
123122, 52eqtri 2305 . . . . . . . . . . . . . . . 16  |-  ( ( 2  x.  1 )  -  1 )  =  1
124123a1i 10 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
( 2  x.  1 )  -  1 )  =  1 )
125121, 124eqtrd 2317 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  1 )
126120, 125oveq12d 5878 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( 2  / 
1 ) )
12737div1i 9490 . . . . . . . . . . . . . 14  |-  ( 2  /  1 )  =  2
128127a1i 10 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
2  /  1 )  =  2 )
129126, 128eqtrd 2317 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  2 )
130120oveq1d 5875 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  ( 2  +  1 ) )
13141a1i 10 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
2  +  1 )  =  3 )
132130, 131eqtrd 2317 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  3 )
133120, 132oveq12d 5878 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( 2  / 
3 ) )
134129, 133oveq12d 5878 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) )  =  ( 2  x.  ( 2  /  3
) ) )
135 wallispilem4.1 . . . . . . . . . . 11  |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) )
136 ovex 5885 . . . . . . . . . . 11  |-  ( 2  x.  ( 2  / 
3 ) )  e. 
_V
137134, 135, 136fvmpt 5604 . . . . . . . . . 10  |-  ( 1  e.  NN  ->  ( F `  1 )  =  ( 2  x.  ( 2  /  3
) ) )
138117, 137ax-mp 8 . . . . . . . . 9  |-  ( F `
 1 )  =  ( 2  x.  (
2  /  3 ) )
139116, 138eqtr2i 2306 . . . . . . . 8  |-  ( 2  x.  ( 2  / 
3 ) )  =  (  seq  1 (  x.  ,  F ) `
 1 )
140139oveq2i 5871 . . . . . . 7  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  /  (  seq  1 (  x.  ,  F ) `  1
) )
14137, 109mulcli 8844 . . . . . . . . . . 11  |-  ( 2  x.  ( 2  / 
3 ) )  e.  CC
142138, 141eqeltri 2355 . . . . . . . . . 10  |-  ( F `
 1 )  e.  CC
143116, 142eqeltri 2355 . . . . . . . . 9  |-  (  seq  1 (  x.  ,  F ) `  1
)  e.  CC
14437, 92, 62, 108divne0i 9510 . . . . . . . . . . . . 13  |-  ( 2  /  3 )  =/=  0
145109, 144pm3.2i 441 . . . . . . . . . . . 12  |-  ( ( 2  /  3 )  e.  CC  /\  (
2  /  3 )  =/=  0 )
14663, 145pm3.2i 441 . . . . . . . . . . 11  |-  ( ( 2  e.  CC  /\  2  =/=  0 )  /\  ( ( 2  / 
3 )  e.  CC  /\  ( 2  /  3
)  =/=  0 ) )
147 mulne0 9412 . . . . . . . . . . 11  |-  ( ( ( 2  e.  CC  /\  2  =/=  0 )  /\  ( ( 2  /  3 )  e.  CC  /\  ( 2  /  3 )  =/=  0 ) )  -> 
( 2  x.  (
2  /  3 ) )  =/=  0 )
148146, 147ax-mp 8 . . . . . . . . . 10  |-  ( 2  x.  ( 2  / 
3 ) )  =/=  0
149139, 148eqnetrri 2467 . . . . . . . . 9  |-  (  seq  1 (  x.  ,  F ) `  1
)  =/=  0
15069, 143, 1493pm3.2i 1130 . . . . . . . 8  |-  ( ( pi  /  2 )  e.  CC  /\  (  seq  1 (  x.  ,  F ) `  1
)  e.  CC  /\  (  seq  1 (  x.  ,  F ) ` 
1 )  =/=  0
)
151 divrec 9442 . . . . . . . 8  |-  ( ( ( pi  /  2
)  e.  CC  /\  (  seq  1 (  x.  ,  F ) ` 
1 )  e.  CC  /\  (  seq  1 (  x.  ,  F ) `
 1 )  =/=  0 )  ->  (
( pi  /  2
)  /  (  seq  1 (  x.  ,  F ) `  1
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  1 )
) ) )
152150, 151ax-mp 8 . . . . . . 7  |-  ( ( pi  /  2 )  /  (  seq  1
(  x.  ,  F
) `  1 )
)  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq  1 (  x.  ,  F ) `
 1 ) ) )
153140, 152eqtri 2305 . . . . . 6  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  1
) ) )
154113, 153eqtri 2305 . . . . 5  |-  ( ( I `  2 )  /  ( I ` 
3 ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  1
) ) )
15544, 154eqtri 2305 . . . 4  |-  ( ( I `  ( 2  x.  1 ) )  /  ( I `  ( ( 2  x.  1 )  +  1 ) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  1
) ) )
15645a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  e.  ZZ )
157 nnz 10047 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  y  e.  ZZ )
158157peano2zd 10122 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  ZZ )
159156, 158zmulcld 10125 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  ZZ )
16076a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  e.  RR )
161 nnre 9755 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  y  e.  RR )
162 1re 8839 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
163162a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  1  e.  RR )
164161, 163readdcld 8864 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR )
165 0re 8840 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
166165, 76pm3.2i 441 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  /\  2  e.  RR )
167 2pos 9830 . . . . . . . . . . . . . . . . . 18  |-  0  <  2
168 ltle 8912 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  RR  /\  2  e.  RR )  ->  ( 0  <  2  ->  0  <_  2 ) )
169166, 167, 168mp2 17 . . . . . . . . . . . . . . . . 17  |-  0  <_  2
170169a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  0  <_  2 )
171 nnnn0 9974 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  y  e.  NN0 )
172 nn0ge0 9993 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN0  ->  0  <_ 
y )
173171, 172syl 15 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  0  <_  y )
174163, 161jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
1  e.  RR  /\  y  e.  RR )
)
175 addge02 9287 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  RR  /\  y  e.  RR )  ->  ( 0  <_  y  <->  1  <_  ( y  +  1 ) ) )
176174, 175syl 15 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
0  <_  y  <->  1  <_  ( y  +  1 ) ) )
177173, 176mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  1  <_  ( y  +  1 ) )
178160, 164, 170, 177lemulge11d 9696 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  2  <_  ( 2  x.  (
y  +  1 ) ) )
179159, 178jca 518 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  e.  ZZ  /\  2  <_  ( 2  x.  ( y  +  1 ) ) ) )
180 eluz1 10236 . . . . . . . . . . . . . . 15  |-  ( 2  e.  ZZ  ->  (
( 2  x.  (
y  +  1 ) )  e.  ( ZZ>= ` 
2 )  <->  ( (
2  x.  ( y  +  1 ) )  e.  ZZ  /\  2  <_  ( 2  x.  (
y  +  1 ) ) ) ) )
18145, 180ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  ( y  +  1 ) )  e.  ( ZZ>= `  2
)  <->  ( ( 2  x.  ( y  +  1 ) )  e.  ZZ  /\  2  <_ 
( 2  x.  (
y  +  1 ) ) ) )
182179, 181sylibr 203 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  ( ZZ>= `  2
) )
18348wallispilem2 27826 . . . . . . . . . . . . . 14  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
( 2  x.  (
y  +  1 ) )  e.  ( ZZ>= ` 
2 )  ->  (
I `  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( (
2  x.  ( y  +  1 ) )  -  2 ) ) ) ) )
184183simp3i 966 . . . . . . . . . . . . 13  |-  ( ( 2  x.  ( y  +  1 ) )  e.  ( ZZ>= `  2
)  ->  ( I `  ( 2  x.  (
y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  - 
1 )  /  (
2  x.  ( y  +  1 ) ) )  x.  ( I `
 ( ( 2  x.  ( y  +  1 ) )  - 
2 ) ) ) )
185182, 184syl 15 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( (
2  x.  ( y  +  1 ) )  -  2 ) ) ) )
18637a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  2  e.  CC )
187 nncn 9756 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  y  e.  CC )
18861a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  1  e.  CC )
189186, 187, 1883jca 1132 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
2  e.  CC  /\  y  e.  CC  /\  1  e.  CC ) )
190 adddi 8828 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  CC  /\  y  e.  CC  /\  1  e.  CC )  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  ( 2  x.  1 ) ) )
191189, 190syl 15 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  ( 2  x.  1 ) ) )
192186mulid1d 8854 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
2  x.  1 )  =  2 )
193192oveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
194191, 193eqtrd 2317 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
195194oveq1d 5875 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( ( ( 2  x.  y )  +  2 )  - 
2 ) )
196186, 187mulcld 8857 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  CC )
197196, 186pncand 9160 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  2 )  =  ( 2  x.  y ) )
198195, 197eqtrd 2317 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( 2  x.  y ) )
199198fveq2d 5531 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  -  2 ) )  =  ( I `  ( 2  x.  y
) ) )
200199oveq2d 5876 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  ( y  +  1 ) )  - 
1 )  /  (
2  x.  ( y  +  1 ) ) )  x.  ( I `
 ( ( 2  x.  ( y  +  1 ) )  - 
2 ) ) )  =  ( ( ( ( 2  x.  (
y  +  1 ) )  -  1 )  /  ( 2  x.  ( y  +  1 ) ) )  x.  ( I `  (
2  x.  y ) ) ) )
201185, 200eqtrd 2317 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( 2  x.  y ) ) ) )
202194oveq1d 5875 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( ( 2  x.  y )  +  2 )  +  1 ) )
203196, 186, 188addassd 8859 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  +  1 )  =  ( ( 2  x.  y )  +  ( 2  +  1 ) ) )
204202, 203eqtrd 2317 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( 2  x.  y )  +  ( 2  +  1 ) ) )
20541a1i 10 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  +  1 )  =  3 )
206205oveq2d 5876 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  +  1 ) )  =  ( ( 2  x.  y )  +  3 ) )
207204, 206eqtrd 2317 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( 2  x.  y )  +  3 ) )
208207fveq2d 5531 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  3 ) ) )
209156, 157zmulcld 10125 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  ZZ )
21075a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  3  e.  ZZ )
211209, 210zaddcld 10123 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  ZZ )
212160, 161remulcld 8865 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  RR )
21377a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  3  e.  RR )
214212, 213readdcld 8864 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  RR )
215160, 212, 2143jca 1132 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  e.  RR  /\  ( 2  x.  y
)  e.  RR  /\  ( ( 2  x.  y )  +  3 )  e.  RR ) )
216 nnge1 9774 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  1  <_  y )
217160, 161, 170, 216lemulge11d 9696 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  2  <_  ( 2  x.  y
) )
218165, 77pm3.2i 441 . . . . . . . . . . . . . . . . . . 19  |-  ( 0  e.  RR  /\  3  e.  RR )
21973nngt0i 9781 . . . . . . . . . . . . . . . . . . 19  |-  0  <  3
220 ltle 8912 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  e.  RR  /\  3  e.  RR )  ->  ( 0  <  3  ->  0  <_  3 ) )
221218, 219, 220mp2 17 . . . . . . . . . . . . . . . . . 18  |-  0  <_  3
222212, 213jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  e.  RR  /\  3  e.  RR )
)
223 addge01 9286 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 2  x.  y
)  e.  RR  /\  3  e.  RR )  ->  ( 0  <_  3  <->  ( 2  x.  y )  <_  ( ( 2  x.  y )  +  3 ) ) )
224222, 223syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
0  <_  3  <->  ( 2  x.  y )  <_ 
( ( 2  x.  y )  +  3 ) ) )
225221, 224mpbii 202 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  y )  <_  ( ( 2  x.  y )  +  3 ) )
226217, 225jca 518 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  <_  ( 2  x.  y )  /\  ( 2  x.  y
)  <_  ( (
2  x.  y )  +  3 ) ) )
227 letr 8916 . . . . . . . . . . . . . . . 16  |-  ( ( 2  e.  RR  /\  ( 2  x.  y
)  e.  RR  /\  ( ( 2  x.  y )  +  3 )  e.  RR )  ->  ( ( 2  <_  ( 2  x.  y )  /\  (
2  x.  y )  <_  ( ( 2  x.  y )  +  3 ) )  -> 
2  <_  ( (
2  x.  y )  +  3 ) ) )
228215, 226, 227sylc 56 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  2  <_  ( ( 2  x.  y )  +  3 ) )
229211, 228jca 518 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  e.  ZZ  /\  2  <_  ( ( 2  x.  y )  +  3 ) ) )
230 eluz1 10236 . . . . . . . . . . . . . . 15  |-  ( 2  e.  ZZ  ->  (
( ( 2  x.  y )  +  3 )  e.  ( ZZ>= ` 
2 )  <->  ( (
( 2  x.  y
)  +  3 )  e.  ZZ  /\  2  <_  ( ( 2  x.  y )  +  3 ) ) ) )
23145, 230ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( ( 2  x.  y
)  +  3 )  e.  ( ZZ>= `  2
)  <->  ( ( ( 2  x.  y )  +  3 )  e.  ZZ  /\  2  <_ 
( ( 2  x.  y )  +  3 ) ) )
232229, 231sylibr 203 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  ( ZZ>= `  2
) )
23348wallispilem2 27826 . . . . . . . . . . . . . 14  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
( ( 2  x.  y )  +  3 )  e.  ( ZZ>= ` 
2 )  ->  (
I `  ( (
2  x.  y )  +  3 ) )  =  ( ( ( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  x.  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) ) ) ) )
234233simp3i 966 . . . . . . . . . . . . 13  |-  ( ( ( 2  x.  y
)  +  3 )  e.  ( ZZ>= `  2
)  ->  ( I `  ( ( 2  x.  y )  +  3 ) )  =  ( ( ( ( ( 2  x.  y )  +  3 )  - 
1 )  /  (
( 2  x.  y
)  +  3 ) )  x.  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) ) )
235232, 234syl 15 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  y )  +  3 ) )  =  ( ( ( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  x.  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) ) ) )
236208, 235eqtrd 2317 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( ( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  x.  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) ) ) )
237201, 236oveq12d 5878 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  ( y  +  1 ) ) )  /  ( I `
 ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  =  ( ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  /  ( 2  x.  ( y  +  1 ) ) )  x.  ( I `  ( 2  x.  y
) ) )  / 
( ( ( ( ( 2  x.  y
)  +  3 )  -  1 )  / 
( ( 2  x.  y )  +  3 ) )  x.  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) ) ) ) )
238194oveq1d 5875 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( ( 2  x.  y )  +  2 )  - 
1 ) )
239196, 186, 188addsubassd 9179 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
240238, 239eqtrd 2317 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
24152eqcomi 2289 . . . . . . . . . . . . . . . . 17  |-  1  =  ( 2  -  1 )
242241a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  1  =  ( 2  -  1 ) )
243 eqcom 2287 . . . . . . . . . . . . . . . . 17  |-  ( 1  =  ( 2  -  1 )  <->  ( 2  -  1 )  =  1 )
244243imbi2i 303 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  NN  ->  1  =  ( 2  -  1 ) )  <->  ( y  e.  NN  ->  ( 2  -  1 )  =  1 ) )
245242, 244mpbi 199 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  -  1 )  =  1 )
246245oveq2d 5876 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  y )  +  1 ) )
247240, 246eqtrd 2317 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  1 ) )
248247oveq1d 5875 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 )  /  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) ) )
249248oveq1d 5875 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  ( y  +  1 ) )  - 
1 )  /  (
2  x.  ( y  +  1 ) ) )  x.  ( I `
 ( 2  x.  y ) ) )  =  ( ( ( ( 2  x.  y
)  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  x.  ( I `  (
2  x.  y ) ) ) )
25092a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  3  e.  CC )
251196, 250, 188addsubassd 9179 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( ( 2  x.  y )  +  ( 3  -  1 ) ) )
25296a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
3  -  1 )  =  2 )
253252oveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 3  -  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
254251, 253eqtrd 2317 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( ( 2  x.  y )  +  2 ) )
255194eqcomd 2290 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  2 )  =  ( 2  x.  ( y  +  1 ) ) )
256254, 255eqtrd 2317 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( 2  x.  ( y  +  1 ) ) )
257256oveq1d 5875 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
258257oveq1d 5875 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( ( ( 2  x.  y )  +  3 )  - 
1 )  /  (
( 2  x.  y
)  +  3 ) )  x.  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  x.  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) ) ) )
259249, 258oveq12d 5878 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( 2  x.  y ) ) )  /  ( ( ( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  x.  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) ) ) )  =  ( ( ( ( ( 2  x.  y
)  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  x.  ( I `  (
2  x.  y ) ) )  /  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  3 ) )  x.  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) ) ) )
260237, 259eqtrd 2317 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  ( y  +  1 ) ) )  /  ( I `
 ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  x.  ( I `  ( 2  x.  y
) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) )  x.  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) ) ) ) )
261196, 188addcld 8856 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  CC )
262187, 188addcld 8856 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  CC )
263186, 262mulcld 8857 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  CC )
26462a1i 10 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  =/=  0 )
265 peano2nn 9760 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
266 nnne0 9780 . . . . . . . . . . . . . 14  |-  ( ( y  +  1 )  e.  NN  ->  (
y  +  1 )  =/=  0 )
267265, 266syl 15 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
y  +  1 )  =/=  0 )
268186, 262, 264, 267mulne0d 9422 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
269261, 263, 268divcld 9538 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
270 2nn0 9984 . . . . . . . . . . . . . 14  |-  2  e.  NN0
271270a1i 10 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  e.  NN0 )
272271, 171nn0mulcld 10025 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  NN0 )
273 ax-resscn 8796 . . . . . . . . . . . . 13  |-  RR  C_  CC
27448wallispilem3 27827 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  y )  e.  NN0  ->  ( I `
 ( 2  x.  y ) )  e.  RR+ )
275 rpre 10362 . . . . . . . . . . . . . 14  |-  ( ( I `  ( 2  x.  y ) )  e.  RR+  ->  ( I `
 ( 2  x.  y ) )  e.  RR )
276274, 275syl 15 . . . . . . . . . . . . 13  |-  ( ( 2  x.  y )  e.  NN0  ->  ( I `
 ( 2  x.  y ) )  e.  RR )
277273, 276sseldi 3180 . . . . . . . . . . . 12  |-  ( ( 2  x.  y )  e.  NN0  ->  ( I `
 ( 2  x.  y ) )  e.  CC )
278272, 277syl 15 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  y ) )  e.  CC )
279196, 250addcld 8856 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  CC )
280165a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  0  e.  RR )
281280, 212, 2143jca 1132 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
0  e.  RR  /\  ( 2  x.  y
)  e.  RR  /\  ( ( 2  x.  y )  +  3 )  e.  RR ) )
282167a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  0  <  2 )
283 nngt0 9777 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  0  <  y )
284160, 161, 282, 283mulgt0d 8973 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  0  <  ( 2  x.  y
) )
285213, 219jctir 524 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
3  e.  RR  /\  0  <  3 ) )
286 elrp 10358 . . . . . . . . . . . . . . . . . 18  |-  ( 3  e.  RR+  <->  ( 3  e.  RR  /\  0  <  3 ) )
287285, 286sylibr 203 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  3  e.  RR+ )
288212, 287ltaddrpd 10421 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  y )  <  ( ( 2  x.  y )  +  3 ) )
289284, 288jca 518 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
0  <  ( 2  x.  y )  /\  ( 2  x.  y
)  <  ( (
2  x.  y )  +  3 ) ) )
290 lttr 8901 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  ( 2  x.  y
)  e.  RR  /\  ( ( 2  x.  y )  +  3 )  e.  RR )  ->  ( ( 0  <  ( 2  x.  y )  /\  (
2  x.  y )  <  ( ( 2  x.  y )  +  3 ) )  -> 
0  <  ( (
2  x.  y )  +  3 ) ) )
291281, 289, 290sylc 56 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <  ( ( 2  x.  y )  +  3 ) )
292291gt0ne0d 9339 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  =/=  0 )
293263, 279, 292divcld 9538 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  CC )
294263, 279, 268, 292divne0d 9554 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  =/=  0 )
295211, 156zsubcld 10124 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  e.  ZZ )
296214, 160jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  e.  RR  /\  2  e.  RR )
)
297 subge0 9289 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 2  x.  y )  +  3 )  e.  RR  /\  2  e.  RR )  ->  ( 0  <_  (
( ( 2  x.  y )  +  3 )  -  2 )  <->  2  <_  ( (
2  x.  y )  +  3 ) ) )
298296, 297syl 15 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
0  <_  ( (
( 2  x.  y
)  +  3 )  -  2 )  <->  2  <_  ( ( 2  x.  y
)  +  3 ) ) )
299228, 298mpbird 223 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  0  <_  ( ( ( 2  x.  y )  +  3 )  -  2 ) )
300295, 299jca 518 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  3 )  -  2 )  e.  ZZ  /\  0  <_  ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) )
301 elnn0z 10038 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0  <->  ( ( ( ( 2  x.  y
)  +  3 )  -  2 )  e.  ZZ  /\  0  <_ 
( ( ( 2  x.  y )  +  3 )  -  2 ) ) )
302300, 301sylibr 203 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0 )
30348wallispilem3 27827 . . . . . . . . . . . . . 14  |-  ( ( ( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0  ->  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) )  e.  RR+ )
304302, 303syl 15 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) )  e.  RR+ )
305304rpcnne0d 10401 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) )  e.  CC  /\  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) )  =/=  0 ) )
306293, 294, 305jca31 520 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) )  e.  CC  /\  ( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  3 ) )  =/=  0 )  /\  ( ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) )  e.  CC  /\  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) )  =/=  0 ) ) )
307269, 278, 306jca31 520 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  e.  CC  /\  ( I `  (
2  x.  y ) )  e.  CC )  /\  ( ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  CC  /\  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  =/=  0 )  /\  ( ( I `  ( ( ( 2  x.  y )  +  3 )  -  2 ) )  e.  CC  /\  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) )  =/=  0 ) ) ) )
308 divmuldiv 9462 . . . . . . . . . 10  |-  ( ( ( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  e.  CC  /\  ( I `  (
2  x.  y ) )  e.  CC )  /\  ( ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  CC  /\  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  =/=  0 )  /\  ( ( I `  ( ( ( 2  x.  y )  +  3 )  -  2 ) )  e.  CC  /\  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) )  =/=  0 ) ) )  ->  (
( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  x.  ( ( I `  ( 2  x.  y ) )  /  ( I `  ( ( ( 2  x.  y )  +  3 )  -  2 ) ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  x.  ( I `  ( 2  x.  y
) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) )  x.  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) ) ) ) )
309307, 308syl 15 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  x.  ( ( I `  ( 2  x.  y ) )  /  ( I `  ( ( ( 2  x.  y )  +  3 )  -  2 ) ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  x.  ( I `  ( 2  x.  y
) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) )  x.  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) ) ) ) )
310260, 309eqtr4d 2320 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  ( y  +  1 ) ) )  /  ( I `
 ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  x.  ( ( I `  ( 2  x.  y
) )  /  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) ) ) ) )
311196, 250, 186addsubassd 9179 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  ( 3  -  2 ) ) )
312100a1i 10 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
3  -  2 )  =  1 )
313312oveq2d 5876 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 3  -  2 ) )  =  ( ( 2  x.  y )  +  1 ) )
314311, 313eqtrd 2317 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  1 ) )
315314fveq2d 5531 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
316315oveq2d 5876 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  y ) )  /  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
317316oveq2d 5876 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  x.  ( ( I `  ( 2  x.  y ) )  /  ( I `  ( ( ( 2  x.  y )  +  3 )  -  2 ) ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  x.  ( ( I `  ( 2  x.  y
) )  /  (
I `  ( (
2  x.  y )  +  1 ) ) ) ) )
318310, 317eqtrd 2317 . . . . . . 7  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  ( y  +  1 ) ) )  /  ( I `
 ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  x.  ( ( I `  ( 2  x.  y
) )  /  (
I `  ( (
2  x.  y )  +  1 ) ) ) ) )
319318adantr 451 . . . . . 6  |-  ( ( y  e.  NN  /\  ( ( I `  ( 2  x.  y
) )  /  (
I `  ( (
2  x.  y )  +  1 ) ) )  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq  1 (  x.  ,  F ) `
 y ) ) ) )  ->  (
( I `  (
2  x.  ( y  +  1 ) ) )  /  ( I `
 ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  x.  ( ( I `  ( 2  x.  y
) )  /  (
I `  ( (
2  x.  y )  +  1 ) ) ) ) )
320 oveq2 5868 . . . . . . . 8  |-  ( ( ( I `  (
2  x.  y ) )  /  ( I `
 ( ( 2  x.  y )  +  1 ) ) )  =  ( ( pi 
/  2 )  x.  ( 1  /  (  seq  1 (  x.  ,  F ) `  y
) ) )  -> 
( ( ( ( ( 2  x.  y
)  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  / 
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  3 ) ) )  x.  (
( I `  (
2  x.  y ) )  /  ( I `
 ( ( 2  x.  y )  +  1 ) ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  (
2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  x.  ( ( pi 
/  2 )  x.  ( 1  /  (  seq  1 (  x.  ,  F ) `  y
) ) ) ) )
321320adantl 452 . . . . . . 7  |-  ( ( y  e.  NN  /\  ( ( I `  ( 2  x.  y
) )  /  (
I `  ( (
2  x.  y )  +  1 ) ) )  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq  1 (  x.  ,  F ) `
 y ) ) ) )  ->  (
( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  x.  ( ( I `  ( 2  x.  y ) )  /  ( I `  ( ( 2  x.  y )  +  1 ) ) ) )  =  ( ( ( ( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  x.  ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  y
) ) ) ) )
322 elnnuz 10266 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  <->  y  e.  ( ZZ>= `  1 )
)
323322biimpi 186 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  ( ZZ>= `  1 )
)
324 seqp1 11063 . . . . . . . . . . . . . 14  |-  ( y  e.  ( ZZ>= `  1
)  ->  (  seq  1 (  x.  ,  F ) `  (
y  +  1 ) )  =  ( (  seq  1 (  x.  ,  F ) `  y )  x.  ( F `  ( y  +  1 ) ) ) )
325323, 324syl 15 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (  seq  1 (  x.  ,  F ) `  (
y  +  1 ) )  =  ( (  seq  1 (  x.  ,  F ) `  y )  x.  ( F `  ( y  +  1 ) ) ) )
326135a1i 10 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) )
327 oveq2 5868 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( y  +  1 )  ->  (
2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
328327oveq1d 5875 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
329327, 328oveq12d 5878 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
330327oveq1d 5875 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
331327, 330oveq12d 5878 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
332329, 331oveq12d 5878 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) ) )
333332adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) )
334160, 164remulcld 8865 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR )
335334, 163resubcld 9213 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR )
336 1lt2 9888 . . . . . . . . . . . . . . . . . . . . 21  |-  1  <  2
337336a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  1  <  2 )
338 nnrp 10365 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  NN  ->  y  e.  RR+ )
339163, 338ltaddrp2d 10422 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  1  <  ( y  +  1 ) )
340160, 164, 337, 339mulgt1d 9695 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  1  <  ( 2  x.  (
y  +  1 ) ) )
341162a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  NN  /\  1  <  ( 2  x.  ( y  +  1 ) ) )  -> 
1  e.  RR )
342 simpr 447 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  NN  /\  1  <  ( 2  x.  ( y  +  1 ) ) )  -> 
1  <  ( 2  x.  ( y  +  1 ) ) )
343341, 342ltned 8957 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN  /\  1  <  ( 2  x.  ( y  +  1 ) ) )  -> 
1  =/=  ( 2  x.  ( y  +  1 ) ) )
344343necomd 2531 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  NN  /\  1  <  ( 2  x.  ( y  +  1 ) ) )  -> 
( 2  x.  (
y  +  1 ) )  =/=  1 )
345344ex 423 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
1  <  ( 2  x.  ( y  +  1 ) )  -> 
( 2  x.  (
y  +  1 ) )  =/=  1 ) )
346340, 345mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  1 )
347263, 188, 346subne0d 9168 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =/=  0 )
348334, 335, 347redivcld 9590 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  RR )
349207, 214eqeltrd 2359 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  RR )
350207, 292eqnetrd 2466 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =/=  0 )
351334, 349, 350redivcld 9590 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  RR )
352348, 351remulcld 8865 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  e.  RR )
353326, 333, 265, 352fvmptd 5608 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  ( F `  ( y  +  1 ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) ) )
354353oveq2d 5876 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
(  seq  1 (  x.  ,  F ) `
 y )  x.  ( F `  (
y  +  1 ) ) )  =  ( (  seq  1 (  x.  ,  F ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) ) )
355325, 354eqtrd 2317 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (  seq  1 (  x.  ,  F ) `  (
y  +  1 ) )  =  ( (  seq  1 (  x.  ,  F ) `  y )  x.  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) ) )
356355oveq2d 5876 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  (
y  +  1 ) ) )  =  ( 1  /  ( (  seq  1 (  x.  ,  F ) `  y )  x.  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) ) ) )
357356oveq2d 5876 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  ( y  +  1 ) ) ) )  =  ( ( pi  /  2
)  x.  ( 1  /  ( (  seq  1 (  x.  ,  F ) `  y
)  x.  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) ) ) ) )
358247oveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) ) )
359207oveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
360358, 359oveq12d 5878 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  3 ) ) ) )
361360oveq2d 5876 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
(  seq  1 (  x.  ,  F ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) )  =  ( (  seq  1 (  x.  ,  F ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) )
362361oveq2d 5876 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
1  /  ( (  seq  1 (  x.  ,  F ) `  y )  x.  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) ) )  =  ( 1  /  ( (  seq  1 (  x.  ,  F ) `  y )  x.  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) ) )
363362oveq2d 5876 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  ( (  seq  1 (  x.  ,  F ) `  y
)  x.  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) ) ) )  =  ( ( pi  /  2
)  x.  ( 1  /  ( (  seq  1 (  x.  ,  F ) `  y
)  x.  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) ) ) ) ) )
364 elfznn 10821 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  ( 1 ... y )  ->  w  e.  NN )
365364adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN  /\  w  e.  ( 1 ... y ) )  ->  w  e.  NN )
366135a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) )
367 oveq2 5868 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  w  ->  (
2  x.  k )  =  ( 2  x.  w ) )
368367oveq1d 5875 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  w  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  w )  - 
1 ) )
369367, 368oveq12d 5878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  -  1 ) ) )
370367oveq1d 5875 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  w  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  w )  +  1 ) )
371367, 370oveq12d 5878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  +  1 ) ) )
372369, 371oveq12d 5878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  w  ->  (
( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) )  =  ( ( ( 2  x.  w )  /  ( ( 2  x.  w )  - 
1 ) )  x.  ( ( 2  x.  w )  /  (
( 2  x.  w
)  +  1 ) ) ) )
373372adantl 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w  e.  NN  /\  k  =  w )  ->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) )  =  ( ( ( 2  x.  w
)  /  ( ( 2  x.  w )  -  1 ) )  x.  ( ( 2  x.  w )  / 
( ( 2  x.  w )  +  1 ) ) ) )
374 id 19 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  w  e.  NN )
375 2rp 10361 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  e.  RR+
376375a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  2  e.  RR+ )
377 nnrp 10365 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  w  e.  RR+ )
378376, 377rpmulcld 10408 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  (
2  x.  w )  e.  RR+ )
37976a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  NN  ->  2  e.  RR )
380 nnre 9755 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  NN  ->  w  e.  RR )
381379, 380remulcld 8865 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  NN  ->  (
2  x.  w )  e.  RR )
382162a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  NN  ->  1  e.  RR )
383381, 382resubcld 9213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  -  1 )  e.  RR )
384382, 380, 3813jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  NN  ->  (
1  e.  RR  /\  w  e.  RR  /\  (
2  x.  w )  e.  RR ) )
385 nnge1 9774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  NN  ->  1  <_  w )
386273, 380sseldi 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  NN  ->  w  e.  CC )
387 mulid2 8838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  CC  ->  (
1  x.  w )  =  w )
388386, 387syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  NN  ->  (
1  x.  w )  =  w )
389382, 379, 377ltmul1d 10429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  NN  ->  (
1  <  2  <->  ( 1  x.  w )  < 
( 2  x.  w
) ) )
390336, 389mpbii 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  NN  ->  (
1  x.  w )  <  ( 2  x.  w ) )
391388, 390eqbrtrrd 4047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  NN  ->  w  <  ( 2  x.  w
) )
392385, 391jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  NN  ->  (
1  <_  w  /\  w  <  ( 2  x.  w ) ) )
393 lelttr 8914 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 1  e.  RR  /\  w  e.  RR  /\  (
2  x.  w )  e.  RR )  -> 
( ( 1  <_  w  /\  w  <  (
2  x.  w ) )  ->  1  <  ( 2  x.  w ) ) )
394384, 392, 393sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  NN  ->  1  <  ( 2  x.  w
) )
395382, 381posdifd 9361 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  NN  ->  (
1  <  ( 2  x.  w )  <->  0  <  ( ( 2  x.  w
)  -  1 ) ) )
396394, 395mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  0  <  ( ( 2  x.  w )  -  1 ) )
397383, 396jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  (
( ( 2  x.  w )  -  1 )  e.  RR  /\  0  <  ( ( 2  x.  w )  - 
1 ) ) )
398 elrp 10358 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 2  x.  w
)  -  1 )  e.  RR+  <->  ( ( ( 2  x.  w )  -  1 )  e.  RR  /\  0  < 
( ( 2  x.  w )  -  1 ) ) )
399397, 398sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  -  1 )  e.  RR+ )
400378, 399rpdivcld 10409 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  /  ( ( 2  x.  w )  -  1 ) )  e.  RR+ )
401169a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  0  <_  2 )
402377rpge0d 10396 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  0  <_  w )
403379, 380, 401, 402mulge0d 9351 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  0  <_  ( 2  x.  w
) )
404381, 403ge0p1rpd 10418 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  +  1 )  e.  RR+ )
405378, 404rpdivcld 10409 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  /  ( ( 2  x.  w )  +  1 ) )  e.  RR+ )
406400, 405rpmulcld 10408 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  (
( ( 2  x.  w )  /  (
( 2  x.  w
)  -  1 ) )  x.  ( ( 2  x.  w )  /  ( ( 2  x.  w )  +  1 ) ) )  e.  RR+ )
407366, 373, 374, 406fvmptd 5608 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  NN  ->  ( F `  w )  =  ( ( ( 2  x.  w )  /  ( ( 2  x.  w )  - 
1 ) )  x.  ( ( 2  x.  w )  /  (
( 2  x.  w
)  +  1 ) ) ) )
408407, 406eqeltrd 2359 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  NN  ->  ( F `  w )  e.  RR+ )
409365, 408syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  NN  /\  w  e.  ( 1 ... y ) )  ->  ( F `  w )  e.  RR+ )
410 rpmulcl 10377 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  e.  RR+  /\  z  e.  RR+ )  ->  (
w  x.  z )  e.  RR+ )
411410adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  NN  /\  ( w  e.  RR+  /\  z  e.  RR+ ) )  -> 
( w  x.  z
)  e.  RR+ )
412323, 409, 411seqcl 11068 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (  seq  1 (  x.  ,  F ) `  y
)  e.  RR+ )
413412rpcnne0d 10401 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
(  seq  1 (  x.  ,  F ) `
 y )  e.  CC  /\  (  seq  1 (  x.  ,  F ) `  y
)  =/=  0 ) )
414375a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  2  e.  RR+ )
415161, 173ge0p1rpd 10418 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR+ )
416414, 415rpmulcld 10408 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR+ )
417160, 161, 170, 173mulge0d 9351 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  0  <_  ( 2  x.  y
) )
418212, 417ge0p1rpd 10418 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  RR+ )
419416, 418rpdivcld 10409 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  e.  RR+ )
420414, 338rpmulcld 10408 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  RR+ )
421420, 287rpaddcld 10407 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  RR+ )
422416, 421rpdivcld 10409 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  RR+ )
423419, 422rpmulcld 10408 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  RR+ )
424423rpcnne0d 10401 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  CC  /\  ( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  =/=  0 ) )
425188, 413, 4243jca 1132 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
1  e.  CC  /\  ( (  seq  1
(  x.  ,  F
) `  y )  e.  CC  /\  (  seq  1 (  x.  ,  F ) `  y
)  =/=  0 )  /\  ( ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  e.  CC  /\  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  =/=  0 ) ) )
426 divdiv1 9473 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  ( (  seq  1
(  x.  ,  F
) `  y )  e.  CC  /\  (  seq  1 (  x.  ,  F ) `  y
)  =/=  0 )  /\  ( ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  e.  CC  /\  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )  =/=  0 ) )  -> 
( ( 1  / 
(  seq  1 (  x.  ,  F ) `
 y ) )  /  ( ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  3 ) ) ) )  =  ( 1  /  (
(  seq  1 (  x.  ,  F ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) ) )
427425, 426syl 15 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 1  /  (  seq  1 (  x.  ,  F ) `  y
) )  /  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) )  =  ( 1  /  ( (  seq  1 (  x.  ,  F ) `  y
)  x.  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) ) ) ) )
428427eqcomd 2290 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
1  /  ( (  seq  1 (  x.  ,  F ) `  y )  x.  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) )  =  ( ( 1  /  (  seq  1 (  x.  ,  F ) `  y
) )  /  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) )
429428oveq2d 5876 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  ( (  seq  1 (  x.  ,  F ) `  y
)  x.  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) ) ) ) )  =  ( ( pi  /  2
)  x.  ( ( 1  /  (  seq  1 (  x.  ,  F ) `  y
) )  /  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) ) )
43069a1i 10 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
pi  /  2 )  e.  CC )
431413simpld 445 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (  seq  1 (  x.  ,  F ) `  y
)  e.  CC )
432413simprd 449 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (  seq  1 (  x.  ,  F ) `  y
)  =/=  0 )
433431, 432reccld 9531 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  y
) )  e.  CC )
434424simpld 445 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  CC )
435424simprd 449 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  =/=  0 )
436430, 433, 434, 435divassd 9573 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  y
) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) )  =  ( ( pi  /  2
)  x.  ( ( 1  /  (  seq  1 (  x.  ,  F ) `  y
) )  /  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) ) )
437436eqcomd 2290 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( ( 1  /  (  seq  1 (  x.  ,  F ) `  y
) )  /  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) )  =  ( ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  y
) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) )
438247, 347eqnetrrd 2468 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =/=  0 )
439263, 261, 263, 279, 438, 292divmuldivd 9579 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  / 
( ( ( 2  x.  y )  +  1 )  x.  (
( 2  x.  y
)  +  3 ) ) ) )
440439oveq2d 5876 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  y
) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) )  =  ( ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  y
) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  (
y  +  1 ) ) )  /  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  3 ) ) ) ) )
441430, 433mulcld 8857 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  y )
) )  e.  CC )
442263, 263mulcld 8857 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
443261, 279mulcld 8857 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  3 ) )  e.  CC )
444263, 263, 268, 268mulne0d 9422 . . . . . . . . . . . . . . 15  |-  ( y