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

Theorem wallispilem4 32053
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 6304 . . . . . . 7  |-  ( x  =  1  ->  (
2  x.  x )  =  ( 2  x.  1 ) )
21fveq2d 5876 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  1 ) ) )
31oveq1d 6311 . . . . . . 7  |-  ( x  =  1  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
43fveq2d 5876 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  1 )  +  1 ) ) )
52, 4oveq12d 6314 . . . . 5  |-  ( x  =  1  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  1 ) )  / 
( I `  (
( 2  x.  1 )  +  1 ) ) ) )
6 fveq2 5872 . . . . . . 7  |-  ( x  =  1  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  1
) )
76oveq2d 6312 . . . . . 6  |-  ( x  =  1  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
87oveq2d 6312 . . . . 5  |-  ( x  =  1  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  1 )
) ) )
95, 8eqeq12d 2479 . . . 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 6304 . . . . . . 7  |-  ( x  =  y  ->  (
2  x.  x )  =  ( 2  x.  y ) )
1110fveq2d 5876 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  y ) ) )
1210oveq1d 6311 . . . . . . 7  |-  ( x  =  y  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  y )  +  1 ) )
1312fveq2d 5876 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
1411, 13oveq12d 6314 . . . . 5  |-  ( x  =  y  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
15 fveq2 5872 . . . . . . 7  |-  ( x  =  y  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  y
) )
1615oveq2d 6312 . . . . . 6  |-  ( x  =  y  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )
1716oveq2d 6312 . . . . 5  |-  ( x  =  y  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  y )
) ) )
1814, 17eqeq12d 2479 . . . 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 6304 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
2  x.  x )  =  ( 2  x.  ( y  +  1 ) ) )
2019fveq2d 5876 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  ( y  +  1 ) ) ) )
2119oveq1d 6311 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
2221fveq2d 5876 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
2320, 22oveq12d 6314 . . . . 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 5872 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) ) )
2524oveq2d 6312 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) ) ) )
2625oveq2d 6312 . . . . 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 2479 . . . 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 6304 . . . . . . 7  |-  ( x  =  n  ->  (
2  x.  x )  =  ( 2  x.  n ) )
2928fveq2d 5876 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  n ) ) )
3028oveq1d 6311 . . . . . . 7  |-  ( x  =  n  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  n )  +  1 ) )
3130fveq2d 5876 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  n )  +  1 ) ) )
3229, 31oveq12d 6314 . . . . 5  |-  ( x  =  n  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  n ) )  / 
( I `  (
( 2  x.  n
)  +  1 ) ) ) )
33 fveq2 5872 . . . . . . 7  |-  ( x  =  n  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  n
) )
3433oveq2d 6312 . . . . . 6  |-  ( x  =  n  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  n
) ) )
3534oveq2d 6312 . . . . 5  |-  ( x  =  n  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  n )
) ) )
3632, 35eqeq12d 2479 . . . 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 10705 . . . . . . 7  |-  ( 2  x.  1 )  =  2
3837fveq2i 5875 . . . . . 6  |-  ( I `
 ( 2  x.  1 ) )  =  ( I `  2
)
3937oveq1i 6306 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
40 2p1e3 10680 . . . . . . . 8  |-  ( 2  +  1 )  =  3
4139, 40eqtri 2486 . . . . . . 7  |-  ( ( 2  x.  1 )  +  1 )  =  3
4241fveq2i 5875 . . . . . 6  |-  ( I `
 ( ( 2  x.  1 )  +  1 ) )  =  ( I `  3
)
4338, 42oveq12i 6308 . . . . 5  |-  ( ( I `  ( 2  x.  1 ) )  /  ( I `  ( ( 2  x.  1 )  +  1 ) ) )  =  ( ( I ` 
2 )  /  (
I `  3 )
)
44 2z 10917 . . . . . . . . 9  |-  2  e.  ZZ
45 uzid 11120 . . . . . . . . 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 32051 . . . . . . . . 9  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
2  e.  ( ZZ>= ` 
2 )  ->  (
I `  2 )  =  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  (
2  -  2 ) ) ) ) )
4948simp3i 1007 . . . . . . . 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 10671 . . . . . . . . 9  |-  ( 2  -  1 )  =  1
5251oveq1i 6306 . . . . . . . 8  |-  ( ( 2  -  1 )  /  2 )  =  ( 1  /  2
)
53 2cn 10627 . . . . . . . . . . 11  |-  2  e.  CC
5453subidi 9909 . . . . . . . . . 10  |-  ( 2  -  2 )  =  0
5554fveq2i 5875 . . . . . . . . 9  |-  ( I `
 ( 2  -  2 ) )  =  ( I `  0
)
5648simp1i 1005 . . . . . . . . 9  |-  ( I `
 0 )  =  pi
5755, 56eqtri 2486 . . . . . . . 8  |-  ( I `
 ( 2  -  2 ) )  =  pi
5852, 57oveq12i 6308 . . . . . . 7  |-  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  ( 2  -  2 ) ) )  =  ( ( 1  / 
2 )  x.  pi )
59 ax-1cn 9567 . . . . . . . . 9  |-  1  e.  CC
60 2cnne0 10771 . . . . . . . . 9  |-  ( 2  e.  CC  /\  2  =/=  0 )
61 picn 22978 . . . . . . . . 9  |-  pi  e.  CC
62 div32 10248 . . . . . . . . 9  |-  ( ( 1  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 )  /\  pi  e.  CC )  ->  ( ( 1  /  2 )  x.  pi )  =  ( 1  x.  ( pi 
/  2 ) ) )
6359, 60, 61, 62mp3an 1324 . . . . . . . 8  |-  ( ( 1  /  2 )  x.  pi )  =  ( 1  x.  (
pi  /  2 ) )
64 2ne0 10649 . . . . . . . . . 10  |-  2  =/=  0
6561, 53, 64divcli 10307 . . . . . . . . 9  |-  ( pi 
/  2 )  e.  CC
6665mulid2i 9616 . . . . . . . 8  |-  ( 1  x.  ( pi  / 
2 ) )  =  ( pi  /  2
)
6763, 66eqtri 2486 . . . . . . 7  |-  ( ( 1  /  2 )  x.  pi )  =  ( pi  /  2
)
6850, 58, 673eqtri 2490 . . . . . 6  |-  ( I `
 2 )  =  ( pi  /  2
)
69 3z 10918 . . . . . . . . 9  |-  3  e.  ZZ
70 2re 10626 . . . . . . . . . 10  |-  2  e.  RR
71 3re 10630 . . . . . . . . . 10  |-  3  e.  RR
72 2lt3 10724 . . . . . . . . . 10  |-  2  <  3
7370, 71, 72ltleii 9724 . . . . . . . . 9  |-  2  <_  3
74 eluz2 11112 . . . . . . . . 9  |-  ( 3  e.  ( ZZ>= `  2
)  <->  ( 2  e.  ZZ  /\  3  e.  ZZ  /\  2  <_ 
3 ) )
7544, 69, 73, 74mpbir3an 1178 . . . . . . . 8  |-  3  e.  ( ZZ>= `  2 )
7647wallispilem2 32051 . . . . . . . . 9  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
3  e.  ( ZZ>= ` 
2 )  ->  (
I `  3 )  =  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  (
3  -  2 ) ) ) ) )
7776simp3i 1007 . . . . . . . 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 10673 . . . . . . . . . 10  |-  ( 3  -  1 )  =  2
8079eqcomi 2470 . . . . . . . . 9  |-  2  =  ( 3  -  1 )
8180oveq1i 6306 . . . . . . . 8  |-  ( 2  /  3 )  =  ( ( 3  -  1 )  /  3
)
82 3cn 10631 . . . . . . . . . . 11  |-  3  e.  CC
8382, 53, 59, 40subaddrii 9928 . . . . . . . . . 10  |-  ( 3  -  2 )  =  1
8483fveq2i 5875 . . . . . . . . 9  |-  ( I `
 ( 3  -  2 ) )  =  ( I `  1
)
8548simp2i 1006 . . . . . . . . 9  |-  ( I `
 1 )  =  2
8684, 85eqtr2i 2487 . . . . . . . 8  |-  2  =  ( I `  ( 3  -  2 ) )
8781, 86oveq12i 6308 . . . . . . 7  |-  ( ( 2  /  3 )  x.  2 )  =  ( ( ( 3  -  1 )  / 
3 )  x.  (
I `  ( 3  -  2 ) ) )
88 3ne0 10651 . . . . . . . . 9  |-  3  =/=  0
8953, 82, 88divcli 10307 . . . . . . . 8  |-  ( 2  /  3 )  e.  CC
9089, 53mulcomi 9619 . . . . . . 7  |-  ( ( 2  /  3 )  x.  2 )  =  ( 2  x.  (
2  /  3 ) )
9178, 87, 903eqtr2i 2492 . . . . . 6  |-  ( I `
 3 )  =  ( 2  x.  (
2  /  3 ) )
9268, 91oveq12i 6308 . . . . 5  |-  ( ( I `  2 )  /  ( I ` 
3 ) )  =  ( ( pi  / 
2 )  /  (
2  x.  ( 2  /  3 ) ) )
93 1z 10915 . . . . . . . . 9  |-  1  e.  ZZ
94 seq1 12123 . . . . . . . . 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 10567 . . . . . . . . 9  |-  1  e.  NN
97 oveq2 6304 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
9897, 37syl6eq 2514 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
2  x.  k )  =  2 )
9997oveq1d 6311 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
10037oveq1i 6306 . . . . . . . . . . . . . . 15  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
101100, 51eqtri 2486 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  1 )  -  1 )  =  1
10299, 101syl6eq 2514 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  1 )
10398, 102oveq12d 6314 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( 2  / 
1 ) )
10453div1i 10293 . . . . . . . . . . . 12  |-  ( 2  /  1 )  =  2
105103, 104syl6eq 2514 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  2 )
10698oveq1d 6311 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  ( 2  +  1 ) )
107106, 40syl6eq 2514 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  3 )
10898, 107oveq12d 6314 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( 2  / 
3 ) )
109105, 108oveq12d 6314 . . . . . . . . . 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 6324 . . . . . . . . . 10  |-  ( 2  x.  ( 2  / 
3 ) )  e. 
_V
112109, 110, 111fvmpt 5956 . . . . . . . . 9  |-  ( 1  e.  NN  ->  ( F `  1 )  =  ( 2  x.  ( 2  /  3
) ) )
11396, 112ax-mp 5 . . . . . . . 8  |-  ( F `
 1 )  =  ( 2  x.  (
2  /  3 ) )
11495, 113eqtr2i 2487 . . . . . . 7  |-  ( 2  x.  ( 2  / 
3 ) )  =  (  seq 1 (  x.  ,  F ) `
 1 )
115114oveq2i 6307 . . . . . 6  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  /  (  seq 1 (  x.  ,  F ) `  1
) )
11653, 89mulcli 9618 . . . . . . . . 9  |-  ( 2  x.  ( 2  / 
3 ) )  e.  CC
117113, 116eqeltri 2541 . . . . . . . 8  |-  ( F `
 1 )  e.  CC
11895, 117eqeltri 2541 . . . . . . 7  |-  (  seq 1 (  x.  ,  F ) `  1
)  e.  CC
11953, 82, 64, 88divne0i 10313 . . . . . . . . 9  |-  ( 2  /  3 )  =/=  0
12053, 89, 64, 119mulne0i 10213 . . . . . . . 8  |-  ( 2  x.  ( 2  / 
3 ) )  =/=  0
121114, 120eqnetrri 2754 . . . . . . 7  |-  (  seq 1 (  x.  ,  F ) `  1
)  =/=  0
12265, 118, 121divreci 10310 . . . . . 6  |-  ( ( pi  /  2 )  /  (  seq 1
(  x.  ,  F
) `  1 )
)  =  ( ( pi  /  2 )  x.  ( 1  / 
(  seq 1 (  x.  ,  F ) ` 
1 ) ) )
123115, 122eqtri 2486 . . . . 5  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
12443, 92, 1233eqtri 2490 . . . 4  |-  ( ( I `  ( 2  x.  1 ) )  /  ( I `  ( ( 2  x.  1 )  +  1 ) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
125 oveq2 6304 . . . . . . 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 466 . . . . . 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 10629 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  e.  CC )
128 nncn 10564 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  y  e.  CC )
12959a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  1  e.  CC )
130127, 128, 129adddid 9637 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  ( 2  x.  1 ) ) )
131127mulid1d 9630 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  1 )  =  2 )
132131oveq2d 6312 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
133130, 132eqtrd 2498 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
134133oveq1d 6311 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( ( 2  x.  y )  +  2 )  - 
1 ) )
135127, 128mulcld 9633 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  CC )
136135, 127, 129addsubassd 9970 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
13751a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  -  1 )  =  1 )
138137oveq2d 6312 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  y )  +  1 ) )
139134, 136, 1383eqtrd 2502 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  1 ) )
140139oveq1d 6311 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 )  /  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) ) )
141140oveq1d 6311 . . . . . . . . . 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 6312 . . . . . . . . . . . . 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 9970 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( ( 2  x.  y )  +  ( 3  -  1 ) ) )
146143, 145, 1333eqtr4d 2508 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( 2  x.  ( y  +  1 ) ) )
147146oveq1d 6311 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
148147oveq1d 6311 . . . . . . . . . 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 6314 . . . . . . . . 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 10907 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  y  e.  ZZ )
152151peano2zd 10993 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  ZZ )
153150, 152zmulcld 10996 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  ZZ )
15470a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  RR )
155 nnre 10563 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  y  e.  RR )
156 1red 9628 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  1  e.  RR )
157155, 156readdcld 9640 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR )
158 0le2 10647 . . . . . . . . . . . . . . 15  |-  0  <_  2
159158a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <_  2 )
160 nnnn0 10823 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  y  e.  NN0 )
161160nn0ge0d 10876 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  0  <_  y )
162156, 155addge02d 10162 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
0  <_  y  <->  1  <_  ( y  +  1 ) ) )
163161, 162mpbid 210 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  1  <_  ( y  +  1 ) )
164154, 157, 159, 163lemulge11d 10503 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  <_  ( 2  x.  (
y  +  1 ) ) )
16544eluz1i 11113 . . . . . . . . . . . . 13  |-  ( ( 2  x.  ( y  +  1 ) )  e.  ( ZZ>= `  2
)  <->  ( ( 2  x.  ( y  +  1 ) )  e.  ZZ  /\  2  <_ 
( 2  x.  (
y  +  1 ) ) ) )
166153, 164, 165sylanbrc 664 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  ( ZZ>= `  2
) )
16747, 166itgsinexp 31956 . . . . . . . . . . 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 6311 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( ( ( 2  x.  y )  +  2 )  - 
2 ) )
169135, 127pncand 9951 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  2 )  =  ( 2  x.  y ) )
170168, 169eqtrd 2498 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( 2  x.  y ) )
171170fveq2d 5876 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  -  2 ) )  =  ( I `  ( 2  x.  y
) ) )
172171oveq2d 6312 . . . . . . . . . . 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 2498 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( 2  x.  y ) ) ) )
174133oveq1d 6311 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( ( 2  x.  y )  +  2 )  +  1 ) )
175135, 127, 129addassd 9635 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  +  1 )  =  ( ( 2  x.  y )  +  ( 2  +  1 ) ) )
17640a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  +  1 )  =  3 )
177176oveq2d 6312 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  +  1 ) )  =  ( ( 2  x.  y )  +  3 ) )
178174, 175, 1773eqtrd 2502 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( 2  x.  y )  +  3 ) )
179178fveq2d 5876 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  3 ) ) )
180150, 151zmulcld 10996 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  ZZ )
18169a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  3  e.  ZZ )
182180, 181zaddcld 10994 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  ZZ )
183154, 155remulcld 9641 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  RR )
18471a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  3  e.  RR )
185183, 184readdcld 9640 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  RR )
186 nnge1 10582 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  1  <_  y )
187154, 155, 159, 186lemulge11d 10503 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  <_  ( 2  x.  y
) )
188 0re 9613 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
189 3pos 10650 . . . . . . . . . . . . . . . 16  |-  0  <  3
190188, 71, 189ltleii 9724 . . . . . . . . . . . . . . 15  |-  0  <_  3
191183, 184addge01d 10161 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
0  <_  3  <->  ( 2  x.  y )  <_ 
( ( 2  x.  y )  +  3 ) ) )
192190, 191mpbii 211 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  <_  ( ( 2  x.  y )  +  3 ) )
193154, 183, 185, 187, 192letrd 9756 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  <_  ( ( 2  x.  y )  +  3 ) )
19444eluz1i 11113 . . . . . . . . . . . . 13  |-  ( ( ( 2  x.  y
)  +  3 )  e.  ( ZZ>= `  2
)  <->  ( ( ( 2  x.  y )  +  3 )  e.  ZZ  /\  2  <_ 
( ( 2  x.  y )  +  3 ) ) )
195182, 193, 194sylanbrc 664 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  ( ZZ>= `  2
) )
19647, 195itgsinexp 31956 . . . . . . . . . . 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 2498 . . . . . . . . . 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 6314 . . . . . . . . 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 9632 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  CC )
200128, 129addcld 9632 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  CC )
201127, 200mulcld 9633 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  CC )
20264a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  2  =/=  0 )
203 peano2nn 10568 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
204203nnne0d 10601 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
y  +  1 )  =/=  0 )
205127, 200, 202, 204mulne0d 10222 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
206199, 201, 205divcld 10341 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  /  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
207 2nn0 10833 . . . . . . . . . . . . 13  |-  2  e.  NN0
208207a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  2  e.  NN0 )
209208, 160nn0mulcld 10878 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  NN0 )
21047wallispilem3 32052 . . . . . . . . . . . 12  |-  ( ( 2  x.  y )  e.  NN0  ->  ( I `
 ( 2  x.  y ) )  e.  RR+ )
211210rpcnd 11283 . . . . . . . . . . 11  |-  ( ( 2  x.  y )  e.  NN0  ->  ( I `
 ( 2  x.  y ) )  e.  CC )
212209, 211syl 16 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  y ) )  e.  CC )
213135, 144addcld 9632 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  CC )
214 0red 9614 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  e.  RR )
215 2pos 10648 . . . . . . . . . . . . . . . 16  |-  0  <  2
216215a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  0  <  2 )
217 nngt0 10585 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  0  <  y )
218154, 155, 216, 217mulgt0d 9754 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <  ( 2  x.  y
) )
219184, 189jctir 538 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
3  e.  RR  /\  0  <  3 ) )
220 elrp 11247 . . . . . . . . . . . . . . . 16  |-  ( 3  e.  RR+  <->  ( 3  e.  RR  /\  0  <  3 ) )
221219, 220sylibr 212 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  3  e.  RR+ )
222183, 221ltaddrpd 11310 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  y )  <  ( ( 2  x.  y )  +  3 ) )
223214, 183, 185, 218, 222lttrd 9760 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <  ( ( 2  x.  y )  +  3 ) )
224223gt0ne0d 10138 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  =/=  0 )
225201, 213, 224divcld 10341 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  CC )
226201, 213, 205, 224divne0d 10357 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  =/=  0 )
227182, 150zsubcld 10995 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  e.  ZZ )
228185, 154subge0d 10163 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
0  <_  ( (
( 2  x.  y
)  +  3 )  -  2 )  <->  2  <_  ( ( 2  x.  y
)  +  3 ) ) )
229193, 228mpbird 232 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <_  ( ( ( 2  x.  y )  +  3 )  -  2 ) )
230 elnn0z 10898 . . . . . . . . . . . . . 14  |-  ( ( ( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0  <->  ( ( ( ( 2  x.  y
)  +  3 )  -  2 )  e.  ZZ  /\  0  <_ 
( ( ( 2  x.  y )  +  3 )  -  2 ) ) )
231227, 229, 230sylanbrc 664 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0 )
23247wallispilem3 32052 . . . . . . . . . . . . 13  |-  ( ( ( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0  ->  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) )  e.  RR+ )
233231, 232syl 16 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) )  e.  RR+ )
234233rpcnne0d 11290 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) )  e.  CC  /\  ( I `  (
( ( 2  x.  y )  +  3 )  -  2 ) )  =/=  0 ) )
235225, 226, 234jca31 534 . . . . . . . . . 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 10265 . . . . . . . . . 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 1227 . . . . . . . . 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 2508 . . . . . . . 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 9970 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  ( 3  -  2 ) ) )
24083a1i 11 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
3  -  2 )  =  1 )
241240oveq2d 6312 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 3  -  2 ) )  =  ( ( 2  x.  y )  +  1 ) )
242239, 241eqtrd 2498 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  1 ) )
243242fveq2d 5876 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
244243oveq2d 6312 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  y ) )  /  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
245244oveq2d 6312 . . . . . . . 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 2498 . . . . . . 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 465 . . . . . 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 11142 . . . . . . . . . . . . 13  |-  ( y  e.  NN  <->  y  e.  ( ZZ>= `  1 )
)
249248biimpi 194 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  y  e.  ( ZZ>= `  1 )
)
250 seqp1 12125 . . . . . . . . . . . 12  |-  ( y  e.  ( ZZ>= `  1
)  ->  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) )  =  ( (  seq 1 (  x.  ,  F ) `  y )  x.  ( F `  ( y  +  1 ) ) ) )
251249, 250syl 16 . . . . . . . . . . 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 6304 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
254253oveq1d 6311 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
255253, 254oveq12d 6314 . . . . . . . . . . . . . . 15  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
256253oveq1d 6311 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
257253, 256oveq12d 6314 . . . . . . . . . . . . . . 15  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
258255, 257oveq12d 6314 . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . 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 9641 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR )
261260, 156resubcld 10008 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR )
262 1lt2 10723 . . . . . . . . . . . . . . . . . . 19  |-  1  <  2
263262a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  1  <  2 )
264 nnrp 11254 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  y  e.  RR+ )
265156, 264ltaddrp2d 11311 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  1  <  ( y  +  1 ) )
266154, 157, 263, 265mulgt1d 10502 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  1  <  ( 2  x.  (
y  +  1 ) ) )
267156, 266gtned 9737 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  1 )
268201, 129, 267subne0d 9959 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =/=  0 )
269260, 261, 268redivcld 10393 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  RR )
270178, 185eqeltrd 2545 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  RR )
271178, 224eqnetrd 2750 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =/=  0 )
272260, 270, 271redivcld 10393 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  RR )
273269, 272remulcld 9641 . . . . . . . . . . . . 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 5961 . . . . . . . . . . . 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 6312 . . . . . . . . . . 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 2498 . . . . . . . . . 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 6312 . . . . . . . . 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 6312 . . . . . . . 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 6312 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) ) )
280178oveq2d 6312 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
281279, 280oveq12d 6314 . . . . . . . . . . . 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 6312 . . . . . . . . . . 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 6312 . . . . . . . . . 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 6312 . . . . . . . . 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 11739 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  ( 1 ... y )  ->  w  e.  NN )
286285adantl 466 . . . . . . . . . . . . . . . 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 6304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
2  x.  k )  =  ( 2  x.  w ) )
289288oveq1d 6311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  w )  - 
1 ) )
290288, 289oveq12d 6314 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  -  1 ) ) )
291288oveq1d 6311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  w )  +  1 ) )
292288, 291oveq12d 6314 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  +  1 ) ) )
293290, 292oveq12d 6314 . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . 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 11250 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  RR+
297296a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  2  e.  RR+ )
298 nnrp 11254 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  w  e.  RR+ )
299297, 298rpmulcld 11297 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  NN  ->  (
2  x.  w )  e.  RR+ )
30070a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  2  e.  RR )
301 nnre 10563 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  w  e.  RR )
302300, 301remulcld 9641 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  (
2  x.  w )  e.  RR )
303 1red 9628 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  1  e.  RR )
304302, 303resubcld 10008 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  -  1 )  e.  RR )
305 nnge1 10582 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  1  <_  w )
306 nncn 10564 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  w  e.  CC )
307306mulid2d 9631 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  (
1  x.  w )  =  w )
308303, 300, 298ltmul1d 11318 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  NN  ->  (
1  <  2  <->  ( 1  x.  w )  < 
( 2  x.  w
) ) )
309262, 308mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  (
1  x.  w )  <  ( 2  x.  w ) )
310307, 309eqbrtrrd 4478 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  NN  ->  w  <  ( 2  x.  w
) )
311303, 301, 302, 305, 310lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  1  <  ( 2  x.  w
) )
312303, 302posdifd 10160 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  (
1  <  ( 2  x.  w )  <->  0  <  ( ( 2  x.  w
)  -  1 ) ) )
313311, 312mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  0  <  ( ( 2  x.  w )  -  1 ) )
314304, 313elrpd 11279 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  -  1 )  e.  RR+ )
315299, 314rpdivcld 11298 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  /  ( ( 2  x.  w )  -  1 ) )  e.  RR+ )
316158a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  0  <_  2 )
317298rpge0d 11285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  NN  ->  0  <_  w )
318300, 301, 316, 317mulge0d 10150 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  NN  ->  0  <_  ( 2  x.  w
) )
319302, 318ge0p1rpd 11307 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  +  1 )  e.  RR+ )
320299, 319rpdivcld 11298 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  NN  ->  (
( 2  x.  w
)  /  ( ( 2  x.  w )  +  1 ) )  e.  RR+ )
321315, 320rpmulcld 11297 . . . . . . . . . . . . . . . . . 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 5961 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  NN  ->  ( F `  w )  =  ( ( ( 2  x.  w )  /  ( ( 2  x.  w )  - 
1 ) )  x.  ( ( 2  x.  w )  /  (
( 2  x.  w
)  +  1 ) ) ) )
323322, 321eqeltrd 2545 . . . . . . . . . . . . . . . 16  |-  ( w  e.  NN  ->  ( F `  w )  e.  RR+ )
324286, 323syl 16 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  w  e.  ( 1 ... y ) )  ->  ( F `  w )  e.  RR+ )
325 rpmulcl 11266 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  RR+  /\  z  e.  RR+ )  ->  (
w  x.  z )  e.  RR+ )
326325adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  ( w  e.  RR+  /\  z  e.  RR+ ) )  -> 
( w  x.  z
)  e.  RR+ )
327249, 324, 326seqcl 12130 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (  seq 1 (  x.  ,  F ) `  y
)  e.  RR+ )
328327rpcnne0d 11290 . . . . . . . . . . . . 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 11307 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR+ )
331329, 330rpmulcld 11297 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR+ )
332154, 155, 159, 161mulge0d 10150 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  0  <_  ( 2  x.  y
) )
333183, 332ge0p1rpd 11307 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  RR+ )
334331, 333rpdivcld 11298 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  1 ) )  e.  RR+ )
335329, 264rpmulcld 11297 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  RR+ )
336335, 221rpaddcld 11296 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  RR+ )
337331, 336rpdivcld 11298 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) )  e.  RR+ )
338334, 337rpmulcld 11297 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  RR+ )
339338rpcnne0d 11290 . . . . . . . . . . . . 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 10276 . . . . . . . . . . . . 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 1228 . . . . . . . . . . . 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 2465 . . . . . . . . . . 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 6312 . . . . . . . . . 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 11283 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (  seq 1 (  x.  ,  F ) `  y
)  e.  CC )
346327rpne0d 11286 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (  seq 1 (  x.  ,  F ) `  y
)  =/=  0 )
347345, 346reccld 10334 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  y
) )  e.  CC )
348338rpcnd 11283 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  CC )
349338rpne0d 11286 . . . . . . . . . . 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 10376 . . . . . . . . . 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 2751 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =/=  0 )
352201, 199, 201, 213, 351, 224divmuldivd 10382 . . . . . . . . . . . 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 6312 . . . . . . . . . . 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 9633 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  y )
) )  e.  CC )
355201, 201mulcld 9633 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
356199, 213mulcld 9633 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  3 ) )  e.  CC )
357201, 201, 205, 205mulne0d 10222 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  =/=  0 )
358199, 213, 351, 224mulne0d 10222 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  3 ) )  =/=  0 )
359354, 355, 356, 357, 358divdiv2d 10373 . . . . . . . . . . . 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 10376 . . . . . . . . . . . 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 2498 . . . . . . . . . . 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 10388 . . . . . . . . . . . . 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 2465 . . . . . . . . . . . 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 6312 . . . . . . . . . . 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 2502 . . . . . . . . . 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 2504 . . . . . . . . 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 10804 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
pi  /  2 )  e.  CC )
369368, 347mulcld 9633 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  y )
) )  e.  CC )
370206, 225, 226divcld 10341 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  1 )  /  (
2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  y )  +  3 ) ) )  e.  CC )
371369, 370mulcomd 9634 . . . . . . . . 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 2502 . . . . . . . 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 2498 . . . . . . 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 465 . . . . . 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 2508 . . . . 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 434 . . . 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 10574 . . 3  |-  ( n  e.  NN  ->  (
( I `  (
2  x.  n ) )  /  ( I `
 ( ( 2  x.  n )  +  1 ) ) )  =  ( ( pi 
/  2 )  x.  ( 1  /  (  seq 1 (  x.  ,  F ) `  n
) ) ) )
378377mpteq2ia 4539 . 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 2496 1  |-  G  =  H
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395    e. wcel 1819    =/= wne 2652   class class class wbr 4456    |-> cmpt 4515   ` cfv 5594  (class class class)co 6296   CCcc 9507   RRcr 9508   0cc0 9509   1c1 9510    + caddc 9512    x. cmul 9514    < clt 9645    <_ cle 9646    - cmin 9824    / cdiv 10227   NNcn 10556   2c2 10606   3c3 10607   NN0cn0 10816   ZZcz 10885   ZZ>=cuz 11106   RR+crp 11245   (,)cioo 11554   ...cfz 11697    seqcseq 12110   ^cexp 12169   sincsin 13811   picpi 13814   S.citg 22153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-inf2 8075  ax-cc 8832  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587  ax-addf 9588  ax-mulf 9589
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-iin 4335  df-disj 4428  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6539  df-ofr 6540  df-om 6700  df-1st 6799  df-2nd 6800  df-supp 6918  df-recs 7060  df-rdg 7094  df-1o 7148  df-2o 7149  df-oadd 7152  df-omul 7153  df-er 7329  df-map 7440  df-pm 7441  df-ixp 7489  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fsupp 7848  df-fi 7889  df-sup 7919  df-oi 7953  df-card 8337  df-acn 8340  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-10 10623  df-n0 10817  df-z 10886  df-dec 11001  df-uz 11107  df-q 11208  df-rp 11246  df-xneg 11343  df-xadd 11344  df-xmul 11345  df-ioo 11558  df-ioc 11559  df-ico 11560  df-icc 11561  df-fz 11698  df-fzo 11822  df-fl 11932  df-mod 12000  df-seq 12111  df-exp 12170  df-fac 12357  df-bc 12384  df-hash 12409  df-shft 12912  df-cj 12944  df-re 12945  df-im 12946  df-sqrt 13080  df-abs 13081  df-limsup 13306  df-clim 13323  df-rlim 13324  df-sum 13521  df-ef 13815  df-sin 13817  df-cos 13818  df-pi 13820  df-struct 14646  df-ndx 14647  df-slot 14648  df-base 14649  df-sets 14650  df-ress 14651  df-plusg 14725  df-mulr 14726  df-starv 14727  df-sca 14728  df-vsca 14729  df-ip 14730  df-tset 14731  df-ple 14732  df-ds 14734  df-unif 14735  df-hom 14736  df-cco 14737  df-rest 14840  df-topn 14841  df-0g 14859  df-gsum 14860  df-topgen 14861  df-pt 14862  df-prds 14865  df-xrs 14919  df-qtop 14924  df-imas 14925  df-xps 14927  df-mre 15003  df-mrc 15004  df-acs 15006  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-submnd 16094  df-mulg 16187  df-cntz 16482  df-cmn 16927  df-psmet 18538  df-xmet 18539  df-met 18540  df-bl 18541  df-mopn 18542  df-fbas 18543  df-fg 18544  df-cnfld 18548  df-top 19526  df-bases 19528  df-topon 19529  df-topsp 19530  df-cld 19647  df-ntr 19648  df-cls 19649  df-nei 19726  df-lp 19764  df-perf 19765  df-cn 19855  df-cnp 19856  df-haus 19943  df-cmp 20014  df-tx 20189  df-hmeo 20382  df-fil 20473  df-fm 20565  df-flim 20566  df-flf 20567  df-xms 20949  df-ms 20950  df-tms 20951  df-cncf 21508  df-ovol 22002  df-vol 22003  df-mbf 22154  df-itg1 22155  df-itg2 22156  df-ibl 22157  df-itg 22158  df-0p 22203  df-limc 22396  df-dv 22397
This theorem is referenced by:  wallispilem5  32054
  Copyright terms: Public domain W3C validator