Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. 2
⊢ (𝑘 ∈ ℕ ↦ (((2
· 𝑘) / ((2 ·
𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2
· 𝑘) / ((2 ·
𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) + 1)))) |
2 | | 1cnd 11150 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) |
3 | | 2cnd 12231 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 2 ∈
ℂ) |
4 | | nncn 12161 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
5 | 3, 4 | mulcld 11175 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℂ) |
6 | 5, 2 | addcld 11174 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℂ) |
7 | | elnnuz 12807 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
8 | 7 | biimpi 215 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) |
9 | | eqidd 2737 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (1...𝑛) → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2)))) |
10 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ (1...𝑛) ∧ 𝑘 = 𝑚) → 𝑘 = 𝑚) |
11 | 10 | oveq2d 7373 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ (1...𝑛) ∧ 𝑘 = 𝑚) → (2 · 𝑘) = (2 · 𝑚)) |
12 | 11 | oveq1d 7372 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ (1...𝑛) ∧ 𝑘 = 𝑚) → ((2 · 𝑘)↑4) = ((2 · 𝑚)↑4)) |
13 | 11 | oveq1d 7372 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ (1...𝑛) ∧ 𝑘 = 𝑚) → ((2 · 𝑘) − 1) = ((2 · 𝑚) − 1)) |
14 | 11, 13 | oveq12d 7375 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ (1...𝑛) ∧ 𝑘 = 𝑚) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 𝑚) · ((2 · 𝑚) − 1))) |
15 | 14 | oveq1d 7372 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ (1...𝑛) ∧ 𝑘 = 𝑚) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 𝑚) · ((2 · 𝑚) −
1))↑2)) |
16 | 12, 15 | oveq12d 7375 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ (1...𝑛) ∧ 𝑘 = 𝑚) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑚)↑4) / (((2 · 𝑚) · ((2 · 𝑚) −
1))↑2))) |
17 | | elfznn 13470 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (1...𝑛) → 𝑚 ∈ ℕ) |
18 | | 2cnd 12231 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1...𝑛) → 2 ∈ ℂ) |
19 | 17 | nncnd 12169 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1...𝑛) → 𝑚 ∈ ℂ) |
20 | 18, 19 | mulcld 11175 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (1...𝑛) → (2 · 𝑚) ∈ ℂ) |
21 | | 4nn0 12432 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℕ0 |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (1...𝑛) → 4 ∈
ℕ0) |
23 | 20, 22 | expcld 14051 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (1...𝑛) → ((2 · 𝑚)↑4) ∈ ℂ) |
24 | | 1cnd 11150 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1...𝑛) → 1 ∈ ℂ) |
25 | 20, 24 | subcld 11512 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1...𝑛) → ((2 · 𝑚) − 1) ∈ ℂ) |
26 | 20, 25 | mulcld 11175 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (1...𝑛) → ((2 · 𝑚) · ((2 · 𝑚) − 1)) ∈
ℂ) |
27 | 26 | sqcld 14049 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (1...𝑛) → (((2 · 𝑚) · ((2 · 𝑚) − 1))↑2) ∈
ℂ) |
28 | | 2ne0 12257 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1...𝑛) → 2 ≠ 0) |
30 | 17 | nnne0d 12203 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1...𝑛) → 𝑚 ≠ 0) |
31 | 18, 19, 29, 30 | mulne0d 11807 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1...𝑛) → (2 · 𝑚) ≠ 0) |
32 | | 1red 11156 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (1...𝑛) → 1 ∈ ℝ) |
33 | | 2re 12227 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (1...𝑛) → 2 ∈ ℝ) |
35 | 34, 32 | remulcld 11185 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ (1...𝑛) → (2 · 1) ∈
ℝ) |
36 | 17 | nnred 12168 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (1...𝑛) → 𝑚 ∈ ℝ) |
37 | 34, 36 | remulcld 11185 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ (1...𝑛) → (2 · 𝑚) ∈ ℝ) |
38 | | 1lt2 12324 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 <
2 |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (1...𝑛) → 1 < 2) |
40 | | 2t1e2 12316 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· 1) = 2 |
41 | 39, 40 | breqtrrdi 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ (1...𝑛) → 1 < (2 ·
1)) |
42 | | 0le2 12255 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
2 |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (1...𝑛) → 0 ≤ 2) |
44 | | elfzle1 13444 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (1...𝑛) → 1 ≤ 𝑚) |
45 | 32, 36, 34, 43, 44 | lemul2ad 12095 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ (1...𝑛) → (2 · 1) ≤ (2 ·
𝑚)) |
46 | 32, 35, 37, 41, 45 | ltletrd 11315 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (1...𝑛) → 1 < (2 · 𝑚)) |
47 | 32, 46 | gtned 11290 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1...𝑛) → (2 · 𝑚) ≠ 1) |
48 | 20, 24, 47 | subne0d 11521 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1...𝑛) → ((2 · 𝑚) − 1) ≠ 0) |
49 | 20, 25, 31, 48 | mulne0d 11807 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (1...𝑛) → ((2 · 𝑚) · ((2 · 𝑚) − 1)) ≠ 0) |
50 | | 2z 12535 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (1...𝑛) → 2 ∈ ℤ) |
52 | 26, 49, 51 | expne0d 14057 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (1...𝑛) → (((2 · 𝑚) · ((2 · 𝑚) − 1))↑2) ≠
0) |
53 | 23, 27, 52 | divcld 11931 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (1...𝑛) → (((2 · 𝑚)↑4) / (((2 · 𝑚) · ((2 · 𝑚) − 1))↑2)) ∈
ℂ) |
54 | 9, 16, 17, 53 | fvmptd 6955 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1...𝑛) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2)))‘𝑚) =
(((2 · 𝑚)↑4) /
(((2 · 𝑚) ·
((2 · 𝑚) −
1))↑2))) |
55 | 54, 53 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝑚 ∈ (1...𝑛) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2)))‘𝑚)
∈ ℂ) |
56 | 55 | adantl 482 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2)))‘𝑚)
∈ ℂ) |
57 | | mulcl 11135 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑚 · 𝑤) ∈ ℂ) |
58 | 57 | adantl 482 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (𝑚 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑚 · 𝑤) ∈ ℂ) |
59 | 8, 56, 58 | seqcl 13928 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛) ∈
ℂ) |
60 | | 2nn 12226 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
61 | 60 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) |
62 | | id 22 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) |
63 | 61, 62 | nnmulcld 12206 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ) |
64 | 63 | peano2nnd 12170 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℕ) |
65 | 64 | nnne0d 12203 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ≠
0) |
66 | 2, 6, 59, 65 | div32d 11954 |
. . . . 5
⊢ (𝑛 ∈ ℕ → ((1 / ((2
· 𝑛) + 1)) ·
(seq1( · , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛)) = (1 · ((seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛) / ((2 · 𝑛) + 1)))) |
67 | 59, 6, 65 | divcld 11931 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → ((seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛) / ((2 · 𝑛) + 1)) ∈
ℂ) |
68 | 67 | mulid2d 11173 |
. . . . 5
⊢ (𝑛 ∈ ℕ → (1
· ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2))))‘𝑛) /
((2 · 𝑛) + 1))) =
((seq1( · , (𝑘
∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛) / ((2 · 𝑛) + 1))) |
69 | | wallispi2lem2 44303 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛) = (((2↑(4 · 𝑛)) · ((!‘𝑛)↑4)) / ((!‘(2
· 𝑛))↑2))) |
70 | 69 | oveq1d 7372 |
. . . . 5
⊢ (𝑛 ∈ ℕ → ((seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛) / ((2 · 𝑛) + 1)) = ((((2↑(4 ·
𝑛)) ·
((!‘𝑛)↑4)) /
((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) |
71 | 66, 68, 70 | 3eqtrd 2780 |
. . . 4
⊢ (𝑛 ∈ ℕ → ((1 / ((2
· 𝑛) + 1)) ·
(seq1( · , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛)) = ((((2↑(4 ·
𝑛)) ·
((!‘𝑛)↑4)) /
((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) |
72 | 71 | mpteq2ia 5208 |
. . 3
⊢ (𝑛 ∈ ℕ ↦ ((1 /
((2 · 𝑛) + 1))
· (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2))))‘𝑛))) =
(𝑛 ∈ ℕ ↦
((((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) |
73 | | wallispi2lem1 44302 |
. . . 4
⊢ (𝑛 ∈ ℕ → (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑛) = ((1 / ((2 · 𝑛) + 1)) · (seq1( ·
, (𝑘 ∈ ℕ ↦
(((2 · 𝑘)↑4) /
(((2 · 𝑘) ·
((2 · 𝑘) −
1))↑2))))‘𝑛))) |
74 | 73 | mpteq2ia 5208 |
. . 3
⊢ (𝑛 ∈ ℕ ↦ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑛)) = (𝑛 ∈ ℕ ↦ ((1 / ((2 ·
𝑛) + 1)) · (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑛))) |
75 | | wallispi2.1 |
. . 3
⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((2↑(4
· 𝑛)) ·
((!‘𝑛)↑4)) /
((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) |
76 | 72, 74, 75 | 3eqtr4ri 2775 |
. 2
⊢ 𝑉 = (𝑛 ∈ ℕ ↦ (seq1( · ,
(𝑘 ∈ ℕ ↦
(((2 · 𝑘) / ((2
· 𝑘) − 1))
· ((2 · 𝑘) /
((2 · 𝑘) +
1)))))‘𝑛)) |
77 | 1, 76 | wallispi 44301 |
1
⊢ 𝑉 ⇝ (π /
2) |