| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnuz 12921 | . . . 4
⊢ ℕ =
(ℤ≥‘1) | 
| 2 |  | 1zzd 12648 | . . . 4
⊢ (⊤
→ 1 ∈ ℤ) | 
| 3 |  | wallispi.1 | . . . . . . . 8
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) + 1)))) | 
| 4 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) | 
| 5 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (((𝑛 ∈ ℕ0
↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)‘(2 · 𝑛)) / ((𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)‘((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ (((𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)‘(2 · 𝑛)) / ((𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)‘((2 · 𝑛) + 1)))) | 
| 6 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛)))) | 
| 7 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (((2
· 𝑛) + 1) / (2
· 𝑛))) = (𝑛 ∈ ℕ ↦ (((2
· 𝑛) + 1) / (2
· 𝑛))) | 
| 8 | 3, 4, 5, 6, 7 | wallispilem5 46084 | . . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1 | 
| 9 | 8 | a1i 11 | . . . . . 6
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1) | 
| 10 |  | 2cnd 12344 | . . . . . . 7
⊢ (⊤
→ 2 ∈ ℂ) | 
| 11 |  | picn 26501 | . . . . . . . 8
⊢ π
∈ ℂ | 
| 12 | 11 | a1i 11 | . . . . . . 7
⊢ (⊤
→ π ∈ ℂ) | 
| 13 |  | pire 26500 | . . . . . . . . 9
⊢ π
∈ ℝ | 
| 14 |  | pipos 26502 | . . . . . . . . 9
⊢ 0 <
π | 
| 15 | 13, 14 | gt0ne0ii 11799 | . . . . . . . 8
⊢ π ≠
0 | 
| 16 | 15 | a1i 11 | . . . . . . 7
⊢ (⊤
→ π ≠ 0) | 
| 17 | 10, 12, 16 | divcld 12043 | . . . . . 6
⊢ (⊤
→ (2 / π) ∈ ℂ) | 
| 18 |  | nnex 12272 | . . . . . . . 8
⊢ ℕ
∈ V | 
| 19 | 18 | mptex 7243 | . . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛))) ∈ V | 
| 20 | 19 | a1i 11 | . . . . . 6
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V) | 
| 21 | 11 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → π
∈ ℂ) | 
| 22 | 21 | halfcld 12511 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (π /
2) ∈ ℂ) | 
| 23 |  | elnnuz 12922 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) | 
| 24 | 23 | biimpi 216 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) | 
| 25 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) | 
| 26 | 25 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1)) | 
| 27 | 25, 26 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1))) | 
| 28 | 25 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1)) | 
| 29 | 25, 28 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1))) | 
| 30 | 27, 29 | oveq12d 7449 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2
· 𝑗) / ((2 ·
𝑗) + 1)))) | 
| 31 |  | elfznn 13593 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ) | 
| 32 |  | 2cnd 12344 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 2 ∈
ℂ) | 
| 33 |  | nncn 12274 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) | 
| 34 | 32, 33 | mulcld 11281 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℂ) | 
| 35 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 1 ∈
ℂ) | 
| 36 | 34, 35 | subcld 11620 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) − 1)
∈ ℂ) | 
| 37 |  | 1red 11262 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 1 ∈
ℝ) | 
| 38 |  | 1t1e1 12428 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
· 1) = 1 | 
| 39 | 37, 37 | remulcld 11291 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (1
· 1) ∈ ℝ) | 
| 40 |  | 2re 12340 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℝ | 
| 41 | 40 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 2 ∈
ℝ) | 
| 42 | 41, 37 | remulcld 11291 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (2
· 1) ∈ ℝ) | 
| 43 |  | nnre 12273 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) | 
| 44 | 41, 43 | remulcld 11291 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℝ) | 
| 45 |  | 1rp 13038 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℝ+ | 
| 46 | 45 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 1 ∈
ℝ+) | 
| 47 |  | 1lt2 12437 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 <
2 | 
| 48 | 47 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 1 <
2) | 
| 49 | 37, 41, 46, 48 | ltmul1dd 13132 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (1
· 1) < (2 · 1)) | 
| 50 |  | 0le2 12368 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ≤
2 | 
| 51 | 50 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 0 ≤
2) | 
| 52 |  | nnge1 12294 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 1 ≤
𝑗) | 
| 53 | 37, 43, 41, 51, 52 | lemul2ad 12208 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (2
· 1) ≤ (2 · 𝑗)) | 
| 54 | 39, 42, 44, 49, 53 | ltletrd 11421 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ → (1
· 1) < (2 · 𝑗)) | 
| 55 | 38, 54 | eqbrtrrid 5179 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 1 < (2
· 𝑗)) | 
| 56 | 37, 55 | gtned 11396 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ≠
1) | 
| 57 | 34, 35, 56 | subne0d 11629 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) − 1) ≠
0) | 
| 58 | 34, 36, 57 | divcld 12043 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) / ((2 ·
𝑗) − 1)) ∈
ℂ) | 
| 59 | 34, 35 | addcld 11280 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ∈
ℂ) | 
| 60 |  | 0red 11264 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 0 ∈
ℝ) | 
| 61 | 44, 37 | readdcld 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ∈
ℝ) | 
| 62 | 46 | rpgt0d 13080 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 0 <
1) | 
| 63 |  | 2rp 13039 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℝ+ | 
| 64 | 63 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → 2 ∈
ℝ+) | 
| 65 |  | nnrp 13046 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) | 
| 66 | 64, 65 | rpmulcld 13093 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℝ+) | 
| 67 | 37, 66 | ltaddrp2d 13111 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 1 <
((2 · 𝑗) +
1)) | 
| 68 | 60, 37, 61, 62, 67 | lttrd 11422 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 0 <
((2 · 𝑗) +
1)) | 
| 69 | 60, 68 | gtned 11396 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ≠
0) | 
| 70 | 34, 59, 69 | divcld 12043 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) / ((2 ·
𝑗) + 1)) ∈
ℂ) | 
| 71 | 58, 70 | mulcld 11281 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → (((2
· 𝑗) / ((2 ·
𝑗) − 1)) · ((2
· 𝑗) / ((2 ·
𝑗) + 1))) ∈
ℂ) | 
| 72 | 31, 71 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈
ℂ) | 
| 73 | 3, 30, 31, 72 | fvmptd3 7039 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1)))) | 
| 74 | 63 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...𝑛) → 2 ∈
ℝ+) | 
| 75 | 31 | nnrpd 13075 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+) | 
| 76 | 74, 75 | rpmulcld 13093 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈
ℝ+) | 
| 77 | 44, 37 | resubcld 11691 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) − 1)
∈ ℝ) | 
| 78 |  | 1m1e0 12338 | . . . . . . . . . . . . . . . . . . . 20
⊢ (1
− 1) = 0 | 
| 79 | 37, 44, 37, 55 | ltsub1dd 11875 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (1
− 1) < ((2 · 𝑗) − 1)) | 
| 80 | 78, 79 | eqbrtrrid 5179 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → 0 <
((2 · 𝑗) −
1)) | 
| 81 | 77, 80 | elrpd 13074 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) − 1)
∈ ℝ+) | 
| 82 | 31, 81 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈
ℝ+) | 
| 83 | 76, 82 | rpdivcld 13094 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈
ℝ+) | 
| 84 | 40 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ) | 
| 85 | 31 | nnred 12281 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ) | 
| 86 | 84, 85 | remulcld 11291 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ) | 
| 87 | 74 | rpge0d 13081 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 2) | 
| 88 | 75 | rpge0d 13081 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗) | 
| 89 | 84, 85, 87, 88 | mulge0d 11840 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗)) | 
| 90 | 86, 89 | ge0p1rpd 13107 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈
ℝ+) | 
| 91 | 76, 90 | rpdivcld 13094 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈
ℝ+) | 
| 92 | 83, 91 | rpmulcld 13093 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈
ℝ+) | 
| 93 | 73, 92 | eqeltrd 2841 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) ∈
ℝ+) | 
| 94 | 93 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹‘𝑗) ∈
ℝ+) | 
| 95 |  | rpmulcl 13058 | . . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℝ+
∧ 𝑤 ∈
ℝ+) → (𝑗 · 𝑤) ∈
ℝ+) | 
| 96 | 95 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+
∧ 𝑤 ∈
ℝ+)) → (𝑗 · 𝑤) ∈
ℝ+) | 
| 97 | 24, 94, 96 | seqcl 14063 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (seq1(
· , 𝐹)‘𝑛) ∈
ℝ+) | 
| 98 | 97 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (seq1(
· , 𝐹)‘𝑛) ∈
ℂ) | 
| 99 | 97 | rpne0d 13082 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (seq1(
· , 𝐹)‘𝑛) ≠ 0) | 
| 100 | 98, 99 | reccld 12036 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑛)) ∈ ℂ) | 
| 101 | 22, 100 | mulcld 11281 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ) | 
| 102 | 6, 101 | fmpti 7132 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ | 
| 103 | 102 | a1i 11 | . . . . . . 7
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ) | 
| 104 | 103 | ffvelcdmda 7104 | . . . . . 6
⊢
((⊤ ∧ 𝑗
∈ ℕ) → ((𝑛
∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ) | 
| 105 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗)) | 
| 106 | 105 | eleq1d 2826 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1(
· , 𝐹)‘𝑗) ∈
ℝ+)) | 
| 107 | 106, 97 | vtoclga 3577 | . . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (seq1(
· , 𝐹)‘𝑗) ∈
ℝ+) | 
| 108 | 107 | rpcnd 13079 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (seq1(
· , 𝐹)‘𝑗) ∈
ℂ) | 
| 109 | 107 | rpne0d 13082 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (seq1(
· , 𝐹)‘𝑗) ≠ 0) | 
| 110 | 35, 108, 109 | divrecd 12046 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗)))) | 
| 111 | 11 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → π
∈ ℂ) | 
| 112 | 64 | rpne0d 13082 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 2 ≠
0) | 
| 113 | 15 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → π ≠
0) | 
| 114 | 32, 111, 112, 113 | divcan6d 12062 | . . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((2 /
π) · (π / 2)) = 1) | 
| 115 | 114 | eqcomd 2743 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → 1 = ((2 /
π) · (π / 2))) | 
| 116 | 115 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (1
· (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2))
· (1 / (seq1( · , 𝐹)‘𝑗)))) | 
| 117 | 32, 111, 113 | divcld 12043 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (2 /
π) ∈ ℂ) | 
| 118 | 111 | halfcld 12511 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (π /
2) ∈ ℂ) | 
| 119 | 108, 109 | reccld 12036 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) ∈ ℂ) | 
| 120 | 117, 118,
119 | mulassd 11284 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (((2 /
π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑗))))) | 
| 121 | 110, 116,
120 | 3eqtrd 2781 | . . . . . . . 8
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑗))))) | 
| 122 |  | eqidd 2738 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( ·
, 𝐹)‘𝑛)))) | 
| 123 | 105 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗))) | 
| 124 | 123 | adantl 481 | . . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗))) | 
| 125 |  | id 22 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) | 
| 126 | 107 | rpreccld 13087 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) ∈
ℝ+) | 
| 127 | 122, 124,
125, 126 | fvmptd 7023 | . . . . . . . 8
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗))) | 
| 128 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛))))) | 
| 129 | 124 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑛))) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘𝑗)))) | 
| 130 | 118, 119 | mulcld 11281 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ) | 
| 131 | 128, 129,
125, 130 | fvmptd 7023 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( ·
, 𝐹)‘𝑗)))) | 
| 132 | 131 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑗 ∈ ℕ → ((2 /
π) · ((𝑛 ∈
ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑗))))) | 
| 133 | 121, 127,
132 | 3eqtr4d 2787 | . . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗))) | 
| 134 | 133 | adantl 481 | . . . . . 6
⊢
((⊤ ∧ 𝑗
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗))) | 
| 135 | 1, 2, 9, 17, 20, 104, 134 | climmulc2 15673 | . . . . 5
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) ·
1)) | 
| 136 |  | 2cn 12341 | . . . . . . 7
⊢ 2 ∈
ℂ | 
| 137 | 136, 11, 15 | divcli 12009 | . . . . . 6
⊢ (2 /
π) ∈ ℂ | 
| 138 | 137 | mulridi 11265 | . . . . 5
⊢ ((2 /
π) · 1) = (2 / π) | 
| 139 | 135, 138 | breqtrdi 5184 | . . . 4
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π)) | 
| 140 |  | 2ne0 12370 | . . . . . 6
⊢ 2 ≠
0 | 
| 141 | 136, 11, 140, 15 | divne0i 12015 | . . . . 5
⊢ (2 /
π) ≠ 0 | 
| 142 | 141 | a1i 11 | . . . 4
⊢ (⊤
→ (2 / π) ≠ 0) | 
| 143 | 127, 119 | eqeltrd 2841 | . . . . . 6
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ) | 
| 144 | 108, 109 | recne0d 12037 | . . . . . . . 8
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) ≠ 0) | 
| 145 | 127, 144 | eqnetrd 3008 | . . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0) | 
| 146 |  | nelsn 4666 | . . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( ·
, 𝐹)‘𝑛)))‘𝑗) ∈ {0}) | 
| 147 | 145, 146 | syl 17 | . . . . . 6
⊢ (𝑗 ∈ ℕ → ¬
((𝑛 ∈ ℕ ↦
(1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0}) | 
| 148 | 143, 147 | eldifd 3962 | . . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖
{0})) | 
| 149 | 148 | adantl 481 | . . . 4
⊢
((⊤ ∧ 𝑗
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖
{0})) | 
| 150 | 108, 109 | recrecd 12040 | . . . . . 6
⊢ (𝑗 ∈ ℕ → (1 / (1 /
(seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗)) | 
| 151 | 122, 124,
125, 119 | fvmptd 7023 | . . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗))) | 
| 152 | 151 | oveq2d 7447 | . . . . . 6
⊢ (𝑗 ∈ ℕ → (1 /
((𝑛 ∈ ℕ ↦
(1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗)))) | 
| 153 |  | wallispi.2 | . . . . . . 7
⊢ 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · ,
𝐹)‘𝑛)) | 
| 154 | 105, 153,
97 | fvmpt3 7020 | . . . . . 6
⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (seq1( · , 𝐹)‘𝑗)) | 
| 155 | 150, 152,
154 | 3eqtr4rd 2788 | . . . . 5
⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( ·
, 𝐹)‘𝑛)))‘𝑗))) | 
| 156 | 155 | adantl 481 | . . . 4
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( ·
, 𝐹)‘𝑛)))‘𝑗))) | 
| 157 | 18 | mptex 7243 | . . . . . 6
⊢ (𝑛 ∈ ℕ ↦ (seq1(
· , 𝐹)‘𝑛)) ∈ V | 
| 158 | 153, 157 | eqeltri 2837 | . . . . 5
⊢ 𝑊 ∈ V | 
| 159 | 158 | a1i 11 | . . . 4
⊢ (⊤
→ 𝑊 ∈
V) | 
| 160 | 1, 2, 139, 142, 149, 156, 159 | climrec 45618 | . . 3
⊢ (⊤
→ 𝑊 ⇝ (1 / (2 /
π))) | 
| 161 | 160 | mptru 1547 | . 2
⊢ 𝑊 ⇝ (1 / (2 /
π)) | 
| 162 |  | recdiv 11973 | . . 3
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0))
→ (1 / (2 / π)) = (π / 2)) | 
| 163 | 136, 140,
11, 15, 162 | mp4an 693 | . 2
⊢ (1 / (2 /
π)) = (π / 2) | 
| 164 | 161, 163 | breqtri 5168 | 1
⊢ 𝑊 ⇝ (π /
2) |