Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . . 4
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | wallispi.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) + 1)))) |
4 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) |
5 | | eqid 2622 |
. . . . . . . 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 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛)))) |
7 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (((2
· 𝑛) + 1) / (2
· 𝑛))) = (𝑛 ∈ ℕ ↦ (((2
· 𝑛) + 1) / (2
· 𝑛))) |
8 | 3, 4, 5, 6, 7 | wallispilem5 40286 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1 |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1) |
10 | | 2cnd 11093 |
. . . . . . 7
⊢ (⊤
→ 2 ∈ ℂ) |
11 | | picn 24211 |
. . . . . . . 8
⊢ π
∈ ℂ |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ π ∈ ℂ) |
13 | | pire 24210 |
. . . . . . . . 9
⊢ π
∈ ℝ |
14 | | pipos 24212 |
. . . . . . . . 9
⊢ 0 <
π |
15 | 13, 14 | gt0ne0ii 10564 |
. . . . . . . 8
⊢ π ≠
0 |
16 | 15 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ π ≠ 0) |
17 | 10, 12, 16 | divcld 10801 |
. . . . . 6
⊢ (⊤
→ (2 / π) ∈ ℂ) |
18 | | nnex 11026 |
. . . . . . . 8
⊢ ℕ
∈ V |
19 | 18 | mptex 6486 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛))) ∈ V |
20 | 19 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V) |
21 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → π
∈ ℂ) |
22 | 21 | halfcld 11277 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (π /
2) ∈ ℂ) |
23 | | elnnuz 11724 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
24 | 23 | biimpi 206 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) |
25 | 3 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) +
1))))) |
26 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) |
27 | 26 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1)) |
28 | 26, 27 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1))) |
29 | 26 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1)) |
30 | 26, 29 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1))) |
31 | 28, 30 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2
· 𝑗) / ((2 ·
𝑗) + 1)))) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (1...𝑛) ∧ 𝑘 = 𝑗) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2
· 𝑗) / ((2 ·
𝑗) + 1)))) |
33 | | elfznn 12370 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ) |
34 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 2 ∈
ℂ) |
35 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
36 | 34, 35 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℂ) |
37 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 1 ∈
ℂ) |
38 | 36, 37 | subcld 10392 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) − 1)
∈ ℂ) |
39 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 1 ∈
ℝ) |
40 | | 1t1e1 11175 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
· 1) = 1 |
41 | 39, 39 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (1
· 1) ∈ ℝ) |
42 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℝ |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 2 ∈
ℝ) |
44 | 43, 39 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (2
· 1) ∈ ℝ) |
45 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
46 | 43, 45 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℝ) |
47 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℝ+ |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 1 ∈
ℝ+) |
49 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 <
2 |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 1 <
2) |
51 | 39, 43, 48, 50 | ltmul1dd 11927 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (1
· 1) < (2 · 1)) |
52 | | 0le2 11111 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ≤
2 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 0 ≤
2) |
54 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 1 ≤
𝑗) |
55 | 39, 45, 43, 53, 54 | lemul2ad 10964 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → (2
· 1) ≤ (2 · 𝑗)) |
56 | 41, 44, 46, 51, 55 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ → (1
· 1) < (2 · 𝑗)) |
57 | 40, 56 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 1 < (2
· 𝑗)) |
58 | 39, 57 | gtned 10172 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ≠
1) |
59 | 36, 37, 58 | subne0d 10401 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) − 1) ≠
0) |
60 | 36, 38, 59 | divcld 10801 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) / ((2 ·
𝑗) − 1)) ∈
ℂ) |
61 | 36, 37 | addcld 10059 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ∈
ℂ) |
62 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 0 ∈
ℝ) |
63 | 46, 39 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ∈
ℝ) |
64 | 48 | rpgt0d 11875 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 0 <
1) |
65 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℝ+ |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → 2 ∈
ℝ+) |
67 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) |
68 | 66, 67 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℝ+) |
69 | 39, 68 | ltaddrp2d 11906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 1 <
((2 · 𝑗) +
1)) |
70 | 62, 39, 63, 64, 69 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → 0 <
((2 · 𝑗) +
1)) |
71 | 62, 70 | gtned 10172 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ≠
0) |
72 | 36, 61, 71 | divcld 10801 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) / ((2 ·
𝑗) + 1)) ∈
ℂ) |
73 | 60, 72 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → (((2
· 𝑗) / ((2 ·
𝑗) − 1)) · ((2
· 𝑗) / ((2 ·
𝑗) + 1))) ∈
ℂ) |
74 | 33, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈
ℂ) |
75 | 25, 32, 33, 74 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1)))) |
76 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...𝑛) → 2 ∈
ℝ+) |
77 | 33 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+) |
78 | 76, 77 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈
ℝ+) |
79 | 46, 39 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) − 1)
∈ ℝ) |
80 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1
− 1) = 0 |
81 | 39, 46, 39, 57 | ltsub1dd 10639 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → (1
− 1) < ((2 · 𝑗) − 1)) |
82 | 80, 81 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → 0 <
((2 · 𝑗) −
1)) |
83 | 79, 82 | elrpd 11869 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) − 1)
∈ ℝ+) |
84 | 33, 83 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈
ℝ+) |
85 | 78, 84 | rpdivcld 11889 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈
ℝ+) |
86 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ) |
87 | 33 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ) |
88 | 86, 87 | remulcld 10070 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ) |
89 | 76 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 2) |
90 | 77 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗) |
91 | 86, 87, 89, 90 | mulge0d 10604 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗)) |
92 | 88, 91 | ge0p1rpd 11902 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈
ℝ+) |
93 | 78, 92 | rpdivcld 11889 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈
ℝ+) |
94 | 85, 93 | rpmulcld 11888 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈
ℝ+) |
95 | 75, 94 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) ∈
ℝ+) |
96 | 95 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹‘𝑗) ∈
ℝ+) |
97 | | rpmulcl 11855 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℝ+
∧ 𝑤 ∈
ℝ+) → (𝑗 · 𝑤) ∈
ℝ+) |
98 | 97 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+
∧ 𝑤 ∈
ℝ+)) → (𝑗 · 𝑤) ∈
ℝ+) |
99 | 24, 96, 98 | seqcl 12821 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (seq1(
· , 𝐹)‘𝑛) ∈
ℝ+) |
100 | 99 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (seq1(
· , 𝐹)‘𝑛) ∈
ℂ) |
101 | 99 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (seq1(
· , 𝐹)‘𝑛) ≠ 0) |
102 | 100, 101 | reccld 10794 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑛)) ∈ ℂ) |
103 | 22, 102 | mulcld 10060 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ) |
104 | 6, 103 | fmpti 6383 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ |
105 | 104 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ) |
106 | 105 | ffvelrnda 6359 |
. . . . . 6
⊢
((⊤ ∧ 𝑗
∈ ℕ) → ((𝑛
∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ) |
107 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗)) |
108 | 107 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1(
· , 𝐹)‘𝑗) ∈
ℝ+)) |
109 | 108, 99 | vtoclga 3272 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (seq1(
· , 𝐹)‘𝑗) ∈
ℝ+) |
110 | 109 | rpcnd 11874 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (seq1(
· , 𝐹)‘𝑗) ∈
ℂ) |
111 | 109 | rpne0d 11877 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (seq1(
· , 𝐹)‘𝑗) ≠ 0) |
112 | 37, 110, 111 | divrecd 10804 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗)))) |
113 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → π
∈ ℂ) |
114 | 66 | rpne0d 11877 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 2 ≠
0) |
115 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → π ≠
0) |
116 | 34, 113, 114, 115 | divcan6d 10820 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((2 /
π) · (π / 2)) = 1) |
117 | 116 | eqcomd 2628 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → 1 = ((2 /
π) · (π / 2))) |
118 | 117 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (1
· (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2))
· (1 / (seq1( · , 𝐹)‘𝑗)))) |
119 | 34, 113, 115 | divcld 10801 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (2 /
π) ∈ ℂ) |
120 | 113 | halfcld 11277 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (π /
2) ∈ ℂ) |
121 | 110, 111 | reccld 10794 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) ∈ ℂ) |
122 | 119, 120,
121 | mulassd 10063 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (((2 /
π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑗))))) |
123 | 112, 118,
122 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑗))))) |
124 | | eqidd 2623 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( ·
, 𝐹)‘𝑛)))) |
125 | 107 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗))) |
126 | 125 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗))) |
127 | | id 22 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
128 | 109 | rpreccld 11882 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) ∈
ℝ+) |
129 | 124, 126,
127, 128 | fvmptd 6288 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗))) |
130 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛))))) |
131 | 126 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑛))) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘𝑗)))) |
132 | 120, 121 | mulcld 10060 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ) |
133 | 130, 131,
127, 132 | fvmptd 6288 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( ·
, 𝐹)‘𝑗)))) |
134 | 133 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → ((2 /
π) · ((𝑛 ∈
ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑗))))) |
135 | 123, 129,
134 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗))) |
136 | 135 | adantl 482 |
. . . . . 6
⊢
((⊤ ∧ 𝑗
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗))) |
137 | 1, 2, 9, 17, 20, 106, 136 | climmulc2 14367 |
. . . . 5
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) ·
1)) |
138 | | 2cn 11091 |
. . . . . . 7
⊢ 2 ∈
ℂ |
139 | 138, 11, 15 | divcli 10767 |
. . . . . 6
⊢ (2 /
π) ∈ ℂ |
140 | 139 | mulid1i 10042 |
. . . . 5
⊢ ((2 /
π) · 1) = (2 / π) |
141 | 137, 140 | syl6breq 4694 |
. . . 4
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π)) |
142 | | 2ne0 11113 |
. . . . . 6
⊢ 2 ≠
0 |
143 | 138, 11, 142, 15 | divne0i 10773 |
. . . . 5
⊢ (2 /
π) ≠ 0 |
144 | 143 | a1i 11 |
. . . 4
⊢ (⊤
→ (2 / π) ≠ 0) |
145 | 129, 121 | eqeltrd 2701 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ) |
146 | 110, 111 | recne0d 10795 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑗)) ≠ 0) |
147 | 129, 146 | eqnetrd 2861 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0) |
148 | | nelsn 4212 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( ·
, 𝐹)‘𝑛)))‘𝑗) ∈ {0}) |
149 | 147, 148 | syl 17 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → ¬
((𝑛 ∈ ℕ ↦
(1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0}) |
150 | 145, 149 | eldifd 3585 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖
{0})) |
151 | 150 | adantl 482 |
. . . 4
⊢
((⊤ ∧ 𝑗
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖
{0})) |
152 | 110, 111 | recrecd 10798 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → (1 / (1 /
(seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗)) |
153 | 124, 126,
127, 121 | fvmptd 6288 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗))) |
154 | 153 | oveq2d 6666 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → (1 /
((𝑛 ∈ ℕ ↦
(1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗)))) |
155 | | wallispi.2 |
. . . . . . 7
⊢ 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · ,
𝐹)‘𝑛)) |
156 | 107, 155,
99 | fvmpt3 6286 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (seq1( · , 𝐹)‘𝑗)) |
157 | 152, 154,
156 | 3eqtr4rd 2667 |
. . . . 5
⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( ·
, 𝐹)‘𝑛)))‘𝑗))) |
158 | 157 | adantl 482 |
. . . 4
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( ·
, 𝐹)‘𝑛)))‘𝑗))) |
159 | 18 | mptex 6486 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ (seq1(
· , 𝐹)‘𝑛)) ∈ V |
160 | 155, 159 | eqeltri 2697 |
. . . . 5
⊢ 𝑊 ∈ V |
161 | 160 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑊 ∈
V) |
162 | 1, 2, 141, 144, 151, 158, 161 | climrec 39835 |
. . 3
⊢ (⊤
→ 𝑊 ⇝ (1 / (2 /
π))) |
163 | 162 | trud 1493 |
. 2
⊢ 𝑊 ⇝ (1 / (2 /
π)) |
164 | | recdiv 10731 |
. . 3
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0))
→ (1 / (2 / π)) = (π / 2)) |
165 | 138, 142,
11, 15, 164 | mp4an 709 |
. 2
⊢ (1 / (2 /
π)) = (π / 2) |
166 | 163, 165 | breqtri 4678 |
1
⊢ 𝑊 ⇝ (π /
2) |