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

Theorem wallispilem4 37749
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 6309 . . . . . . 7  |-  ( x  =  1  ->  (
2  x.  x )  =  ( 2  x.  1 ) )
21fveq2d 5881 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  1 ) ) )
31oveq1d 6316 . . . . . . 7  |-  ( x  =  1  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
43fveq2d 5881 . . . . . 6  |-  ( x  =  1  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  1 )  +  1 ) ) )
52, 4oveq12d 6319 . . . . 5  |-  ( x  =  1  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  1 ) )  / 
( I `  (
( 2  x.  1 )  +  1 ) ) ) )
6 fveq2 5877 . . . . . . 7  |-  ( x  =  1  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  1
) )
76oveq2d 6317 . . . . . 6  |-  ( x  =  1  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
87oveq2d 6317 . . . . 5  |-  ( x  =  1  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  1 )
) ) )
95, 8eqeq12d 2444 . . . 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 6309 . . . . . . 7  |-  ( x  =  y  ->  (
2  x.  x )  =  ( 2  x.  y ) )
1110fveq2d 5881 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  y ) ) )
1210oveq1d 6316 . . . . . . 7  |-  ( x  =  y  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  y )  +  1 ) )
1312fveq2d 5881 . . . . . 6  |-  ( x  =  y  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
1411, 13oveq12d 6319 . . . . 5  |-  ( x  =  y  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
15 fveq2 5877 . . . . . . 7  |-  ( x  =  y  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  y
) )
1615oveq2d 6317 . . . . . 6  |-  ( x  =  y  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  y
) ) )
1716oveq2d 6317 . . . . 5  |-  ( x  =  y  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  y )
) ) )
1814, 17eqeq12d 2444 . . . 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 6309 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
2  x.  x )  =  ( 2  x.  ( y  +  1 ) ) )
2019fveq2d 5881 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  ( y  +  1 ) ) ) )
2119oveq1d 6316 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
2221fveq2d 5881 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
2320, 22oveq12d 6319 . . . . 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 5877 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) ) )
2524oveq2d 6317 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  (
y  +  1 ) ) ) )
2625oveq2d 6317 . . . . 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 2444 . . . 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 6309 . . . . . . 7  |-  ( x  =  n  ->  (
2  x.  x )  =  ( 2  x.  n ) )
2928fveq2d 5881 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( 2  x.  x ) )  =  ( I `  (
2  x.  n ) ) )
3028oveq1d 6316 . . . . . . 7  |-  ( x  =  n  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  n )  +  1 ) )
3130fveq2d 5881 . . . . . 6  |-  ( x  =  n  ->  (
I `  ( (
2  x.  x )  +  1 ) )  =  ( I `  ( ( 2  x.  n )  +  1 ) ) )
3229, 31oveq12d 6319 . . . . 5  |-  ( x  =  n  ->  (
( I `  (
2  x.  x ) )  /  ( I `
 ( ( 2  x.  x )  +  1 ) ) )  =  ( ( I `
 ( 2  x.  n ) )  / 
( I `  (
( 2  x.  n
)  +  1 ) ) ) )
33 fveq2 5877 . . . . . . 7  |-  ( x  =  n  ->  (  seq 1 (  x.  ,  F ) `  x
)  =  (  seq 1 (  x.  ,  F ) `  n
) )
3433oveq2d 6317 . . . . . 6  |-  ( x  =  n  ->  (
1  /  (  seq 1 (  x.  ,  F ) `  x
) )  =  ( 1  /  (  seq 1 (  x.  ,  F ) `  n
) ) )
3534oveq2d 6317 . . . . 5  |-  ( x  =  n  ->  (
( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  x )
) )  =  ( ( pi  /  2
)  x.  ( 1  /  (  seq 1
(  x.  ,  F
) `  n )
) ) )
3632, 35eqeq12d 2444 . . . 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 5880 . . . . . 6  |-  ( I `
 ( 2  x.  1 ) )  =  ( I `  2
)
3937oveq1i 6311 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
40 2p1e3 10733 . . . . . . . 8  |-  ( 2  +  1 )  =  3
4139, 40eqtri 2451 . . . . . . 7  |-  ( ( 2  x.  1 )  +  1 )  =  3
4241fveq2i 5880 . . . . . 6  |-  ( I `
 ( ( 2  x.  1 )  +  1 ) )  =  ( I `  3
)
4338, 42oveq12i 6313 . . . . 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 37747 . . . . . . . . 9  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
2  e.  ( ZZ>= ` 
2 )  ->  (
I `  2 )  =  ( ( ( 2  -  1 )  /  2 )  x.  ( I `  (
2  -  2 ) ) ) ) )
4948simp3i 1016 . . . . . . . 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 6311 . . . . . . . 8  |-  ( ( 2  -  1 )  /  2 )  =  ( 1  /  2
)
53 2cn 10680 . . . . . . . . . . 11  |-  2  e.  CC
5453subidi 9945 . . . . . . . . . 10  |-  ( 2  -  2 )  =  0
5554fveq2i 5880 . . . . . . . . 9  |-  ( I `
 ( 2  -  2 ) )  =  ( I `  0
)
5648simp1i 1014 . . . . . . . . 9  |-  ( I `
 0 )  =  pi
5755, 56eqtri 2451 . . . . . . . 8  |-  ( I `
 ( 2  -  2 ) )  =  pi
5852, 57oveq12i 6313 . . . . . . 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 23400 . . . . . . . . 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 1360 . . . . . . . 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 2451 . . . . . . 7  |-  ( ( 1  /  2 )  x.  pi )  =  ( pi  /  2
)
6850, 58, 673eqtri 2455 . . . . . 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 1187 . . . . . . . 8  |-  3  e.  ( ZZ>= `  2 )
7647wallispilem2 37747 . . . . . . . . 9  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
3  e.  ( ZZ>= ` 
2 )  ->  (
I `  3 )  =  ( ( ( 3  -  1 )  /  3 )  x.  ( I `  (
3  -  2 ) ) ) ) )
7776simp3i 1016 . . . . . . . 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 2435 . . . . . . . . 9  |-  2  =  ( 3  -  1 )
8180oveq1i 6311 . . . . . . . 8  |-  ( 2  /  3 )  =  ( ( 3  -  1 )  /  3
)
82 3cn 10684 . . . . . . . . . . 11  |-  3  e.  CC
8382, 53, 59, 40subaddrii 9964 . . . . . . . . . 10  |-  ( 3  -  2 )  =  1
8483fveq2i 5880 . . . . . . . . 9  |-  ( I `
 ( 3  -  2 ) )  =  ( I `  1
)
8548simp2i 1015 . . . . . . . . 9  |-  ( I `
 1 )  =  2
8684, 85eqtr2i 2452 . . . . . . . 8  |-  2  =  ( I `  ( 3  -  2 ) )
8781, 86oveq12i 6313 . . . . . . 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 2457 . . . . . 6  |-  ( I `
 3 )  =  ( 2  x.  (
2  /  3 ) )
9268, 91oveq12i 6313 . . . . 5  |-  ( ( I `  2 )  /  ( I ` 
3 ) )  =  ( ( pi  / 
2 )  /  (
2  x.  ( 2  /  3 ) ) )
93 1z 10967 . . . . . . . . 9  |-  1  e.  ZZ
94 seq1 12225 . . . . . . . . 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 6309 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
9897, 37syl6eq 2479 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
2  x.  k )  =  2 )
9997oveq1d 6316 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
10037oveq1i 6311 . . . . . . . . . . . . . . 15  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
101100, 51eqtri 2451 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  1 )  -  1 )  =  1
10299, 101syl6eq 2479 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  1 )
10398, 102oveq12d 6319 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( 2  / 
1 ) )
10453div1i 10335 . . . . . . . . . . . 12  |-  ( 2  /  1 )  =  2
105103, 104syl6eq 2479 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  2 )
10698oveq1d 6316 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  ( 2  +  1 ) )
107106, 40syl6eq 2479 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  3 )
10898, 107oveq12d 6319 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( 2  / 
3 ) )
109105, 108oveq12d 6319 . . . . . . . . . 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 6329 . . . . . . . . . 10  |-  ( 2  x.  ( 2  / 
3 ) )  e. 
_V
112109, 110, 111fvmpt 5960 . . . . . . . . 9  |-  ( 1  e.  NN  ->  ( F `  1 )  =  ( 2  x.  ( 2  /  3
) ) )
11396, 112ax-mp 5 . . . . . . . 8  |-  ( F `
 1 )  =  ( 2  x.  (
2  /  3 ) )
11495, 113eqtr2i 2452 . . . . . . 7  |-  ( 2  x.  ( 2  / 
3 ) )  =  (  seq 1 (  x.  ,  F ) `
 1 )
115114oveq2i 6312 . . . . . 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 2506 . . . . . . . 8  |-  ( F `
 1 )  e.  CC
11895, 117eqeltri 2506 . . . . . . 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 2721 . . . . . . 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 2451 . . . . 5  |-  ( ( pi  /  2 )  /  ( 2  x.  ( 2  /  3
) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
12443, 92, 1233eqtri 2455 . . . 4  |-  ( ( I `  ( 2  x.  1 ) )  /  ( I `  ( ( 2  x.  1 )  +  1 ) ) )  =  ( ( pi  / 
2 )  x.  (
1  /  (  seq 1 (  x.  ,  F ) `  1
) ) )
125 oveq2 6309 . . . . . . 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 467 . . . . . 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 6317 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
133130, 132eqtrd 2463 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
134133oveq1d 6316 . . . . . . . . . . . . 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 6317 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  y )  +  1 ) )
139134, 136, 1383eqtrd 2467 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  1 ) )
140139oveq1d 6316 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 )  /  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( 2  x.  y )  +  1 )  / 
( 2  x.  (
y  +  1 ) ) ) )
141140oveq1d 6316 . . . . . . . . . 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 6317 . . . . . . . . . . . . 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 2473 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  1 )  =  ( 2  x.  ( y  +  1 ) ) )
147146oveq1d 6316 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  y )  +  3 )  -  1 )  /  ( ( 2  x.  y )  +  3 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
148147oveq1d 6316 . . . . . . . . . 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 6319 . . . . . . . . 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 213 . . . . . . . . . . . . . 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 668 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  ( ZZ>= `  2
) )
16747, 166itgsinexp 37650 . . . . . . . . . . 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 6316 . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  2 )  =  ( 2  x.  y ) )
171170fveq2d 5881 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
I `  ( (
2  x.  ( y  +  1 ) )  -  2 ) )  =  ( I `  ( 2  x.  y
) ) )
172171oveq2d 6317 . . . . . . . . . . 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 2463 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( 2  x.  ( y  +  1 ) ) )  =  ( ( ( ( 2  x.  ( y  +  1 ) )  -  1 )  / 
( 2  x.  (
y  +  1 ) ) )  x.  (
I `  ( 2  x.  y ) ) ) )
174133oveq1d 6316 . . . . . . . . . . . . 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 6317 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  +  1 ) )  =  ( ( 2  x.  y )  +  3 ) )
178174, 175, 1773eqtrd 2467 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =  ( ( 2  x.  y )  +  3 ) )
179178fveq2d 5881 . . . . . . . . . . 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 214 . . . . . . . . . . . . . 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 668 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  3 )  e.  ( ZZ>= `  2
) )
19647, 195itgsinexp 37650 . . . . . . . . . . 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 2463 . . . . . . . . . 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 6319 . . . . . . . . 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 37748 . . . . . . . . . . . 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 540 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
3  e.  RR  /\  0  <  3 ) )
220 elrp 11304 . . . . . . . . . . . . . . . 16  |-  ( 3  e.  RR+  <->  ( 3  e.  RR  /\  0  <  3 ) )
221219, 220sylibr 215 . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  e.  NN0 )
23247wallispilem3 37748 . . . . . . . . . . . . 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 536 . . . . . . . . . 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 1263 . . . . . . . . 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 2473 . . . . . . . 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 6317 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 3  -  2 ) )  =  ( ( 2  x.  y )  +  1 ) )
242239, 241eqtrd 2463 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  3 )  -  2 )  =  ( ( 2  x.  y )  +  1 ) )
243242fveq2d 5881 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
I `  ( (
( 2  x.  y
)  +  3 )  -  2 ) )  =  ( I `  ( ( 2  x.  y )  +  1 ) ) )
244243oveq2d 6317 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( I `  (
2  x.  y ) )  /  ( I `
 ( ( ( 2  x.  y )  +  3 )  - 
2 ) ) )  =  ( ( I `
 ( 2  x.  y ) )  / 
( I `  (
( 2  x.  y
)  +  1 ) ) ) )
245244oveq2d 6317 . . . . . . . 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 2463 . . . . . . 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 466 . . . . . 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 197 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  y  e.  ( ZZ>= `  1 )
)
250 seqp1 12227 . . . . . . . . . . . 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 6309 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
254253oveq1d 6316 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
255253, 254oveq12d 6319 . . . . . . . . . . . . . . 15  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
256253oveq1d 6316 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
257253, 256oveq12d 6319 . . . . . . . . . . . . . . 15  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
258255, 257oveq12d 6319 . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . 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 2510 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  RR )
271178, 224eqnetrd 2717 . . . . . . . . . . . . . . 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 5966 . . . . . . . . . . . 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 6317 . . . . . . . . . . 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 2463 . . . . . . . . . 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 6317 . . . . . . . . 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 6317 . . . . . . . 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 6317 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  1 ) ) )
280178oveq2d 6317 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  y )  +  3 ) ) )
281279, 280oveq12d 6319 . . . . . . . . . . . 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 6317 . . . . . . . . . . 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 6317 . . . . . . . . . 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 6317 . . . . . . . . 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 467 . . . . . . . . . . . . . . . 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 6309 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
2  x.  k )  =  ( 2  x.  w ) )
289288oveq1d 6316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  w )  - 
1 ) )
290288, 289oveq12d 6319 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  -  1 ) ) )
291288oveq1d 6316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  w  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  w )  +  1 ) )
292288, 291oveq12d 6319 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  w  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  w )  / 
( ( 2  x.  w )  +  1 ) ) )
293290, 292oveq12d 6319 . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  NN  ->  (
1  x.  w )  <  ( 2  x.  w ) )
310307, 309eqbrtrrd 4443 . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . 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 5966 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  NN  ->  ( F `  w )  =  ( ( ( 2  x.  w )  /  ( ( 2  x.  w )  - 
1 ) )  x.  ( ( 2  x.  w )  /  (
( 2  x.  w
)  +  1 ) ) ) )
323322, 321eqeltrd 2510 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  ( w  e.  RR+  /\  z  e.  RR+ ) )  -> 
( w  x.  z
)  e.  RR+ )
327249, 324, 326seqcl 12232 . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . 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 2430 . . . . . . . . . . 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 6317 . . . . . . . . . 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 2718 . . . . . . . . . . . . 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 6317 . . . . . . . . . . 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 2463 . . . . . . . . . . 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 2430 . . . . . . . . . . . 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 6317 . . . . . . . . . . 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 2467 . . . . . . . . . 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 2469 . . . . . . . . 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 2467 . . . . . . . 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 2463 . . . . . . 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 466 . . . . . 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 2473 . . . . 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 435 . . . 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 4503 . 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 2461 1  |-  G  =  H
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1868    =/= wne 2618   class class class wbr 4420    |-> cmpt 4479   ` cfv 5597  (class class class)co 6301   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 12212   ^cexp 12271   sincsin 14103   picpi 14106   S.citg 22562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  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 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-disj 4392  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-ofr 6542  df-om 6703  df-1st 6803  df-2nd 6804  df-supp 6922  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-2o 7187  df-oadd 7190  df-omul 7191  df-er 7367  df-map 7478  df-pm 7479  df-ixp 7527  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-fsupp 7886  df-fi 7927  df-sup 7958  df-inf 7959  df-oi 8027  df-card 8374  df-acn 8377  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 12027  df-mod 12096  df-seq 12213  df-exp 12272  df-fac 12459  df-bc 12487  df-hash 12515  df-shft 13118  df-cj 13150  df-re 13151  df-im 13152  df-sqrt 13286  df-abs 13287  df-limsup 13513  df-clim 13539  df-rlim 13540  df-sum 13740  df-ef 14108  df-sin 14110  df-cos 14111  df-pi 14113  df-struct 15110  df-ndx 15111  df-slot 15112  df-base 15113  df-sets 15114  df-ress 15115  df-plusg 15190  df-mulr 15191  df-starv 15192  df-sca 15193  df-vsca 15194  df-ip 15195  df-tset 15196  df-ple 15197  df-ds 15199  df-unif 15200  df-hom 15201  df-cco 15202  df-rest 15308  df-topn 15309  df-0g 15327  df-gsum 15328  df-topgen 15329  df-pt 15330  df-prds 15333  df-xrs 15387  df-qtop 15393  df-imas 15394  df-xps 15397  df-mre 15479  df-mrc 15480  df-acs 15482  df-mgm 16475  df-sgrp 16514  df-mnd 16524  df-submnd 16570  df-mulg 16663  df-cntz 16958  df-cmn 17419  df-psmet 18949  df-xmet 18950  df-met 18951  df-bl 18952  df-mopn 18953  df-fbas 18954  df-fg 18955  df-cnfld 18958  df-top 19907  df-bases 19908  df-topon 19909  df-topsp 19910  df-cld 20020  df-ntr 20021  df-cls 20022  df-nei 20100  df-lp 20138  df-perf 20139  df-cn 20229  df-cnp 20230  df-haus 20317  df-cmp 20388  df-tx 20563  df-hmeo 20756  df-fil 20847  df-fm 20939  df-flim 20940  df-flf 20941  df-xms 21321  df-ms 21322  df-tms 21323  df-cncf 21896  df-ovol 22402  df-vol 22404  df-mbf 22563  df-itg1 22564  df-itg2 22565  df-ibl 22566  df-itg 22567  df-0p 22614  df-limc 22807  df-dv 22808
This theorem is referenced by:  wallispilem5  37750
  Copyright terms: Public domain W3C validator