# 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 )