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

Theorem wallispilem4 37930
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 6298 . . . . . . 7  |-  ( x  =  1  ->  (
2  x.  x )  =  ( 2  x.  1 ) )
21fveq2d 5869 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  1 ) ) )
31oveq1d 6305 . . . . . . 7  |-  ( x  =  1  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
43fveq2d 5869 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  1 )  +  1 ) ) )
52, 4oveq12d 6308 . . . . 5  |-  ( x  =  1  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  1 ) )  / 
( I `  (
( 2  x.  1 )  +  1 ) ) ) )
6 fveq2 5865 . . . . . . 7  |-  ( x  =  1  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  1
) )
76oveq2d 6306 . . . . . 6  |-  ( x  =  1  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
87oveq2d 6306 . . . . 5  |-  ( x  =  1  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  1 )
) ) )
95, 8eqeq12d 2466 . . . 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 6298 . . . . . . 7  |-  ( x  =  y  ->  (
2  x.  x )  =  ( 2  x.  y ) )
1110fveq2d 5869 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  y ) ) )
1210oveq1d 6305 . . . . . . 7  |-  ( x  =  y  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  y )  +  1 ) )
1312fveq2d 5869 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
1411, 13oveq12d 6308 . . . . 5  |-  ( x  =  y  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
15 fveq2 5865 . . . . . . 7  |-  ( x  =  y  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  y
) )
1615oveq2d 6306 . . . . . 6  |-  ( x  =  y  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )
1716oveq2d 6306 . . . . 5  |-  ( x  =  y  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  y )
) ) )
1814, 17eqeq12d 2466 . . . 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 6298 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
2  x.  x )  =  ( 2  x.  ( y  +  1 ) ) )
2019fveq2d 5869 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  ( y  +  1 ) ) ) )
2119oveq1d 6305 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
2221fveq2d 5869 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
2320, 22oveq12d 6308 . . . . 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 5865 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) ) )
2524oveq2d 6306 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) ) ) )
2625oveq2d 6306 . . . . 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 2466 . . . 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 6298 . . . . . . 7  |-  ( x  =  n  ->  (
2  x.  x )  =  ( 2  x.  n ) )
2928fveq2d 5869 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  n ) ) )
3028oveq1d 6305 . . . . . . 7  |-  ( x  =  n  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  n )  +  1 ) )
3130fveq2d 5869 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  n )  +  1 ) ) )
3229, 31oveq12d 6308 . . . . 5  |-  ( x  =  n  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  n ) )  / 
( I `  (
( 2  x.  n
)  +  1 ) ) ) )
33 fveq2 5865 . . . . . . 7  |-  ( x  =  n  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  n
) )
3433oveq2d 6306 . . . . . 6  |-  ( x  =  n  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  n
) ) )
3534oveq2d 6306 . . . . 5  |-  ( x  =  n  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  n )
) ) )
3632, 35eqeq12d 2466 . . . 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 2t1e2 10758 . . . . . . 7  |-  ( 2  x.  1 )  =  2
3837fveq2i 5868 . . . . . 6  |-  ( I `
 ( 2  x.  1 ) )  =  ( I `  2
)
3937oveq1i 6300 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
40 2p1e3 10733 . . . . . . . 8  |-  ( 2  +  1 )  =  3
4139, 40eqtri 2473 . . . . . . 7  |-  ( ( 2  x.  1 )  +  1 )  =  3
4241fveq2i 5868 . . . . . 6  |-  ( I `
 ( ( 2  x.  1 )  +  1 ) )  =  ( I `  3
)
4338, 42oveq12i 6302 . . . . 5  |-  ( ( I `  ( 2  x.  1 ) )  /  ( I `  ( ( 2  x.  1 )  +  1 ) ) )  =  ( ( I ` 
2 )  /  (
I `  3 )
)
44 2z 10969 . . . . . . . . 9  |-  2  e.  ZZ
45 uzid 11173 . . . . . . . . 9  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
4644, 45ax-mp 5 . . . . . . . 8  |-  2  e.  ( ZZ>= `  2 )
47 wallispilem4.2 . . . . . . . . . 10  |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  z ) ^ n
)  _d z )
4847wallispilem2 37928 . . . . . . . . 9  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
2  e.  ( ZZ>= ` 
2 )  ->  (
I `  2 )  =  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  (
2  -  2 ) ) ) ) )
4948simp3i 1019 . . . . . . . 8  |-  ( 2  e.  ( ZZ>= `  2
)  ->  ( I `  2 )  =  ( ( ( 2  -  1 )  / 
2 )  x.  (
I `  ( 2  -  2 ) ) ) )
5046, 49ax-mp 5 . . . . . . 7  |-  ( I `
 2 )  =  ( ( ( 2  -  1 )  / 
2 )  x.  (
I `  ( 2  -  2 ) ) )
51 2m1e1 10724 . . . . . . . . 9  |-  ( 2  -  1 )  =  1
5251oveq1i 6300 . . . . . . . 8  |-  ( ( 2  -  1 )  /  2 )  =  ( 1  /  2
)
53 2cn 10680 . . . . . . . . . . 11  |-  2  e.  CC
5453subidi 9945 . . . . . . . . . 10  |-  ( 2  -  2 )  =  0
5554fveq2i 5868 . . . . . . . . 9  |-  ( I `
 ( 2  -  2 ) )  =  ( I `  0
)
5648simp1i 1017 . . . . . . . . 9  |-  ( I `
 0 )  =  pi
5755, 56eqtri 2473 . . . . . . . 8  |-  ( I `
 ( 2  -  2 ) )  =  pi
5852, 57oveq12i 6302 . . . . . . 7  |-  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  ( 2  -  2 ) ) )  =  ( ( 1  / 
2 )  x.  pi )
59 ax-1cn 9597 . . . . . . . . 9  |-  1  e.  CC
60 2cnne0 10824 . . . . . . . . 9  |-  ( 2  e.  CC  /\  2  =/=  0 )
61 picn 23414 . . . . . . . . 9  |-  pi  e.  CC
62 div32 10290 . . . . . . . . 9  |-  ( ( 1  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 )  /\  pi  e.  CC )  ->  ( ( 1  /  2 )  x.  pi )  =  ( 1  x.  ( pi 
/  2 ) ) )
6359, 60, 61, 62mp3an 1364 . . . . . . . 8  |-  ( ( 1  /  2 )  x.  pi )  =  ( 1  x.  (
pi  /  2 ) )
64 2ne0 10702 . . . . . . . . . 10  |-  2  =/=  0
6561, 53, 64divcli 10349 . . . . . . . . 9  |-  ( pi 
/  2 )  e.  CC
6665mulid2i 9646 . . . . . . . 8  |-  ( 1  x.  ( pi  / 
2 ) )  =  ( pi  /  2
)
6763, 66eqtri 2473 . . . . . . 7  |-  ( ( 1  /  2 )  x.  pi )  =  ( pi  /  2
)
6850, 58, 673eqtri 2477 . . . . . 6  |-  ( I `
 2 )  =  ( pi  /  2
)
69 3z 10970 . . . . . . . . 9  |-  3  e.  ZZ
70 2re 10679 . . . . . . . . . 10  |-  2  e.  RR
71 3re 10683 . . . . . . . . . 10  |-  3  e.  RR
72 2lt3 10777 . . . . . . . . . 10  |-  2  <  3
7370, 71, 72ltleii 9757 . . . . . . . . 9  |-  2  <_  3
74 eluz2 11165 . . . . . . . . 9  |-  ( 3  e.  ( ZZ>= `  2
)  <->  ( 2  e.  ZZ  /\  3  e.  ZZ  /\  2  <_ 
3 ) )
7544, 69, 73, 74mpbir3an 1190 . . . . . . . 8  |-  3  e.  ( ZZ>= `  2 )
7647wallispilem2 37928 . . . . . . . . 9  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
3  e.  ( ZZ>= ` 
2 )  ->  (
I `  3 )  =  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  (
3  -  2 ) ) ) ) )
7776simp3i 1019 . . . . . . . 8  |-  ( 3  e.  ( ZZ>= `  2
)  ->  ( I `  3 )  =  ( ( ( 3  -  1 )  / 
3 )  x.  (
I `  ( 3  -  2 ) ) ) )
7875, 77ax-mp 5 . . . . . . 7  |-  ( I `
 3 )  =  ( ( ( 3  -  1 )  / 
3 )  x.  (
I `  ( 3  -  2 ) ) )
79 3m1e2 10726 . . . . . . . . . 10  |-  ( 3  -  1 )  =  2
8079eqcomi 2460 . . . . . . . . 9  |-  2  =  ( 3  -  1 )
8180oveq1i 6300 . . . . . . . 8  |-  ( 2  /  3 )  =  ( ( 3  -  1 )  /  3
)
82 3cn 10684 . . . . . . . . . . 11  |-  3  e.  CC
8382, 53, 59, 40subaddrii 9964 . . . . . . . . . 10  |-  ( 3  -  2 )  =  1
8483fveq2i 5868 . . . . . . . . 9  |-  ( I `
 ( 3  -  2 ) )  =  ( I `  1
)
8548simp2i 1018 . . . . . . . . 9  |-  ( I `
 1 )  =  2
8684, 85eqtr2i 2474 . . . . . . . 8  |-  2  =  ( I `  ( 3  -  2 ) )
8781, 86oveq12i 6302 . . . . . . 7  |-  ( ( 2  /  3 )  x.  2 )  =  ( ( ( 3  -  1 )  / 
3 )  x.  (
I `  ( 3  -  2 ) ) )
88 3ne0 10704 . . . . . . . . 9  |-  3  =/=  0
8953, 82, 88divcli 10349 . . . . . . . 8  |-  ( 2  /  3 )  e.  CC
9089, 53mulcomi 9649 . . . . . . 7  |-  ( ( 2  /  3 )  x.  2 )  =  ( 2  x.  (
2  /  3 ) )
9178, 87, 903eqtr2i 2479 . . . . . 6  |-  ( I `
 3 )  =  ( 2  x.  (
2  /  3 ) )
9268, 91oveq12i 6302 . . . . 5  |-  ( ( I `  2 )  /  ( I ` 
3 ) )  =  ( ( pi  / 
2 )  /  (
2  x.  ( 2  /  3 ) ) )
93 1z 10967 . . . . . . . . 9  |-  1  e.  ZZ
94 seq1 12226 . . . . . . . . 9  |-  ( 1  e.  ZZ  ->  (  seq 1 (  x.  ,  F ) `  1
)  =  ( F `
 1 ) )
9593, 94ax-mp 5 . . . . . . . 8  |-  (  seq 1 (  x.  ,  F ) `  1
)  =  ( F `
 1 )
96 1nn 10620 . . . . . . . . 9  |-  1  e.  NN
97 oveq2 6298 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
9897, 37syl6eq 2501 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
2  x.  k )  =  2 )
9997oveq1d 6305 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
10037oveq1i 6300 . . . . . . . . . . . . . . 15  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
101100, 51eqtri 2473 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  1 )  -  1 )  =  1
10299, 101syl6eq 2501 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  1 )
10398, 102oveq12d 6308 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( 2  / 
1 ) )
10453div1i 10335 . . . . . . . . . . . 12  |-  ( 2  /  1 )  =  2
105103, 104syl6eq 2501 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  2 )
10698oveq1d 6305 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  ( 2  +  1 ) )
107106, 40syl6eq 2501 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  3 )
10898, 107oveq12d 6308 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( 2  / 
3 ) )
109105, 108oveq12d 6308 . . . . . . . . . 10  |-  ( k  =  1  ->  (
( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) )  =  ( 2  x.  ( 2  /  3
) ) )
110 wallispilem4.1 . . . . . . . . . 10  |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) )
111 ovex 6318 . . . . . . . . . 10  |-  ( 2  x.  ( 2  / 
3 ) )  e. 
_V
112109, 110, 111fvmpt 5948 . . . . . . . . 9  |-  ( 1  e.  NN  ->  ( F `  1 )  =  ( 2  x.  ( 2  /  3
) ) )
11396, 112ax-mp 5 . . . . . . . 8  |-  ( F `
 1 )  =  ( 2  x.  (
2  /  3 ) )
11495, 113eqtr2i 2474 . . . . . . 7  |-  ( 2  x.  ( 2  / 
3 ) )  =  (  seq 1 (  x.  ,  F ) `
 1 )
115114oveq2i 6301 . . . . . 6  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  /  (  seq 1 (  x.  ,  F ) `  1
) )
11653, 89mulcli 9648 . . . . . . . . 9  |-  ( 2  x.  ( 2  / 
3 ) )  e.  CC
117113, 116eqeltri 2525 . . . . . . . 8  |-  ( F `
 1 )  e.  CC
11895, 117eqeltri 2525 . . . . . . 7  |-  (  seq 1 (  x.  ,  F ) `  1
)  e.  CC
11953, 82, 64, 88divne0i 10355 . . . . . . . . 9  |-  ( 2  /  3 )  =/=  0
12053, 89, 64, 119mulne0i 10255 . . . . . . . 8  |-  ( 2  x.  ( 2  / 
3 ) )  =/=  0
121114, 120eqnetrri 2695 . . . . . . 7  |-  (  seq 1 (  x.  ,  F ) `  1
)  =/=  0
12265, 118, 121divreci 10352 . . . . . 6  |-  ( ( pi  /  2 )  /  (  seq 1
(  x.  ,  F
) `  1 )
)  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq 1 (  x.  ,  F ) ` 
1 ) ) )
123115, 122eqtri 2473 . . . . 5  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
12443, 92, 1233eqtri 2477 . . . 4  |-  ( ( I `  ( 2  x.  1 ) )  /  ( I `  ( ( 2  x.  1 )  +  1 ) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
125 oveq2 6298 . . . . . . 7  |-  ( ( ( 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
) ) ) ) )
126125adantl 468 . . . . . 6  |-  ( ( 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 )
) ) ) )
127 2cnd 10682 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  e.  CC )
128 nncn 10617 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  y  e.  CC )
12959a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  1  e.  CC )
130127, 128, 129adddid 9667 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  ( 2  x.  1 ) ) )
131127mulid1d 9660 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  1 )  =  2 )
132131oveq2d 6306 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
133130, 132eqtrd 2485 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
134133oveq1d 6305 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( ( 2  x.  y )  +  2 )  - 
1 ) )
135127, 128mulcld 9663 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  CC )
136135, 127, 129addsubassd 10006 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
13751a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  -  1 )  =  1 )
138137oveq2d 6306 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  y )  +  1 ) )
139134, 136, 1383eqtrd 2489 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  1 ) )
140139oveq1d 6305 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 )  /  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) ) )
141140oveq1d 6305 . . . . . . . . . 10  |-  ( 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 ) ) ) )
14279a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
3  -  1 )  =  2 )
143142oveq2d 6306 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 3  -  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
14482a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  3  e.  CC )
145135, 144, 129addsubassd 10006 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( ( 2  x.  y )  +  ( 3  -  1 ) ) )
146143, 145, 1333eqtr4d 2495 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( 2  x.  ( y  +  1 ) ) )
147146oveq1d 6305 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
148147oveq1d 6305 . . . . . . . . . 10  |-  ( 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 ) ) ) )
149141, 148oveq12d 6308 . . . . . . . . 9  |-  ( 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 ) ) ) ) )
15044a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  ZZ )
151 nnz 10959 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  y  e.  ZZ )
152151peano2zd 11043 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  ZZ )
153150, 152zmulcld 11046 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  ZZ )
15470a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  RR )
155 nnre 10616 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  y  e.  RR )
156 1red 9658 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  1  e.  RR )
157155, 156readdcld 9670 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR )
158 0le2 10700 . . . . . . . . . . . . . . 15  |-  0  <_  2
159158a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <_  2 )
160 nnnn0 10876 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  y  e.  NN0 )
161160nn0ge0d 10928 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  0  <_  y )
162156, 155addge02d 10202 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
0  <_  y  <->  1  <_  ( y  +  1 ) ) )
163161, 162mpbid 214 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  1  <_  ( y  +  1 ) )
164154, 157, 159, 163lemulge11d 10544 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  <_  ( 2  x.  (
y  +  1 ) ) )
16544eluz1i 11166 . . . . . . . . . . . . 13  |-  ( ( 2  x.  ( y  +  1 ) )  e.  ( ZZ>= `  2
)  <->  ( ( 2  x.  ( y  +  1 ) )  e.  ZZ  /\  2  <_ 
( 2  x.  (
y  +  1 ) ) ) )
166153, 164, 165sylanbrc 670 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  ( ZZ>= `  2
) )
16747, 166itgsinexp 37831 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( (
2  x.  ( y  +  1 ) )  -  2 ) ) ) )
168133oveq1d 6305 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( ( ( 2  x.  y )  +  2 )  - 
2 ) )
169135, 127pncand 9987 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  2 )  =  ( 2  x.  y ) )
170168, 169eqtrd 2485 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( 2  x.  y ) )
171170fveq2d 5869 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  -  2 ) )  =  ( I `  ( 2  x.  y
) ) )
172171oveq2d 6306 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
173167, 172eqtrd 2485 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( 2  x.  y ) ) ) )
174133oveq1d 6305 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( ( 2  x.  y )  +  2 )  +  1 ) )
175135, 127, 129addassd 9665 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  +  1 )  =  ( ( 2  x.  y )  +  ( 2  +  1 ) ) )
17640a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  +  1 )  =  3 )
177176oveq2d 6306 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  +  1 ) )  =  ( ( 2  x.  y )  +  3 ) )
178174, 175, 1773eqtrd 2489 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( 2  x.  y )  +  3 ) )
179178fveq2d 5869 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  3 ) ) )
180150, 151zmulcld 11046 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  ZZ )
18169a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  3  e.  ZZ )
182180, 181zaddcld 11044 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  ZZ )
183154, 155remulcld 9671 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  RR )
18471a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  3  e.  RR )
185183, 184readdcld 9670 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  RR )
186 nnge1 10635 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  1  <_  y )
187154, 155, 159, 186lemulge11d 10544 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  <_  ( 2  x.  y
) )
188 0re 9643 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
189 3pos 10703 . . . . . . . . . . . . . . . 16  |-  0  <  3
190188, 71, 189ltleii 9757 . . . . . . . . . . . . . . 15  |-  0  <_  3
191183, 184addge01d 10201 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
0  <_  3  <->  ( 2  x.  y )  <_ 
( ( 2  x.  y )  +  3 ) ) )
192190, 191mpbii 215 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  <_  ( ( 2  x.  y )  +  3 ) )
193154, 183, 185, 187, 192letrd 9792 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  <_  ( ( 2  x.  y )  +  3 ) )
19444eluz1i 11166 . . . . . . . . . . . . 13  |-  ( ( ( 2  x.  y
)  +  3 )  e.  ( ZZ>= `  2
)  <->  ( ( ( 2  x.  y )  +  3 )  e.  ZZ  /\  2  <_ 
( ( 2  x.  y )  +  3 ) ) )
195182, 193, 194sylanbrc 670 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  ( ZZ>= `  2
) )
19647, 195itgsinexp 37831 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  y )  +  3 ) )  =  ( ( ( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  x.  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) ) ) )
197179, 196eqtrd 2485 . . . . . . . . . 10  |-  ( 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 ) ) ) )
198173, 197oveq12d 6308 . . . . . . . . 9  |-  ( 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 ) ) ) ) )
199135, 129addcld 9662 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  CC )
200128, 129addcld 9662 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  CC )
201127, 200mulcld 9663 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  CC )
20264a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  2  =/=  0 )
203 peano2nn 10621 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
204203nnne0d 10654 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
y  +  1 )  =/=  0 )
205127, 200, 202, 204mulne0d 10264 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
206199, 201, 205divcld 10383 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
207 2nn0 10886 . . . . . . . . . . . . 13  |-  2  e.  NN0
208207a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  2  e.  NN0 )
209208, 160nn0mulcld 10930 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  NN0 )
21047wallispilem3 37929 . . . . . . . . . . . 12  |-  ( ( 2  x.  y )  e.  NN0  ->  ( I `
 ( 2  x.  y ) )  e.  RR+ )
211210rpcnd 11343 . . . . . . . . . . 11  |-  ( ( 2  x.  y )  e.  NN0  ->  ( I `
 ( 2  x.  y ) )  e.  CC )
212209, 211syl 17 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  y ) )  e.  CC )
213135, 144addcld 9662 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  CC )
214 0red 9644 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  e.  RR )
215 2pos 10701 . . . . . . . . . . . . . . . 16  |-  0  <  2
216215a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  0  <  2 )
217 nngt0 10638 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  0  <  y )
218154, 155, 216, 217mulgt0d 9790 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <  ( 2  x.  y
) )
219184, 189jctir 541 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
3  e.  RR  /\  0  <  3 ) )
220 elrp 11304 . . . . . . . . . . . . . . . 16  |-  ( 3  e.  RR+  <->  ( 3  e.  RR  /\  0  <  3 ) )
221219, 220sylibr 216 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  3  e.  RR+ )
222183, 221ltaddrpd 11371 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  <  ( ( 2  x.  y )  +  3 ) )
223214, 183, 185, 218, 222lttrd 9796 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <  ( ( 2  x.  y )  +  3 ) )
224223gt0ne0d 10178 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  =/=  0 )
225201, 213, 224divcld 10383 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  CC )
226201, 213, 205, 224divne0d 10399 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  =/=  0 )
227182, 150zsubcld 11045 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  e.  ZZ )
228185, 154subge0d 10203 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
0  <_  ( (
( 2  x.  y
)  +  3 )  -  2 )  <->  2  <_  ( ( 2  x.  y
)  +  3 ) ) )
229193, 228mpbird 236 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <_  ( ( ( 2  x.  y )  +  3 )  -  2 ) )
230 elnn0z 10950 . . . . . . . . . . . . . 14  |-  ( ( ( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0  <->  ( ( ( ( 2  x.  y
)  +  3 )  -  2 )  e.  ZZ  /\  0  <_ 
( ( ( 2  x.  y )  +  3 )  -  2 ) ) )
231227, 229, 230sylanbrc 670 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0 )
23247wallispilem3 37929 . . . . . . . . . . . . 13  |-  ( ( ( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0  ->  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) )  e.  RR+ )
233231, 232syl 17 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) )  e.  RR+ )
234233rpcnne0d 11350 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) )  e.  CC  /\  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) )  =/=  0 ) )
235225, 226, 234jca31 537 . . . . . . . . . 10  |-  ( 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 ) ) )
236 divmuldiv 10307 . . . . . . . . . 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 ) ) ) ) )
237206, 212, 235, 236syl21anc 1267 . . . . . . . . 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 ) ) ) ) )
238149, 198, 2373eqtr4d 2495 . . . . . . . 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 ) ) ) ) )
239135, 144, 127addsubassd 10006 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  ( 3  -  2 ) ) )
24083a1i 11 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
3  -  2 )  =  1 )
241240oveq2d 6306 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 3  -  2 ) )  =  ( ( 2  x.  y )  +  1 ) )
242239, 241eqtrd 2485 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  1 ) )
243242fveq2d 5869 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
244243oveq2d 6306 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  y ) )  /  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
245244oveq2d 6306 . . . . . . . 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 ) ) ) ) )
246238, 245eqtrd 2485 . . . . . . 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 ) ) ) ) )
247246adantr 467 . . . . . 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 ) ) ) ) )
248 elnnuz 11195 . . . . . . . . . . . . 13  |-  ( y  e.  NN  <->  y  e.  ( ZZ>= `  1 )
)
249248biimpi 198 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  y  e.  ( ZZ>= `  1 )
)
250 seqp1 12228 . . . . . . . . . . . 12  |-  ( y  e.  ( ZZ>= `  1
)  ->  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) )  =  ( (  seq 1 (  x.  ,  F ) `  y )  x.  ( F `  ( y  +  1 ) ) ) )
251249, 250syl 17 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) )  =  ( (  seq 1 (  x.  ,  F ) `  y )  x.  ( F `  ( y  +  1 ) ) ) )
252110a1i 11 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) )
253 oveq2 6298 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
254253oveq1d 6305 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
255253, 254oveq12d 6308 . . . . . . . . . . . . . . 15  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
256253oveq1d 6305 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
257253, 256oveq12d 6308 . . . . . . . . . . . . . . 15  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
258255, 257oveq12d 6308 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
259258adantl 468 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) )
260154, 157remulcld 9671 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR )
261260, 156resubcld 10047 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR )
262 1lt2 10776 . . . . . . . . . . . . . . . . . . 19  |-  1  <  2
263262a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  1  <  2 )
264 nnrp 11311 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  y  e.  RR+ )
265156, 264ltaddrp2d 11372 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  1  <  ( y  +  1 ) )
266154, 157, 263, 265mulgt1d 10543 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  1  <  ( 2  x.  (
y  +  1 ) ) )
267156, 266gtned 9770 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  1 )
268201, 129, 267subne0d 9995 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =/=  0 )
269260, 261, 268redivcld 10435 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  RR )
270178, 185eqeltrd 2529 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  RR )
271178, 224eqnetrd 2691 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =/=  0 )
272260, 270, 271redivcld 10435 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  RR )
273269, 272remulcld 9671 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  e.  RR )
274252, 259, 203, 273fvmptd 5954 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
275274oveq2d 6306 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
276251, 275eqtrd 2485 . . . . . . . . . 10  |-  ( 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 ) ) ) ) )
277276oveq2d 6306 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
278277oveq2d 6306 . . . . . . . 8  |-  ( 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 ) ) ) ) ) ) )
279139oveq2d 6306 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) ) )
280178oveq2d 6306 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
281279, 280oveq12d 6308 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
282281oveq2d 6306 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
283282oveq2d 6306 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
284283oveq2d 6306 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) ) )
285 elfznn 11828 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  ( 1 ... y )  ->  w  e.  NN )
286285adantl 468 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  NN  /\  w  e.  ( 1 ... y ) )  ->  w  e.  NN )
287110a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  NN  ->  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) )
288 oveq2 6298 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
2  x.  k )  =  ( 2  x.  w ) )
289288oveq1d 6305 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  w )  - 
1 ) )
290288, 289oveq12d 6308 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  -  1 ) ) )
291288oveq1d 6305 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  w )  +  1 ) )
292288, 291oveq12d 6308 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  +  1 ) ) )
293290, 292oveq12d 6308 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) ) )
294293adantl 468 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) )
295 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  NN  ->  w  e.  NN )
296 2rp 11307 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  RR+
297296a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  2  e.  RR+ )
298 nnrp 11311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  w  e.  RR+ )
299297, 298rpmulcld 11357 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  NN  ->  (
2  x.  w )  e.  RR+ )
30070a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  2  e.  RR )
301 nnre 10616 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  w  e.  RR )
302300, 301remulcld 9671 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  (
2  x.  w )  e.  RR )
303 1red 9658 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  1  e.  RR )
304302, 303resubcld 10047 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  -  1 )  e.  RR )
305 nnge1 10635 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  1  <_  w )
306 nncn 10617 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  w  e.  CC )
307306mulid2d 9661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  (
1  x.  w )  =  w )
308303, 300, 298ltmul1d 11379 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  (
1  <  2  <->  ( 1  x.  w )  < 
( 2  x.  w
) ) )
309262, 308mpbii 215 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  (
1  x.  w )  <  ( 2  x.  w ) )
310307, 309eqbrtrrd 4425 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  w  <  ( 2  x.  w
) )
311303, 301, 302, 305, 310lelttrd 9793 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  1  <  ( 2  x.  w
) )
312303, 302posdifd 10200 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  (
1  <  ( 2  x.  w )  <->  0  <  ( ( 2  x.  w
)  -  1 ) ) )
313311, 312mpbid 214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  0  <  ( ( 2  x.  w )  -  1 ) )
314304, 313elrpd 11338 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  -  1 )  e.  RR+ )
315299, 314rpdivcld 11358 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  /  ( ( 2  x.  w )  -  1 ) )  e.  RR+ )
316158a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  0  <_  2 )
317298rpge0d 11345 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  0  <_  w )
318300, 301, 316, 317mulge0d 10190 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  0  <_  ( 2  x.  w
) )
319302, 318ge0p1rpd 11368 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  +  1 )  e.  RR+ )
320299, 319rpdivcld 11358 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  /  ( ( 2  x.  w )  +  1 ) )  e.  RR+ )
321315, 320rpmulcld 11357 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  NN  ->  (
( ( 2  x.  w )  /  (
( 2  x.  w
)  -  1 ) )  x.  ( ( 2  x.  w )  /  ( ( 2  x.  w )  +  1 ) ) )  e.  RR+ )
322287, 294, 295, 321fvmptd 5954 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  NN  ->  ( F `  w )  =  ( ( ( 2  x.  w )  /  ( ( 2  x.  w )  - 
1 ) )  x.  ( ( 2  x.  w )  /  (
( 2  x.  w
)  +  1 ) ) ) )
323322, 321eqeltrd 2529 . . . . . . . . . . . . . . . 16  |-  ( w  e.  NN  ->  ( F `  w )  e.  RR+ )
324286, 323syl 17 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  w  e.  ( 1 ... y ) )  ->  ( F `  w )  e.  RR+ )
325 rpmulcl 11324 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  RR+  /\  z  e.  RR+ )  ->  (
w  x.  z )  e.  RR+ )
326325adantl 468 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  ( w  e.  RR+  /\  z  e.  RR+ ) )  -> 
( w  x.  z
)  e.  RR+ )
327249, 324, 326seqcl 12233 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (  seq 1 (  x.  ,  F ) `  y
)  e.  RR+ )
328327rpcnne0d 11350 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
(  seq 1 (  x.  ,  F ) `  y )  e.  CC  /\  (  seq 1 (  x.  ,  F ) `
 y )  =/=  0 ) )
329296a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  2  e.  RR+ )
330155, 161ge0p1rpd 11368 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR+ )
331329, 330rpmulcld 11357 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR+ )
332154, 155, 159, 161mulge0d 10190 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  0  <_  ( 2  x.  y
) )
333183, 332ge0p1rpd 11368 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  RR+ )
334331, 333rpdivcld 11358 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  e.  RR+ )
335329, 264rpmulcld 11357 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  RR+ )
336335, 221rpaddcld 11356 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  RR+ )
337331, 336rpdivcld 11358 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  RR+ )
338334, 337rpmulcld 11357 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  RR+ )
339338rpcnne0d 11350 . . . . . . . . . . . . 13  |-  ( 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 ) )
340 divdiv1 10318 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) ) ) )
341129, 328, 339, 340syl3anc 1268 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) ) )
342341eqcomd 2457 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
343342oveq2d 6306 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
34465a1i 11 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
pi  /  2 )  e.  CC )
345327rpcnd 11343 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (  seq 1 (  x.  ,  F ) `  y
)  e.  CC )
346327rpne0d 11346 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (  seq 1 (  x.  ,  F ) `  y
)  =/=  0 )
347345, 346reccld 10376 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  y
) )  e.  CC )
348338rpcnd 11343 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  CC )
349338rpne0d 11346 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  =/=  0 )
350344, 347, 348, 349divassd 10418 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
351139, 268eqnetrrd 2692 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =/=  0 )
352201, 199, 201, 213, 351, 224divmuldivd 10424 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
353352oveq2d 6306 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
354344, 347mulcld 9663 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  y )
) )  e.  CC )
355201, 201mulcld 9663 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
356199, 213mulcld 9663 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  3 ) )  e.  CC )
357201, 201, 205, 205mulne0d 10264 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  =/=  0 )
358199, 213, 351, 224mulne0d 10264 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  3 ) )  =/=  0 )
359354, 355, 356, 357, 358divdiv2d 10415 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 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 ) ) ) )  =  ( ( ( ( pi 
/  2 )  x.  ( 1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )  x.  ( ( ( 2  x.  y )  +  1 )  x.  (
( 2  x.  y
)  +  3 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) ) ) )
360354, 356, 355, 357divassd 10418 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( ( pi 
/  2 )  x.  ( 1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )  x.  ( ( ( 2  x.  y )  +  1 )  x.  (
( 2  x.  y
)  +  3 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) ) )  =  ( ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  y )
) )  x.  (
( ( ( 2  x.  y )  +  1 )  x.  (
( 2  x.  y
)  +  3 ) )  /  ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) ) ) ) )
361359, 360eqtrd 2485 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 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 ) ) ) )  =  ( ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )  x.  ( ( ( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  3 ) )  /  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) ) ) ) )
362199, 201, 201, 213, 205, 224, 205divdivdivd 10430 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  1 )  /  (
2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  =  ( ( ( ( 2  x.  y
)  +  1 )  x.  ( ( 2  x.  y )  +  3 ) )  / 
( ( 2  x.  ( y  +  1 ) )  x.  (
2  x.  ( y  +  1 ) ) ) ) )
363362eqcomd 2457 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  1 )  x.  (
( 2  x.  y
)  +  3 ) )  /  ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) ) )  =  ( ( ( ( 2  x.  y
)  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  / 
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  3 ) ) ) )
364363oveq2d 6306 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )  x.  ( ( ( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  3 ) )  /  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) ) ) )  =  ( ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )  x.  ( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) )
365353, 361, 3643eqtrd 2489 . . . . . . . . . 10  |-  ( 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
) ) )  x.  ( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) )
366343, 350, 3653eqtr2d 2491 . . . . . . . . 9  |-  ( 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
) ) )  x.  ( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) ) )
36761a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  pi  e.  CC )
368367halfcld 10857 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
pi  /  2 )  e.  CC )
369368, 347mulcld 9663 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  y )
) )  e.  CC )
370206, 225, 226divcld 10383 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  1 )  /  (
2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  CC )
371369, 370mulcomd 9664 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )  x.  ( ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) ) )  =  ( ( ( ( ( 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 ) ) ) ) )
372284, 366, 3713eqtrd 2489 . . . . . . . 8  |-  ( 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 ) ) ) ) ) )  =  ( ( ( ( ( 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 ) ) ) ) )
373278, 372eqtrd 2485 . . . . . . 7  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  ( 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 ) ) ) ) )
374373adantr 467 . . . . . 6  |-  ( ( y  e.  NN  /\  ( ( I `  ( 2  x.  y
) )  /  (
I `  ( (
2  x.  y )  +  1 ) ) )  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq 1 (  x.  ,  F ) `  y ) ) ) )  ->  ( (
pi  /  2 )  x.  ( 1  / 
(  seq 1 (  x.  ,  F ) `  ( 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
) ) ) ) )
375126, 247, 3743eqtr4d 2495 . . . . 5  |-  ( ( 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 ) ) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  ( y  +  1 ) ) ) ) )
376375ex 436 . . . 4  |-  ( 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 ) ) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  ( y  +  1 ) ) ) ) ) )
3779, 18, 27, 36, 124, 376nnind 10627 . . 3  |-  ( n  e.  NN  ->  (
( I `  (
2  x.  n ) )  /  ( I `
 ( ( 2  x.  n )  +  1 ) ) )  =  ( ( pi 
/  2 )  x.  ( 1  /  (  seq 1 (  x.  ,  F ) `  n
) ) ) )
378377mpteq2ia 4485 . 2  |-  ( n  e.  NN  |->  ( ( I `  ( 2  x.  n ) )  /  ( I `  ( ( 2  x.  n )  +  1 ) ) ) )  =  ( n  e.  NN  |->  ( ( pi 
/  2 )  x.  ( 1  /  (  seq 1 (  x.  ,  F ) `  n
) ) ) )
379 wallispilem4.3 . 2  |-  G  =  ( n  e.  NN  |->  ( ( I `  ( 2  x.  n
) )  /  (
I `  ( (
2  x.  n )  +  1 ) ) ) )
380 wallispilem4.4 . 2  |-  H  =  ( n  e.  NN  |->  ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  n
) ) ) )
381378, 379, 3803eqtr4i 2483 1  |-  G  =  H
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1444    e. wcel 1887    =/= wne 2622   class class class wbr 4402    |-> cmpt 4461   ` cfv 5582  (class class class)co 6290   CCcc 9537   RRcr 9538   0cc0 9539   1c1 9540    + caddc 9542    x. cmul 9544    < clt 9675    <_ cle 9676    - cmin 9860    / cdiv 10269   NNcn 10609   2c2 10659   3c3 10660   NN0cn0 10869   ZZcz 10937   ZZ>=cuz 11159   RR+crp 11302   (,)cioo 11635   ...cfz 11784    seqcseq 12213   ^cexp 12272   sincsin 14116   picpi 14119   S.citg 22576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-cc 8865  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617  ax-addf 9618  ax-mulf 9619
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-disj 4374  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-of 6531  df-ofr 6532  df-om 6693  df-1st 6793  df-2nd 6794  df-supp 6915  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-omul 7187  df-er 7363  df-map 7474  df-pm 7475  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7884  df-fi 7925  df-sup 7956  df-inf 7957  df-oi 8025  df-card 8373  df-acn 8376  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ioc 11640  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-fl 12028  df-mod 12097  df-seq 12214  df-exp 12273  df-fac 12460  df-bc 12488  df-hash 12516  df-shft 13130  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-limsup 13526  df-clim 13552  df-rlim 13553  df-sum 13753  df-ef 14121  df-sin 14123  df-cos 14124  df-pi 14126  df-struct 15123  df-ndx 15124  df-slot 15125  df-base 15126  df-sets 15127  df-ress 15128  df-plusg 15203  df-mulr 15204  df-starv 15205  df-sca 15206  df-vsca 15207  df-ip 15208  df-tset 15209  df-ple 15210  df-ds 15212  df-unif 15213  df-hom 15214  df-cco 15215  df-rest 15321  df-topn 15322  df-0g 15340  df-gsum 15341  df-topgen 15342  df-pt 15343  df-prds 15346  df-xrs 15400  df-qtop 15406  df-imas 15407  df-xps 15410  df-mre 15492  df-mrc 15493  df-acs 15495  df-mgm 16488  df-sgrp 16527  df-mnd 16537  df-submnd 16583  df-mulg 16676  df-cntz 16971  df-cmn 17432  df-psmet 18962  df-xmet 18963  df-met 18964  df-bl 18965  df-mopn 18966  df-fbas 18967  df-fg 18968  df-cnfld 18971  df-top 19921  df-bases 19922  df-topon 19923  df-topsp 19924  df-cld 20034  df-ntr 20035  df-cls 20036  df-nei 20114  df-lp 20152  df-perf 20153  df-cn 20243  df-cnp 20244  df-haus 20331  df-cmp 20402  df-tx 20577  df-hmeo 20770  df-fil 20861  df-fm 20953  df-flim 20954  df-flf 20955  df-xms 21335  df-ms 21336  df-tms 21337  df-cncf 21910  df-ovol 22416  df-vol 22418  df-mbf 22577  df-itg1 22578  df-itg2 22579  df-ibl 22580  df-itg 22581  df-0p 22628  df-limc 22821  df-dv 22822
This theorem is referenced by:  wallispilem5  37931
  Copyright terms: Public domain W3C validator