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 ⊢ 𝐹 = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
wallispi.2 ⊢ 𝑊 = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) )
Assertion wallispi 𝑊 ⇝ ( π / 2 )

Proof

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