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

Theorem wallispilem4 27323
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 5989 . . . . . . 7  |-  ( x  =  1  ->  (
2  x.  x )  =  ( 2  x.  1 ) )
21fveq2d 5636 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  1 ) ) )
31oveq1d 5996 . . . . . . 7  |-  ( x  =  1  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
43fveq2d 5636 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  1 )  +  1 ) ) )
52, 4oveq12d 5999 . . . . 5  |-  ( x  =  1  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  1 ) )  / 
( I `  (
( 2  x.  1 )  +  1 ) ) ) )
6 fveq2 5632 . . . . . . 7  |-  ( x  =  1  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  1
) )
76oveq2d 5997 . . . . . 6  |-  ( x  =  1  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq  1 (  x.  ,  F ) `  1
) ) )
87oveq2d 5997 . . . . 5  |-  ( x  =  1  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  1 )
) ) )
95, 8eqeq12d 2380 . . . 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 5989 . . . . . . 7  |-  ( x  =  y  ->  (
2  x.  x )  =  ( 2  x.  y ) )
1110fveq2d 5636 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  y ) ) )
1210oveq1d 5996 . . . . . . 7  |-  ( x  =  y  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  y )  +  1 ) )
1312fveq2d 5636 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
1411, 13oveq12d 5999 . . . . 5  |-  ( x  =  y  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
15 fveq2 5632 . . . . . . 7  |-  ( x  =  y  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  y
) )
1615oveq2d 5997 . . . . . 6  |-  ( x  =  y  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq  1 (  x.  ,  F ) `  y
) ) )
1716oveq2d 5997 . . . . 5  |-  ( x  =  y  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  y )
) ) )
1814, 17eqeq12d 2380 . . . 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 5989 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
2  x.  x )  =  ( 2  x.  ( y  +  1 ) ) )
2019fveq2d 5636 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  ( y  +  1 ) ) ) )
2119oveq1d 5996 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
2221fveq2d 5636 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
2320, 22oveq12d 5999 . . . . 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 5632 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  (
y  +  1 ) ) )
2524oveq2d 5997 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq  1 (  x.  ,  F ) `  (
y  +  1 ) ) ) )
2625oveq2d 5997 . . . . 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 2380 . . . 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 5989 . . . . . . 7  |-  ( x  =  n  ->  (
2  x.  x )  =  ( 2  x.  n ) )
2928fveq2d 5636 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  n ) ) )
3028oveq1d 5996 . . . . . . 7  |-  ( x  =  n  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  n )  +  1 ) )
3130fveq2d 5636 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  n )  +  1 ) ) )
3229, 31oveq12d 5999 . . . . 5  |-  ( x  =  n  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  n ) )  / 
( I `  (
( 2  x.  n
)  +  1 ) ) ) )
33 fveq2 5632 . . . . . . 7  |-  ( x  =  n  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  n
) )
3433oveq2d 5997 . . . . . 6  |-  ( x  =  n  ->  (
1  /  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq  1 (  x.  ,  F ) `  n
) ) )
3534oveq2d 5997 . . . . 5  |-  ( x  =  n  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  n )
) ) )
3632, 35eqeq12d 2380 . . . 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 9963 . . . . . . . 8  |-  2  e.  CC
3837mulid1i 8986 . . . . . . 7  |-  ( 2  x.  1 )  =  2
3938fveq2i 5635 . . . . . 6  |-  ( I `
 ( 2  x.  1 ) )  =  ( I `  2
)
4038oveq1i 5991 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
41 2p1e3 9996 . . . . . . . 8  |-  ( 2  +  1 )  =  3
4240, 41eqtri 2386 . . . . . . 7  |-  ( ( 2  x.  1 )  +  1 )  =  3
4342fveq2i 5635 . . . . . 6  |-  ( I `
 ( ( 2  x.  1 )  +  1 ) )  =  ( I `  3
)
4439, 43oveq12i 5993 . . . . 5  |-  ( ( I `  ( 2  x.  1 ) )  /  ( I `  ( ( 2  x.  1 )  +  1 ) ) )  =  ( ( I ` 
2 )  /  (
I `  3 )
)
45 2z 10205 . . . . . . . . . . 11  |-  2  e.  ZZ
46 uzid 10393 . . . . . . . . . . 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 27321 . . . . . . . . . . 11  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
2  e.  ( ZZ>= ` 
2 )  ->  (
I `  2 )  =  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  (
2  -  2 ) ) ) ) )
5049simp3i 967 . . . . . . . . . 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 9988 . . . . . . . . . . 11  |-  ( 2  -  1 )  =  1
5352oveq1i 5991 . . . . . . . . . 10  |-  ( ( 2  -  1 )  /  2 )  =  ( 1  /  2
)
54 subid 9214 . . . . . . . . . . . . 13  |-  ( 2  e.  CC  ->  (
2  -  2 )  =  0 )
5537, 54ax-mp 8 . . . . . . . . . . . 12  |-  ( 2  -  2 )  =  0
5655fveq2i 5635 . . . . . . . . . . 11  |-  ( I `
 ( 2  -  2 ) )  =  ( I `  0
)
5749simp1i 965 . . . . . . . . . . 11  |-  ( I `
 0 )  =  pi
5856, 57eqtri 2386 . . . . . . . . . 10  |-  ( I `
 ( 2  -  2 ) )  =  pi
5953, 58oveq12i 5993 . . . . . . . . 9  |-  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  ( 2  -  2 ) ) )  =  ( ( 1  / 
2 )  x.  pi )
6051, 59eqtri 2386 . . . . . . . 8  |-  ( I `
 2 )  =  ( ( 1  / 
2 )  x.  pi )
61 ax-1cn 8942 . . . . . . . . . . 11  |-  1  e.  CC
62 2ne0 9976 . . . . . . . . . . . 12  |-  2  =/=  0
6337, 62pm3.2i 441 . . . . . . . . . . 11  |-  ( 2  e.  CC  /\  2  =/=  0 )
64 pire 20050 . . . . . . . . . . . 12  |-  pi  e.  RR
6564recni 8996 . . . . . . . . . . 11  |-  pi  e.  CC
6661, 63, 653pm3.2i 1131 . . . . . . . . . 10  |-  ( 1  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 )  /\  pi  e.  CC )
67 div32 9591 . . . . . . . . . 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 9649 . . . . . . . . . 10  |-  ( pi 
/  2 )  e.  CC
7069mulid2i 8987 . . . . . . . . 9  |-  ( 1  x.  ( pi  / 
2 ) )  =  ( pi  /  2
)
7168, 70eqtri 2386 . . . . . . . 8  |-  ( ( 1  /  2 )  x.  pi )  =  ( pi  /  2
)
7260, 71eqtri 2386 . . . . . . 7  |-  ( I `
 2 )  =  ( pi  /  2
)
73 3nn 10027 . . . . . . . . . . . 12  |-  3  e.  NN
74 nnz 10196 . . . . . . . . . . . 12  |-  ( 3  e.  NN  ->  3  e.  ZZ )
7573, 74ax-mp 8 . . . . . . . . . . 11  |-  3  e.  ZZ
76 2re 9962 . . . . . . . . . . . . 13  |-  2  e.  RR
77 3re 9964 . . . . . . . . . . . . 13  |-  3  e.  RR
7876, 77pm3.2i 441 . . . . . . . . . . . 12  |-  ( 2  e.  RR  /\  3  e.  RR )
79 2lt3 10036 . . . . . . . . . . . 12  |-  2  <  3
80 ltle 9057 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR  /\  3  e.  RR )  ->  ( 2  <  3  ->  2  <_  3 ) )
8178, 79, 80mp2 17 . . . . . . . . . . 11  |-  2  <_  3
8245, 75, 813pm3.2i 1131 . . . . . . . . . 10  |-  ( 2  e.  ZZ  /\  3  e.  ZZ  /\  2  <_ 
3 )
83 eluz2 10387 . . . . . . . . . 10  |-  ( 3  e.  ( ZZ>= `  2
)  <->  ( 2  e.  ZZ  /\  3  e.  ZZ  /\  2  <_ 
3 ) )
8482, 83mpbir 200 . . . . . . . . 9  |-  3  e.  ( ZZ>= `  2 )
8548wallispilem2 27321 . . . . . . . . . 10  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
3  e.  ( ZZ>= ` 
2 )  ->  (
I `  3 )  =  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  (
3  -  2 ) ) ) ) )
8685simp3i 967 . . . . . . . . 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 2366 . . . . . . . . . . . . . . . 16  |-  3  =  3
8937, 61, 41addcomli 9151 . . . . . . . . . . . . . . . 16  |-  ( 1  +  2 )  =  3
9088, 89eqtr4i 2389 . . . . . . . . . . . . . . 15  |-  3  =  ( 1  +  2 )
9190eqcomi 2370 . . . . . . . . . . . . . 14  |-  ( 1  +  2 )  =  3
92 3cn 9965 . . . . . . . . . . . . . . . 16  |-  3  e.  CC
9392, 61, 373pm3.2i 1131 . . . . . . . . . . . . . . 15  |-  ( 3  e.  CC  /\  1  e.  CC  /\  2  e.  CC )
94 subadd 9201 . . . . . . . . . . . . . . 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 2368 . . . . . . . . . . . . 13  |-  ( ( 3  -  1 )  =  2  <->  2  =  ( 3  -  1 ) )
9896, 97mpbi 199 . . . . . . . . . . . 12  |-  2  =  ( 3  -  1 )
9998oveq1i 5991 . . . . . . . . . . 11  |-  ( 2  /  3 )  =  ( ( 3  -  1 )  /  3
)
10092, 37, 61, 41subaddrii 9282 . . . . . . . . . . . . . 14  |-  ( 3  -  2 )  =  1
101100fveq2i 5635 . . . . . . . . . . . . 13  |-  ( I `
 ( 3  -  2 ) )  =  ( I `  1
)
10249simp2i 966 . . . . . . . . . . . . 13  |-  ( I `
 1 )  =  2
103101, 102eqtri 2386 . . . . . . . . . . . 12  |-  ( I `
 ( 3  -  2 ) )  =  2
104 eqcom 2368 . . . . . . . . . . . 12  |-  ( ( I `  ( 3  -  2 ) )  =  2  <->  2  =  ( I `  (
3  -  2 ) ) )
105103, 104mpbi 199 . . . . . . . . . . 11  |-  2  =  ( I `  ( 3  -  2 ) )
10699, 105oveq12i 5993 . . . . . . . . . 10  |-  ( ( 2  /  3 )  x.  2 )  =  ( ( ( 3  -  1 )  / 
3 )  x.  (
I `  ( 3  -  2 ) ) )
107106eqcomi 2370 . . . . . . . . 9  |-  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  ( 3  -  2 ) ) )  =  ( ( 2  / 
3 )  x.  2 )
108 3ne0 9978 . . . . . . . . . . 11  |-  3  =/=  0
10937, 92, 108divcli 9649 . . . . . . . . . 10  |-  ( 2  /  3 )  e.  CC
110109, 37mulcomi 8990 . . . . . . . . 9  |-  ( ( 2  /  3 )  x.  2 )  =  ( 2  x.  (
2  /  3 ) )
111107, 110eqtri 2386 . . . . . . . 8  |-  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  ( 3  -  2 ) ) )  =  ( 2  x.  (
2  /  3 ) )
11287, 111eqtri 2386 . . . . . . 7  |-  ( I `
 3 )  =  ( 2  x.  (
2  /  3 ) )
11372, 112oveq12i 5993 . . . . . 6  |-  ( ( I `  2 )  /  ( I ` 
3 ) )  =  ( ( pi  / 
2 )  /  (
2  x.  ( 2  /  3 ) ) )
114 1z 10204 . . . . . . . . . 10  |-  1  e.  ZZ
115 seq1 11223 . . . . . . . . . 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 9904 . . . . . . . . . 10  |-  1  e.  NN
118 oveq2 5989 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
11938a1i 10 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
2  x.  1 )  =  2 )
120118, 119eqtrd 2398 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
2  x.  k )  =  2 )
121118oveq1d 5996 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
12238oveq1i 5991 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
123122, 52eqtri 2386 . . . . . . . . . . . . . . . 16  |-  ( ( 2  x.  1 )  -  1 )  =  1
124123a1i 10 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
( 2  x.  1 )  -  1 )  =  1 )
125121, 124eqtrd 2398 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  1 )
126120, 125oveq12d 5999 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( 2  / 
1 ) )
12737div1i 9635 . . . . . . . . . . . . . 14  |-  ( 2  /  1 )  =  2
128127a1i 10 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
2  /  1 )  =  2 )
129126, 128eqtrd 2398 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  2 )
130120oveq1d 5996 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  ( 2  +  1 ) )
13141a1i 10 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
2  +  1 )  =  3 )
132130, 131eqtrd 2398 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  3 )
133120, 132oveq12d 5999 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( 2  / 
3 ) )
134129, 133oveq12d 5999 . . . . . . . . . . 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 6006 . . . . . . . . . . 11  |-  ( 2  x.  ( 2  / 
3 ) )  e. 
_V
137134, 135, 136fvmpt 5709 . . . . . . . . . 10  |-  ( 1  e.  NN  ->  ( F `  1 )  =  ( 2  x.  ( 2  /  3
) ) )
138117, 137ax-mp 8 . . . . . . . . 9  |-  ( F `
 1 )  =  ( 2  x.  (
2  /  3 ) )
139116, 138eqtr2i 2387 . . . . . . . 8  |-  ( 2  x.  ( 2  / 
3 ) )  =  (  seq  1 (  x.  ,  F ) `
 1 )
140139oveq2i 5992 . . . . . . 7  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  /  (  seq  1 (  x.  ,  F ) `  1
) )
14137, 109mulcli 8989 . . . . . . . . . . 11  |-  ( 2  x.  ( 2  / 
3 ) )  e.  CC
142138, 141eqeltri 2436 . . . . . . . . . 10  |-  ( F `
 1 )  e.  CC
143116, 142eqeltri 2436 . . . . . . . . 9  |-  (  seq  1 (  x.  ,  F ) `  1
)  e.  CC
14437, 92, 62, 108divne0i 9655 . . . . . . . . . . . . 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 9557 . . . . . . . . . . 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 2548 . . . . . . . . 9  |-  (  seq  1 (  x.  ,  F ) `  1
)  =/=  0
15069, 143, 1493pm3.2i 1131 . . . . . . . 8  |-  ( ( pi  /  2 )  e.  CC  /\  (  seq  1 (  x.  ,  F ) `  1
)  e.  CC  /\  (  seq  1 (  x.  ,  F ) ` 
1 )  =/=  0
)
151 divrec 9587 . . . . . . . 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 2386 . . . . . 6  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  1
) ) )
154113, 153eqtri 2386 . . . . 5  |-  ( ( I `  2 )  /  ( I ` 
3 ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq  1 (  x.  ,  F ) `  1
) ) )
15544, 154eqtri 2386 . . . 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 10196 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  y  e.  ZZ )
158157peano2zd 10271 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  ZZ )
159156, 158zmulcld 10274 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  ZZ )
16076a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  e.  RR )
161 nnre 9900 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  y  e.  RR )
162 1re 8984 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
163162a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  1  e.  RR )
164161, 163readdcld 9009 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR )
165 0re 8985 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
166165, 76pm3.2i 441 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  /\  2  e.  RR )
167 2pos 9975 . . . . . . . . . . . . . . . . . 18  |-  0  <  2
168 ltle 9057 . . . . . . . . . . . . . . . . . 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 10121 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  y  e.  NN0 )
172 nn0ge0 10140 . . . . . . . . . . . . . . . . . 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 9432 . . . . . . . . . . . . . . . . . 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 9841 . . . . . . . . . . . . . . 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 10385 . . . . . . . . . . . . . . 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 27321 . . . . . . . . . . . . . 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 967 . . . . . . . . . . . . 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 9901 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  y  e.  CC )
18861a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  1  e.  CC )
189186, 187, 1883jca 1133 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
2  e.  CC  /\  y  e.  CC  /\  1  e.  CC ) )
190 adddi 8973 . . . . . . . . . . . . . . . . . 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 8999 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
2  x.  1 )  =  2 )
193192oveq2d 5997 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
194191, 193eqtrd 2398 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
195194oveq1d 5996 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( ( ( 2  x.  y )  +  2 )  - 
2 ) )
196186, 187mulcld 9002 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  CC )
197196, 186pncand 9305 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  2 )  =  ( 2  x.  y ) )
198195, 197eqtrd 2398 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( 2  x.  y ) )
199198fveq2d 5636 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  -  2 ) )  =  ( I `  ( 2  x.  y
) ) )
200199oveq2d 5997 . . . . . . . . . . . 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 2398 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( 2  x.  y ) ) ) )
202194oveq1d 5996 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( ( 2  x.  y )  +  2 )  +  1 ) )
203196, 186, 188addassd 9004 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  +  1 )  =  ( ( 2  x.  y )  +  ( 2  +  1 ) ) )
204202, 203eqtrd 2398 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( 2  x.  y )  +  ( 2  +  1 ) ) )
20541a1i 10 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  +  1 )  =  3 )
206205oveq2d 5997 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  +  1 ) )  =  ( ( 2  x.  y )  +  3 ) )
207204, 206eqtrd 2398 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( 2  x.  y )  +  3 ) )
208207fveq2d 5636 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  3 ) ) )
209156, 157zmulcld 10274 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  ZZ )
21075a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  3  e.  ZZ )
211209, 210zaddcld 10272 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  ZZ )
212160, 161remulcld 9010 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  RR )
21377a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  3  e.  RR )
214212, 213readdcld 9009 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  RR )
215160, 212, 2143jca 1133 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  e.  RR  /\  ( 2  x.  y
)  e.  RR  /\  ( ( 2  x.  y )  +  3 )  e.  RR ) )
216 nnge1 9919 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  1  <_  y )
217160, 161, 170, 216lemulge11d 9841 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  2  <_  ( 2  x.  y
) )
218165, 77pm3.2i 441 . . . . . . . . . . . . . . . . . . 19  |-  ( 0  e.  RR  /\  3  e.  RR )
21973nngt0i 9926 . . . . . . . . . . . . . . . . . . 19  |-  0  <  3
220 ltle 9057 . . . . . . . . . . . . . . . . . . 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 9431 . . . . . . . . . . . . . . . . . . 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 9061 . . . . . . . . . . . . . . . 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 10385 . . . . . . . . . . . . . . 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 27321 . . . . . . . . . . . . . 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 967 . . . . . . . . . . . . 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 2398 . . . . . . . . . . 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 5999 . . . . . . . . . 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 5996 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( ( 2  x.  y )  +  2 )  - 
1 ) )
239196, 186, 188addsubassd 9324 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
240238, 239eqtrd 2398 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
24152eqcomi 2370 . . . . . . . . . . . . . . . . 17  |-  1  =  ( 2  -  1 )
242241a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  1  =  ( 2  -  1 ) )
243 eqcom 2368 . . . . . . . . . . . . . . . . 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 5997 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  y )  +  1 ) )
247240, 246eqtrd 2398 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  1 ) )
248247oveq1d 5996 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 )  /  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) ) )
249248oveq1d 5996 . . . . . . . . . . 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 9324 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( ( 2  x.  y )  +  ( 3  -  1 ) ) )
25296a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
3  -  1 )  =  2 )
253252oveq2d 5997 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 3  -  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
254251, 253eqtrd 2398 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( ( 2  x.  y )  +  2 ) )
255194eqcomd 2371 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  2 )  =  ( 2  x.  ( y  +  1 ) ) )
256254, 255eqtrd 2398 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( 2  x.  ( y  +  1 ) ) )
257256oveq1d 5996 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
258257oveq1d 5996 . . . . . . . . . . 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 5999 . . . . . . . . . 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 2398 . . . . . . . . 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 9001 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  CC )
262187, 188addcld 9001 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  CC )
263186, 262mulcld 9002 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  CC )
26462a1i 10 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  =/=  0 )
265 peano2nn 9905 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
266 nnne0 9925 . . . . . . . . . . . . . 14  |-  ( ( y  +  1 )  e.  NN  ->  (
y  +  1 )  =/=  0 )
267265, 266syl 15 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
y  +  1 )  =/=  0 )
268186, 262, 264, 267mulne0d 9567 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
269261, 263, 268divcld 9683 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
270 2nn0 10131 . . . . . . . . . . . . . 14  |-  2  e.  NN0
271270a1i 10 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  e.  NN0 )
272271, 171nn0mulcld 10172 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  NN0 )
273 ax-resscn 8941 . . . . . . . . . . . . 13  |-  RR  C_  CC
27448wallispilem3 27322 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  y )  e.  NN0  ->  ( I `
 ( 2  x.  y ) )  e.  RR+ )
275 rpre 10511 . . . . . . . . . . . . . 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 3264 . . . . . . . . . . . 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 9001 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  CC )
280165a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  0  e.  RR )
281280, 212, 2143jca 1133 . . . . . . . . . . . . . . 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 9922 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  0  <  y )
284160, 161, 282, 283mulgt0d 9118 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  0  <  ( 2  x.  y
) )
285213, 219jctir 524 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
3  e.  RR  /\  0  <  3 ) )
286 elrp 10507 . . . . . . . . . . . . . . . . . 18  |-  ( 3  e.  RR+  <->  ( 3  e.  RR  /\  0  <  3 ) )
287285, 286sylibr 203 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  3  e.  RR+ )
288212, 287ltaddrpd 10570 . . . . . . . . . . . . . . . 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 9046 . . . . . . . . . . . . . . 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 9484 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  =/=  0 )
293263, 279, 292divcld 9683 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  CC )
294263, 279, 268, 292divne0d 9699 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  =/=  0 )
295211, 156zsubcld 10273 . . . . . . . . . . . . . . . 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 9434 . . . . . . . . . . . . . . . . . 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 10187 . . . . . . . . . . . . . . 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 27322 . . . . . . . . . . . . . 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 10550 . . . . . . . . . . . 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 9607 . . . . . . . . . 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 2401 . . . . . . . 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 9324 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  ( 3  -  2 ) ) )
312100a1i 10 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
3  -  2 )  =  1 )
313312oveq2d 5997 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 3  -  2 ) )  =  ( ( 2  x.  y )  +  1 ) )
314311, 313eqtrd 2398 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  1 ) )
315314fveq2d 5636 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
316315oveq2d 5997 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  y ) )  /  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
317316oveq2d 5997 . . . . . . . 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 2398 . . . . . . 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 5989 . . . . . . . 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 10415 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  <->  y  e.  ( ZZ>= `  1 )
)
323322biimpi 186 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  ( ZZ>= `  1 )
)
324 seqp1 11225 . . . . . . . . . . . . . 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 5989 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( y  +  1 )  ->  (
2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
328327oveq1d 5996 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
329327, 328oveq12d 5999 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
330327oveq1d 5996 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
331327, 330oveq12d 5999 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
332329, 331oveq12d 5999 . . . . . . . . . . . . . . . 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 9010 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR )
335334, 163resubcld 9358 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR )
336 1lt2 10035 . . . . . . . . . . . . . . . . . . . . 21  |-  1  <  2
337336a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  1  <  2 )
338 nnrp 10514 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  NN  ->  y  e.  RR+ )
339163, 338ltaddrp2d 10571 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  1  <  ( y  +  1 ) )
340160, 164, 337, 339mulgt1d 9840 . . . . . . . . . . . . . . . . . . 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 9102 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN  /\  1  <  ( 2  x.  ( y  +  1 ) ) )  -> 
1  =/=  ( 2  x.  ( y  +  1 ) ) )
344343necomd 2612 . . . . . . . . . . . . . . . . . . . 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 9313 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =/=  0 )
348334, 335, 347redivcld 9735 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  RR )
349207, 214eqeltrd 2440 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  RR )
350207, 292eqnetrd 2547 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =/=  0 )
351334, 349, 350redivcld 9735 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  RR )
352348, 351remulcld 9010 . . . . . . . . . . . . . . 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 5713 . . . . . . . . . . . . . 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 5997 . . . . . . . . . . . . 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 2398 . . . . . . . . . . . 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 5997 . . . . . . . . . . 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 5997 . . . . . . . . . 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 5997 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) ) )
359207oveq2d 5997 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
360358, 359oveq12d 5999 . . . . . . . . . . . . . 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 5997 . . . . . . . . . . . . 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 5997 . . . . . . . . . . . 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 5997 . . . . . . . . . . 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 10972 . . . . . . . . . . . . . . . . . . . 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 5989 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  w  ->  (
2  x.  k )  =  ( 2  x.  w ) )
368367oveq1d 5996 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  w  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  w )  - 
1 ) )
369367, 368oveq12d 5999 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  -  1 ) ) )
370367oveq1d 5996 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  w  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  w )  +  1 ) )
371367, 370oveq12d 5999 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  +  1 ) ) )
372369, 371oveq12d 5999 . . . . . . . . . . . . . . . . . . . . . 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 10510 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  e.  RR+
376375a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  2  e.  RR+ )
377 nnrp 10514 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  w  e.  RR+ )
378376, 377rpmulcld 10557 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  (
2  x.  w )  e.  RR+ )
37976a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  NN  ->  2  e.  RR )
380 nnre 9900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  NN  ->  w  e.  RR )
381379, 380remulcld 9010 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  NN  ->  (
2  x.  w )  e.  RR )
382162a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  NN  ->  1  e.  RR )
383381, 382resubcld 9358 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  -  1 )  e.  RR )
384382, 380, 3813jca 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  NN  ->  (
1  e.  RR  /\  w  e.  RR  /\  (
2  x.  w )  e.  RR ) )
385 nnge1 9919 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  NN  ->  1  <_  w )
386273, 380sseldi 3264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  NN  ->  w  e.  CC )
387 mulid2 8983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  CC  ->  (
1  x.  w )  =  w )
388386, 387syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  NN  ->  (
1  x.  w )  =  w )
389382, 379, 377ltmul1d 10578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4147 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  NN  ->  w  <  ( 2  x.  w
) )
392385, 391jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  NN  ->  (
1  <_  w  /\  w  <  ( 2  x.  w ) ) )
393 lelttr 9059 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9506 . . . . . . . . . . . . . . . . . . . . . . . . . 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 10507 . . . . . . . . . . . . . . . . . . . . . . . 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 10558 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  /  ( ( 2  x.  w )  -  1 ) )  e.  RR+ )
401169a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  0  <_  2 )
402377rpge0d 10545 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  0  <_  w )
403379, 380, 401, 402mulge0d 9496 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  0  <_  ( 2  x.  w
) )
404381, 403ge0p1rpd 10567 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  +  1 )  e.  RR+ )
405378, 404rpdivcld 10558 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  /  ( ( 2  x.  w )  +  1 ) )  e.  RR+ )
406400, 405rpmulcld 10557 . . . . . . . . . . . . . . . . . . . . 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 5713 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  NN  ->  ( F `  w )  =  ( ( ( 2  x.  w )  /  ( ( 2  x.  w )  - 
1 ) )  x.  ( ( 2  x.  w )  /  (
( 2  x.  w
)  +  1 ) ) ) )
408407, 406eqeltrd 2440 . . . . . . . . . . . . . . . . . . 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 10526 . . . . . . . . . . . . . . . . . . 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 11230 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (  seq  1 (  x.  ,  F ) `  y
)  e.  RR+ )
413412rpcnne0d 10550 . . . . . . . . . . . . . . . 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 10567 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR+ )
416414, 415rpmulcld 10557 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR+ )
417160, 161, 170, 173mulge0d 9496 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  0  <_  ( 2  x.  y
) )
418212, 417ge0p1rpd 10567 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  RR+ )
419416, 418rpdivcld 10558 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  e.  RR+ )
420414, 338rpmulcld 10557 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  RR+ )
421420, 287rpaddcld 10556 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  RR+ )
422416, 421rpdivcld 10558 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  RR+ )
423419, 422rpmulcld 10557 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  RR+ )
424423rpcnne0d 10550 . . . . . . . . . . . . . . . 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 1133 . . . . . . . . . . . . . . 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 9618 . . . . . . . . . . . . . . 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 2371 . . . . . . . . . . . . 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 5997 . . . . . . . . . . . 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 9676 . . . . . . . . . . . . . 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 9718 . . . . . . . . . . . . 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 2371 . . . . . . . . . . . 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 2549 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =/=  0 )
439263, 261, 263, 279, 438, 292divmuldivd 9724 . . . . . . . . . . . . . 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 5997 . . . . . . . . . . . . 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 9002 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq  1
(  x.  ,  F
) `  y )
) )  e.  CC )
442263, 263mulcld 9002 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
443261, 279