Metamath Proof Explorer


Theorem wallispi

Description: Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses wallispi.1 F=k2k2k12k2k+1
wallispi.2 W=nseq1×Fn
Assertion wallispi Wπ2

Proof

Step Hyp Ref Expression
1 wallispi.1 F=k2k2k12k2k+1
2 wallispi.2 W=nseq1×Fn
3 nnuz =1
4 1zzd 1
5 eqid n00πsinxndx=n00πsinxndx
6 eqid nn00πsinxndx2nn00πsinxndx2n+1=nn00πsinxndx2nn00πsinxndx2n+1
7 eqid nπ21seq1×Fn=nπ21seq1×Fn
8 eqid n2n+12n=n2n+12n
9 1 5 6 7 8 wallispilem5 nπ21seq1×Fn1
10 9 a1i nπ21seq1×Fn1
11 2cnd 2
12 picn π
13 12 a1i π
14 pire π
15 pipos 0<π
16 14 15 gt0ne0ii π0
17 16 a1i π0
18 11 13 17 divcld 2π
19 nnex V
20 19 mptex n1seq1×FnV
21 20 a1i n1seq1×FnV
22 12 a1i nπ
23 22 halfcld nπ2
24 elnnuz nn1
25 24 biimpi nn1
26 oveq2 k=j2k=2j
27 26 oveq1d k=j2k1=2j1
28 26 27 oveq12d k=j2k2k1=2j2j1
29 26 oveq1d k=j2k+1=2j+1
30 26 29 oveq12d k=j2k2k+1=2j2j+1
31 28 30 oveq12d k=j2k2k12k2k+1=2j2j12j2j+1
32 elfznn j1nj
33 2cnd j2
34 nncn jj
35 33 34 mulcld j2j
36 1cnd j1
37 35 36 subcld j2j1
38 1red j1
39 1t1e1 11=1
40 38 38 remulcld j11
41 2re 2
42 41 a1i j2
43 42 38 remulcld j21
44 nnre jj
45 42 44 remulcld j2j
46 1rp 1+
47 46 a1i j1+
48 1lt2 1<2
49 48 a1i j1<2
50 38 42 47 49 ltmul1dd j11<21
51 0le2 02
52 51 a1i j02
53 nnge1 j1j
54 38 44 42 52 53 lemul2ad j212j
55 40 43 45 50 54 ltletrd j11<2j
56 39 55 eqbrtrrid j1<2j
57 38 56 gtned j2j1
58 35 36 57 subne0d j2j10
59 35 37 58 divcld j2j2j1
60 35 36 addcld j2j+1
61 0red j0
62 45 38 readdcld j2j+1
63 47 rpgt0d j0<1
64 2rp 2+
65 64 a1i j2+
66 nnrp jj+
67 65 66 rpmulcld j2j+
68 38 67 ltaddrp2d j1<2j+1
69 61 38 62 63 68 lttrd j0<2j+1
70 61 69 gtned j2j+10
71 35 60 70 divcld j2j2j+1
72 59 71 mulcld j2j2j12j2j+1
73 32 72 syl j1n2j2j12j2j+1
74 1 31 32 73 fvmptd3 j1nFj=2j2j12j2j+1
75 64 a1i j1n2+
76 32 nnrpd j1nj+
77 75 76 rpmulcld j1n2j+
78 45 38 resubcld j2j1
79 1m1e0 11=0
80 38 45 38 56 ltsub1dd j11<2j1
81 79 80 eqbrtrrid j0<2j1
82 78 81 elrpd j2j1+
83 32 82 syl j1n2j1+
84 77 83 rpdivcld j1n2j2j1+
85 41 a1i j1n2
86 32 nnred j1nj
87 85 86 remulcld j1n2j
88 75 rpge0d j1n02
89 76 rpge0d j1n0j
90 85 86 88 89 mulge0d j1n02j
91 87 90 ge0p1rpd j1n2j+1+
92 77 91 rpdivcld j1n2j2j+1+
93 84 92 rpmulcld j1n2j2j12j2j+1+
94 74 93 eqeltrd j1nFj+
95 94 adantl nj1nFj+
96 rpmulcl j+w+jw+
97 96 adantl nj+w+jw+
98 25 95 97 seqcl nseq1×Fn+
99 98 rpcnd nseq1×Fn
100 98 rpne0d nseq1×Fn0
101 99 100 reccld n1seq1×Fn
102 23 101 mulcld nπ21seq1×Fn
103 7 102 fmpti nπ21seq1×Fn:
104 103 a1i nπ21seq1×Fn:
105 104 ffvelrnda jnπ21seq1×Fnj
106 fveq2 n=jseq1×Fn=seq1×Fj
107 106 eleq1d n=jseq1×Fn+seq1×Fj+
108 107 98 vtoclga jseq1×Fj+
109 108 rpcnd jseq1×Fj
110 108 rpne0d jseq1×Fj0
111 36 109 110 divrecd j1seq1×Fj=11seq1×Fj
112 12 a1i jπ
113 65 rpne0d j20
114 16 a1i jπ0
115 33 112 113 114 divcan6d j2ππ2=1
116 115 eqcomd j1=2ππ2
117 116 oveq1d j11seq1×Fj=2ππ21seq1×Fj
118 33 112 114 divcld j2π
119 112 halfcld jπ2
120 109 110 reccld j1seq1×Fj
121 118 119 120 mulassd j2ππ21seq1×Fj=2ππ21seq1×Fj
122 111 117 121 3eqtrd j1seq1×Fj=2ππ21seq1×Fj
123 eqidd jn1seq1×Fn=n1seq1×Fn
124 106 oveq2d n=j1seq1×Fn=1seq1×Fj
125 124 adantl jn=j1seq1×Fn=1seq1×Fj
126 id jj
127 108 rpreccld j1seq1×Fj+
128 123 125 126 127 fvmptd jn1seq1×Fnj=1seq1×Fj
129 eqidd jnπ21seq1×Fn=nπ21seq1×Fn
130 125 oveq2d jn=jπ21seq1×Fn=π21seq1×Fj
131 119 120 mulcld jπ21seq1×Fj
132 129 130 126 131 fvmptd jnπ21seq1×Fnj=π21seq1×Fj
133 132 oveq2d j2πnπ21seq1×Fnj=2ππ21seq1×Fj
134 122 128 133 3eqtr4d jn1seq1×Fnj=2πnπ21seq1×Fnj
135 134 adantl jn1seq1×Fnj=2πnπ21seq1×Fnj
136 3 4 10 18 21 105 135 climmulc2 n1seq1×Fn2π1
137 2cn 2
138 137 12 16 divcli 2π
139 138 mulid1i 2π1=2π
140 136 139 breqtrdi n1seq1×Fn2π
141 2ne0 20
142 137 12 141 16 divne0i 2π0
143 142 a1i 2π0
144 128 120 eqeltrd jn1seq1×Fnj
145 109 110 recne0d j1seq1×Fj0
146 128 145 eqnetrd jn1seq1×Fnj0
147 nelsn n1seq1×Fnj0¬n1seq1×Fnj0
148 146 147 syl j¬n1seq1×Fnj0
149 144 148 eldifd jn1seq1×Fnj0
150 149 adantl jn1seq1×Fnj0
151 109 110 recrecd j11seq1×Fj=seq1×Fj
152 123 125 126 120 fvmptd jn1seq1×Fnj=1seq1×Fj
153 152 oveq2d j1n1seq1×Fnj=11seq1×Fj
154 106 2 98 fvmpt3 jWj=seq1×Fj
155 151 153 154 3eqtr4rd jWj=1n1seq1×Fnj
156 155 adantl jWj=1n1seq1×Fnj
157 19 mptex nseq1×FnV
158 2 157 eqeltri WV
159 158 a1i WV
160 3 4 140 143 150 156 159 climrec W12π
161 160 mptru W12π
162 recdiv 220ππ012π=π2
163 137 141 12 16 162 mp4an 12π=π2
164 161 163 breqtri Wπ2