# 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}=\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)$
wallispi.2 ${⊢}{W}=\left({n}\in ℕ⟼seq1\left(×,{F}\right)\left({n}\right)\right)$
Assertion wallispi ${⊢}{W}⇝\left(\frac{\mathrm{\pi }}{2}\right)$

### Proof

Step Hyp Ref Expression
1 wallispi.1 ${⊢}{F}=\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)$
2 wallispi.2 ${⊢}{W}=\left({n}\in ℕ⟼seq1\left(×,{F}\right)\left({n}\right)\right)$
3 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
4 1zzd ${⊢}\top \to 1\in ℤ$
5 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{n}}d{x}\right)=\left({n}\in {ℕ}_{0}⟼{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{n}}d{x}\right)$
6 eqid ${⊢}\left({n}\in ℕ⟼\frac{\left({n}\in {ℕ}_{0}⟼{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{n}}d{x}\right)\left(2{n}\right)}{\left({n}\in {ℕ}_{0}⟼{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{n}}d{x}\right)\left(2{n}+1\right)}\right)=\left({n}\in ℕ⟼\frac{\left({n}\in {ℕ}_{0}⟼{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{n}}d{x}\right)\left(2{n}\right)}{\left({n}\in {ℕ}_{0}⟼{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{n}}d{x}\right)\left(2{n}+1\right)}\right)$
7 eqid ${⊢}\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)=\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)$
8 eqid ${⊢}\left({n}\in ℕ⟼\frac{2{n}+1}{2{n}}\right)=\left({n}\in ℕ⟼\frac{2{n}+1}{2{n}}\right)$
9 1 5 6 7 8 wallispilem5 ${⊢}\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)⇝1$
10 9 a1i ${⊢}\top \to \left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)⇝1$
11 2cnd ${⊢}\top \to 2\in ℂ$
12 picn ${⊢}\mathrm{\pi }\in ℂ$
13 12 a1i ${⊢}\top \to \mathrm{\pi }\in ℂ$
14 pire ${⊢}\mathrm{\pi }\in ℝ$
15 pipos ${⊢}0<\mathrm{\pi }$
16 14 15 gt0ne0ii ${⊢}\mathrm{\pi }\ne 0$
17 16 a1i ${⊢}\top \to \mathrm{\pi }\ne 0$
18 11 13 17 divcld ${⊢}\top \to \frac{2}{\mathrm{\pi }}\in ℂ$
19 nnex ${⊢}ℕ\in \mathrm{V}$
20 19 mptex ${⊢}\left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\in \mathrm{V}$
21 20 a1i ${⊢}\top \to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\in \mathrm{V}$
22 12 a1i ${⊢}{n}\in ℕ\to \mathrm{\pi }\in ℂ$
23 22 halfcld ${⊢}{n}\in ℕ\to \frac{\mathrm{\pi }}{2}\in ℂ$
24 elnnuz ${⊢}{n}\in ℕ↔{n}\in {ℤ}_{\ge 1}$
25 24 biimpi ${⊢}{n}\in ℕ\to {n}\in {ℤ}_{\ge 1}$
26 oveq2 ${⊢}{k}={j}\to 2{k}=2{j}$
27 26 oveq1d ${⊢}{k}={j}\to 2{k}-1=2{j}-1$
28 26 27 oveq12d ${⊢}{k}={j}\to \frac{2{k}}{2{k}-1}=\frac{2{j}}{2{j}-1}$
29 26 oveq1d ${⊢}{k}={j}\to 2{k}+1=2{j}+1$
30 26 29 oveq12d ${⊢}{k}={j}\to \frac{2{k}}{2{k}+1}=\frac{2{j}}{2{j}+1}$
31 28 30 oveq12d ${⊢}{k}={j}\to \left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)=\left(\frac{2{j}}{2{j}-1}\right)\left(\frac{2{j}}{2{j}+1}\right)$
32 elfznn ${⊢}{j}\in \left(1\dots {n}\right)\to {j}\in ℕ$
33 2cnd ${⊢}{j}\in ℕ\to 2\in ℂ$
34 nncn ${⊢}{j}\in ℕ\to {j}\in ℂ$
35 33 34 mulcld ${⊢}{j}\in ℕ\to 2{j}\in ℂ$
36 1cnd ${⊢}{j}\in ℕ\to 1\in ℂ$
37 35 36 subcld ${⊢}{j}\in ℕ\to 2{j}-1\in ℂ$
38 1red ${⊢}{j}\in ℕ\to 1\in ℝ$
39 1t1e1 ${⊢}1\cdot 1=1$
40 38 38 remulcld ${⊢}{j}\in ℕ\to 1\cdot 1\in ℝ$
41 2re ${⊢}2\in ℝ$
42 41 a1i ${⊢}{j}\in ℕ\to 2\in ℝ$
43 42 38 remulcld ${⊢}{j}\in ℕ\to 2\cdot 1\in ℝ$
44 nnre ${⊢}{j}\in ℕ\to {j}\in ℝ$
45 42 44 remulcld ${⊢}{j}\in ℕ\to 2{j}\in ℝ$
46 1rp ${⊢}1\in {ℝ}^{+}$
47 46 a1i ${⊢}{j}\in ℕ\to 1\in {ℝ}^{+}$
48 1lt2 ${⊢}1<2$
49 48 a1i ${⊢}{j}\in ℕ\to 1<2$
50 38 42 47 49 ltmul1dd ${⊢}{j}\in ℕ\to 1\cdot 1<2\cdot 1$
51 0le2 ${⊢}0\le 2$
52 51 a1i ${⊢}{j}\in ℕ\to 0\le 2$
53 nnge1 ${⊢}{j}\in ℕ\to 1\le {j}$
54 38 44 42 52 53 lemul2ad ${⊢}{j}\in ℕ\to 2\cdot 1\le 2{j}$
55 40 43 45 50 54 ltletrd ${⊢}{j}\in ℕ\to 1\cdot 1<2{j}$
56 39 55 eqbrtrrid ${⊢}{j}\in ℕ\to 1<2{j}$
57 38 56 gtned ${⊢}{j}\in ℕ\to 2{j}\ne 1$
58 35 36 57 subne0d ${⊢}{j}\in ℕ\to 2{j}-1\ne 0$
59 35 37 58 divcld ${⊢}{j}\in ℕ\to \frac{2{j}}{2{j}-1}\in ℂ$
60 35 36 addcld ${⊢}{j}\in ℕ\to 2{j}+1\in ℂ$
61 0red ${⊢}{j}\in ℕ\to 0\in ℝ$
62 45 38 readdcld ${⊢}{j}\in ℕ\to 2{j}+1\in ℝ$
63 47 rpgt0d ${⊢}{j}\in ℕ\to 0<1$
64 2rp ${⊢}2\in {ℝ}^{+}$
65 64 a1i ${⊢}{j}\in ℕ\to 2\in {ℝ}^{+}$
66 nnrp ${⊢}{j}\in ℕ\to {j}\in {ℝ}^{+}$
67 65 66 rpmulcld ${⊢}{j}\in ℕ\to 2{j}\in {ℝ}^{+}$
68 38 67 ltaddrp2d ${⊢}{j}\in ℕ\to 1<2{j}+1$
69 61 38 62 63 68 lttrd ${⊢}{j}\in ℕ\to 0<2{j}+1$
70 61 69 gtned ${⊢}{j}\in ℕ\to 2{j}+1\ne 0$
71 35 60 70 divcld ${⊢}{j}\in ℕ\to \frac{2{j}}{2{j}+1}\in ℂ$
72 59 71 mulcld ${⊢}{j}\in ℕ\to \left(\frac{2{j}}{2{j}-1}\right)\left(\frac{2{j}}{2{j}+1}\right)\in ℂ$
73 32 72 syl ${⊢}{j}\in \left(1\dots {n}\right)\to \left(\frac{2{j}}{2{j}-1}\right)\left(\frac{2{j}}{2{j}+1}\right)\in ℂ$
74 1 31 32 73 fvmptd3 ${⊢}{j}\in \left(1\dots {n}\right)\to {F}\left({j}\right)=\left(\frac{2{j}}{2{j}-1}\right)\left(\frac{2{j}}{2{j}+1}\right)$
75 64 a1i ${⊢}{j}\in \left(1\dots {n}\right)\to 2\in {ℝ}^{+}$
76 32 nnrpd ${⊢}{j}\in \left(1\dots {n}\right)\to {j}\in {ℝ}^{+}$
77 75 76 rpmulcld ${⊢}{j}\in \left(1\dots {n}\right)\to 2{j}\in {ℝ}^{+}$
78 45 38 resubcld ${⊢}{j}\in ℕ\to 2{j}-1\in ℝ$
79 1m1e0 ${⊢}1-1=0$
80 38 45 38 56 ltsub1dd ${⊢}{j}\in ℕ\to 1-1<2{j}-1$
81 79 80 eqbrtrrid ${⊢}{j}\in ℕ\to 0<2{j}-1$
82 78 81 elrpd ${⊢}{j}\in ℕ\to 2{j}-1\in {ℝ}^{+}$
83 32 82 syl ${⊢}{j}\in \left(1\dots {n}\right)\to 2{j}-1\in {ℝ}^{+}$
84 77 83 rpdivcld ${⊢}{j}\in \left(1\dots {n}\right)\to \frac{2{j}}{2{j}-1}\in {ℝ}^{+}$
85 41 a1i ${⊢}{j}\in \left(1\dots {n}\right)\to 2\in ℝ$
86 32 nnred ${⊢}{j}\in \left(1\dots {n}\right)\to {j}\in ℝ$
87 85 86 remulcld ${⊢}{j}\in \left(1\dots {n}\right)\to 2{j}\in ℝ$
88 75 rpge0d ${⊢}{j}\in \left(1\dots {n}\right)\to 0\le 2$
89 76 rpge0d ${⊢}{j}\in \left(1\dots {n}\right)\to 0\le {j}$
90 85 86 88 89 mulge0d ${⊢}{j}\in \left(1\dots {n}\right)\to 0\le 2{j}$
91 87 90 ge0p1rpd ${⊢}{j}\in \left(1\dots {n}\right)\to 2{j}+1\in {ℝ}^{+}$
92 77 91 rpdivcld ${⊢}{j}\in \left(1\dots {n}\right)\to \frac{2{j}}{2{j}+1}\in {ℝ}^{+}$
93 84 92 rpmulcld ${⊢}{j}\in \left(1\dots {n}\right)\to \left(\frac{2{j}}{2{j}-1}\right)\left(\frac{2{j}}{2{j}+1}\right)\in {ℝ}^{+}$
94 74 93 eqeltrd ${⊢}{j}\in \left(1\dots {n}\right)\to {F}\left({j}\right)\in {ℝ}^{+}$
95 94 adantl ${⊢}\left({n}\in ℕ\wedge {j}\in \left(1\dots {n}\right)\right)\to {F}\left({j}\right)\in {ℝ}^{+}$
96 rpmulcl ${⊢}\left({j}\in {ℝ}^{+}\wedge {w}\in {ℝ}^{+}\right)\to {j}{w}\in {ℝ}^{+}$
97 96 adantl ${⊢}\left({n}\in ℕ\wedge \left({j}\in {ℝ}^{+}\wedge {w}\in {ℝ}^{+}\right)\right)\to {j}{w}\in {ℝ}^{+}$
98 25 95 97 seqcl ${⊢}{n}\in ℕ\to seq1\left(×,{F}\right)\left({n}\right)\in {ℝ}^{+}$
99 98 rpcnd ${⊢}{n}\in ℕ\to seq1\left(×,{F}\right)\left({n}\right)\in ℂ$
100 98 rpne0d ${⊢}{n}\in ℕ\to seq1\left(×,{F}\right)\left({n}\right)\ne 0$
101 99 100 reccld ${⊢}{n}\in ℕ\to \frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\in ℂ$
102 23 101 mulcld ${⊢}{n}\in ℕ\to \left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\in ℂ$
103 7 102 fmpti ${⊢}\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right):ℕ⟶ℂ$
104 103 a1i ${⊢}\top \to \left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right):ℕ⟶ℂ$
105 104 ffvelrnda ${⊢}\left(\top \wedge {j}\in ℕ\right)\to \left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)\left({j}\right)\in ℂ$
106 fveq2 ${⊢}{n}={j}\to seq1\left(×,{F}\right)\left({n}\right)=seq1\left(×,{F}\right)\left({j}\right)$
107 106 eleq1d ${⊢}{n}={j}\to \left(seq1\left(×,{F}\right)\left({n}\right)\in {ℝ}^{+}↔seq1\left(×,{F}\right)\left({j}\right)\in {ℝ}^{+}\right)$
108 107 98 vtoclga ${⊢}{j}\in ℕ\to seq1\left(×,{F}\right)\left({j}\right)\in {ℝ}^{+}$
109 108 rpcnd ${⊢}{j}\in ℕ\to seq1\left(×,{F}\right)\left({j}\right)\in ℂ$
110 108 rpne0d ${⊢}{j}\in ℕ\to seq1\left(×,{F}\right)\left({j}\right)\ne 0$
111 36 109 110 divrecd ${⊢}{j}\in ℕ\to \frac{1}{seq1\left(×,{F}\right)\left({j}\right)}=1\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)$
112 12 a1i ${⊢}{j}\in ℕ\to \mathrm{\pi }\in ℂ$
113 65 rpne0d ${⊢}{j}\in ℕ\to 2\ne 0$
114 16 a1i ${⊢}{j}\in ℕ\to \mathrm{\pi }\ne 0$
115 33 112 113 114 divcan6d ${⊢}{j}\in ℕ\to \left(\frac{2}{\mathrm{\pi }}\right)\left(\frac{\mathrm{\pi }}{2}\right)=1$
116 115 eqcomd ${⊢}{j}\in ℕ\to 1=\left(\frac{2}{\mathrm{\pi }}\right)\left(\frac{\mathrm{\pi }}{2}\right)$
117 116 oveq1d ${⊢}{j}\in ℕ\to 1\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)=\left(\frac{2}{\mathrm{\pi }}\right)\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)$
118 33 112 114 divcld ${⊢}{j}\in ℕ\to \frac{2}{\mathrm{\pi }}\in ℂ$
119 112 halfcld ${⊢}{j}\in ℕ\to \frac{\mathrm{\pi }}{2}\in ℂ$
120 109 110 reccld ${⊢}{j}\in ℕ\to \frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\in ℂ$
121 118 119 120 mulassd ${⊢}{j}\in ℕ\to \left(\frac{2}{\mathrm{\pi }}\right)\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)=\left(\frac{2}{\mathrm{\pi }}\right)\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)$
122 111 117 121 3eqtrd ${⊢}{j}\in ℕ\to \frac{1}{seq1\left(×,{F}\right)\left({j}\right)}=\left(\frac{2}{\mathrm{\pi }}\right)\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)$
123 eqidd ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)=\left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)$
124 106 oveq2d ${⊢}{n}={j}\to \frac{1}{seq1\left(×,{F}\right)\left({n}\right)}=\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}$
125 124 adantl ${⊢}\left({j}\in ℕ\wedge {n}={j}\right)\to \frac{1}{seq1\left(×,{F}\right)\left({n}\right)}=\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}$
126 id ${⊢}{j}\in ℕ\to {j}\in ℕ$
127 108 rpreccld ${⊢}{j}\in ℕ\to \frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\in {ℝ}^{+}$
128 123 125 126 127 fvmptd ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)=\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}$
129 eqidd ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)=\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)$
130 125 oveq2d ${⊢}\left({j}\in ℕ\wedge {n}={j}\right)\to \left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)=\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)$
131 119 120 mulcld ${⊢}{j}\in ℕ\to \left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)\in ℂ$
132 129 130 126 131 fvmptd ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)\left({j}\right)=\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)$
133 132 oveq2d ${⊢}{j}\in ℕ\to \left(\frac{2}{\mathrm{\pi }}\right)\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)\left({j}\right)=\left(\frac{2}{\mathrm{\pi }}\right)\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\right)$
134 122 128 133 3eqtr4d ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)=\left(\frac{2}{\mathrm{\pi }}\right)\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)\left({j}\right)$
135 134 adantl ${⊢}\left(\top \wedge {j}\in ℕ\right)\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)=\left(\frac{2}{\mathrm{\pi }}\right)\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)\left({j}\right)$
136 3 4 10 18 21 105 135 climmulc2 ${⊢}\top \to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)⇝\left(\frac{2}{\mathrm{\pi }}\right)\cdot 1$
137 2cn ${⊢}2\in ℂ$
138 137 12 16 divcli ${⊢}\frac{2}{\mathrm{\pi }}\in ℂ$
139 138 mulid1i ${⊢}\left(\frac{2}{\mathrm{\pi }}\right)\cdot 1=\frac{2}{\mathrm{\pi }}$
140 136 139 breqtrdi ${⊢}\top \to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)⇝\left(\frac{2}{\mathrm{\pi }}\right)$
141 2ne0 ${⊢}2\ne 0$
142 137 12 141 16 divne0i ${⊢}\frac{2}{\mathrm{\pi }}\ne 0$
143 142 a1i ${⊢}\top \to \frac{2}{\mathrm{\pi }}\ne 0$
144 128 120 eqeltrd ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)\in ℂ$
145 109 110 recne0d ${⊢}{j}\in ℕ\to \frac{1}{seq1\left(×,{F}\right)\left({j}\right)}\ne 0$
146 128 145 eqnetrd ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)\ne 0$
147 nelsn ${⊢}\left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)\ne 0\to ¬\left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)\in \left\{0\right\}$
148 146 147 syl ${⊢}{j}\in ℕ\to ¬\left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)\in \left\{0\right\}$
149 144 148 eldifd ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$
150 149 adantl ${⊢}\left(\top \wedge {j}\in ℕ\right)\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$
151 109 110 recrecd ${⊢}{j}\in ℕ\to \frac{1}{\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}}=seq1\left(×,{F}\right)\left({j}\right)$
152 123 125 126 120 fvmptd ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)=\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}$
153 152 oveq2d ${⊢}{j}\in ℕ\to \frac{1}{\left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)}=\frac{1}{\frac{1}{seq1\left(×,{F}\right)\left({j}\right)}}$
154 106 2 98 fvmpt3 ${⊢}{j}\in ℕ\to {W}\left({j}\right)=seq1\left(×,{F}\right)\left({j}\right)$
155 151 153 154 3eqtr4rd ${⊢}{j}\in ℕ\to {W}\left({j}\right)=\frac{1}{\left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)}$
156 155 adantl ${⊢}\left(\top \wedge {j}\in ℕ\right)\to {W}\left({j}\right)=\frac{1}{\left({n}\in ℕ⟼\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\left({j}\right)}$
157 19 mptex ${⊢}\left({n}\in ℕ⟼seq1\left(×,{F}\right)\left({n}\right)\right)\in \mathrm{V}$
158 2 157 eqeltri ${⊢}{W}\in \mathrm{V}$
159 158 a1i ${⊢}\top \to {W}\in \mathrm{V}$
160 3 4 140 143 150 156 159 climrec ${⊢}\top \to {W}⇝\left(\frac{1}{\frac{2}{\mathrm{\pi }}}\right)$
161 160 mptru ${⊢}{W}⇝\left(\frac{1}{\frac{2}{\mathrm{\pi }}}\right)$
162 recdiv ${⊢}\left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(\mathrm{\pi }\in ℂ\wedge \mathrm{\pi }\ne 0\right)\right)\to \frac{1}{\frac{2}{\mathrm{\pi }}}=\frac{\mathrm{\pi }}{2}$
163 137 141 12 16 162 mp4an ${⊢}\frac{1}{\frac{2}{\mathrm{\pi }}}=\frac{\mathrm{\pi }}{2}$
164 161 163 breqtri ${⊢}{W}⇝\left(\frac{\mathrm{\pi }}{2}\right)$