Metamath Proof Explorer

Theorem wallispi2

Description: An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to prove Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis wallispi2.1 
|- V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
Assertion wallispi2 
|- V ~~> ( _pi / 2 )

Proof

Step Hyp Ref Expression
1 wallispi2.1 
 |-  V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
2 eqid 
 |-  ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) ) = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )
3 1cnd 
 |-  ( n e. NN -> 1 e. CC )
4 2cnd 
 |-  ( n e. NN -> 2 e. CC )
5 nncn 
 |-  ( n e. NN -> n e. CC )
6 4 5 mulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. CC )
7 6 3 addcld 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) e. CC )
8 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
9 8 biimpi 
 |-  ( n e. NN -> n e. ( ZZ>= ` 1 ) )
10 eqidd 
 |-  ( m e. ( 1 ... n ) -> ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) = ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) )
11 simpr 
 |-  ( ( m e. ( 1 ... n ) /\ k = m ) -> k = m )
12 11 oveq2d 
 |-  ( ( m e. ( 1 ... n ) /\ k = m ) -> ( 2 x. k ) = ( 2 x. m ) )
13 12 oveq1d 
 |-  ( ( m e. ( 1 ... n ) /\ k = m ) -> ( ( 2 x. k ) ^ 4 ) = ( ( 2 x. m ) ^ 4 ) )
14 12 oveq1d 
 |-  ( ( m e. ( 1 ... n ) /\ k = m ) -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. m ) - 1 ) )
15 12 14 oveq12d 
 |-  ( ( m e. ( 1 ... n ) /\ k = m ) -> ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) )
16 15 oveq1d 
 |-  ( ( m e. ( 1 ... n ) /\ k = m ) -> ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) = ( ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) ^ 2 ) )
17 13 16 oveq12d 
 |-  ( ( m e. ( 1 ... n ) /\ k = m ) -> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) = ( ( ( 2 x. m ) ^ 4 ) / ( ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) ^ 2 ) ) )
18 elfznn 
 |-  ( m e. ( 1 ... n ) -> m e. NN )
19 2cnd 
 |-  ( m e. ( 1 ... n ) -> 2 e. CC )
20 18 nncnd 
 |-  ( m e. ( 1 ... n ) -> m e. CC )
21 19 20 mulcld 
 |-  ( m e. ( 1 ... n ) -> ( 2 x. m ) e. CC )
22 4nn0 
 |-  4 e. NN0
23 22 a1i 
 |-  ( m e. ( 1 ... n ) -> 4 e. NN0 )
24 21 23 expcld 
 |-  ( m e. ( 1 ... n ) -> ( ( 2 x. m ) ^ 4 ) e. CC )
25 1cnd 
 |-  ( m e. ( 1 ... n ) -> 1 e. CC )
26 21 25 subcld 
 |-  ( m e. ( 1 ... n ) -> ( ( 2 x. m ) - 1 ) e. CC )
27 21 26 mulcld 
 |-  ( m e. ( 1 ... n ) -> ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) e. CC )
28 27 sqcld 
 |-  ( m e. ( 1 ... n ) -> ( ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) ^ 2 ) e. CC )
29 2ne0 
 |-  2 =/= 0
30 29 a1i 
 |-  ( m e. ( 1 ... n ) -> 2 =/= 0 )
31 18 nnne0d 
 |-  ( m e. ( 1 ... n ) -> m =/= 0 )
32 19 20 30 31 mulne0d 
 |-  ( m e. ( 1 ... n ) -> ( 2 x. m ) =/= 0 )
33 1red 
 |-  ( m e. ( 1 ... n ) -> 1 e. RR )
34 2re 
 |-  2 e. RR
35 34 a1i 
 |-  ( m e. ( 1 ... n ) -> 2 e. RR )
36 35 33 remulcld 
 |-  ( m e. ( 1 ... n ) -> ( 2 x. 1 ) e. RR )
37 18 nnred 
 |-  ( m e. ( 1 ... n ) -> m e. RR )
38 35 37 remulcld 
 |-  ( m e. ( 1 ... n ) -> ( 2 x. m ) e. RR )
39 1lt2 
 |-  1 < 2
40 39 a1i 
 |-  ( m e. ( 1 ... n ) -> 1 < 2 )
41 2t1e2 
 |-  ( 2 x. 1 ) = 2
42 40 41 breqtrrdi 
 |-  ( m e. ( 1 ... n ) -> 1 < ( 2 x. 1 ) )
43 0le2 
 |-  0 <_ 2
44 43 a1i 
 |-  ( m e. ( 1 ... n ) -> 0 <_ 2 )
45 elfzle1 
 |-  ( m e. ( 1 ... n ) -> 1 <_ m )
46 33 37 35 44 45 lemul2ad 
 |-  ( m e. ( 1 ... n ) -> ( 2 x. 1 ) <_ ( 2 x. m ) )
47 33 36 38 42 46 ltletrd 
 |-  ( m e. ( 1 ... n ) -> 1 < ( 2 x. m ) )
48 33 47 gtned 
 |-  ( m e. ( 1 ... n ) -> ( 2 x. m ) =/= 1 )
49 21 25 48 subne0d 
 |-  ( m e. ( 1 ... n ) -> ( ( 2 x. m ) - 1 ) =/= 0 )
50 21 26 32 49 mulne0d 
 |-  ( m e. ( 1 ... n ) -> ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) =/= 0 )
51 2z 
 |-  2 e. ZZ
52 51 a1i 
 |-  ( m e. ( 1 ... n ) -> 2 e. ZZ )
53 27 50 52 expne0d 
 |-  ( m e. ( 1 ... n ) -> ( ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) ^ 2 ) =/= 0 )
54 24 28 53 divcld 
 |-  ( m e. ( 1 ... n ) -> ( ( ( 2 x. m ) ^ 4 ) / ( ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) ^ 2 ) ) e. CC )
55 10 17 18 54 fvmptd 
 |-  ( m e. ( 1 ... n ) -> ( ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ` m ) = ( ( ( 2 x. m ) ^ 4 ) / ( ( ( 2 x. m ) x. ( ( 2 x. m ) - 1 ) ) ^ 2 ) ) )
56 55 54 eqeltrd 
 |-  ( m e. ( 1 ... n ) -> ( ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ` m ) e. CC )
57 56 adantl 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ` m ) e. CC )
58 mulcl 
 |-  ( ( m e. CC /\ w e. CC ) -> ( m x. w ) e. CC )
59 58 adantl 
 |-  ( ( n e. NN /\ ( m e. CC /\ w e. CC ) ) -> ( m x. w ) e. CC )
60 9 57 59 seqcl 
 |-  ( n e. NN -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) e. CC )
61 2nn 
 |-  2 e. NN
62 61 a1i 
 |-  ( n e. NN -> 2 e. NN )
63 id 
 |-  ( n e. NN -> n e. NN )
64 62 63 nnmulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. NN )
65 64 peano2nnd 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) e. NN )
66 65 nnne0d 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) =/= 0 )
67 3 7 60 66 div32d 
 |-  ( n e. NN -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) ) = ( 1 x. ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) / ( ( 2 x. n ) + 1 ) ) ) )
68 60 7 66 divcld 
 |-  ( n e. NN -> ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) / ( ( 2 x. n ) + 1 ) ) e. CC )
69 68 mulid2d 
 |-  ( n e. NN -> ( 1 x. ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) / ( ( 2 x. n ) + 1 ) ) ) = ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) / ( ( 2 x. n ) + 1 ) ) )
70 wallispi2lem2 
 |-  ( n e. NN -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) = ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) )
71 70 oveq1d 
 |-  ( n e. NN -> ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) / ( ( 2 x. n ) + 1 ) ) = ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
72 67 69 71 3eqtrd 
 |-  ( n e. NN -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) ) = ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
73 72 mpteq2ia 
 |-  ( n e. NN |-> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) ) ) = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
74 wallispi2lem1 
 |-  ( n e. NN -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) ) ) ` n ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) ) )
75 74 mpteq2ia 
 |-  ( n e. NN |-> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) ) ) ` n ) ) = ( n e. NN |-> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` n ) ) )
76 73 75 1 3eqtr4ri 
 |-  V = ( n e. NN |-> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) ) ) ` n ) )
77 2 76 wallispi 
 |-  V ~~> ( _pi / 2 )