Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . . 4
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | ax-1cn 9873 |
. . . . 5
⊢ 1 ∈
ℂ |
4 | 1 | eqimss2i 3623 |
. . . . . 6
⊢
(ℤ≥‘1) ⊆ ℕ |
5 | | nnex 10903 |
. . . . . 6
⊢ ℕ
∈ V |
6 | 4, 5 | climconst2 14127 |
. . . . 5
⊢ ((1
∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {1}) ⇝
1) |
7 | 3, 2, 6 | sylancr 694 |
. . . 4
⊢ (⊤
→ (ℕ × {1}) ⇝ 1) |
8 | | ovex 6577 |
. . . . 5
⊢ ((ℕ
× {1}) ∘𝑓 + ((ℕ × {𝐴}) ∘𝑓 ·
𝐺)) ∈
V |
9 | 8 | a1i 11 |
. . . 4
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{𝐴})
∘𝑓 · 𝐺)) ∈ V) |
10 | | basellem7.2 |
. . . . . . 7
⊢ 𝐴 ∈ ℂ |
11 | 4, 5 | climconst2 14127 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℤ) → (ℕ × {𝐴}) ⇝ 𝐴) |
12 | 10, 2, 11 | sylancr 694 |
. . . . . 6
⊢ (⊤
→ (ℕ × {𝐴}) ⇝ 𝐴) |
13 | | ovex 6577 |
. . . . . . 7
⊢ ((ℕ
× {𝐴})
∘𝑓 · 𝐺) ∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ((ℕ × {𝐴}) ∘𝑓 ·
𝐺) ∈
V) |
15 | | basel.g |
. . . . . . . 8
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 ·
𝑛) + 1))) |
16 | 15 | basellem6 24612 |
. . . . . . 7
⊢ 𝐺 ⇝ 0 |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝐺 ⇝
0) |
18 | 10 | elexi 3186 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
19 | 18 | fconst 6004 |
. . . . . . . 8
⊢ (ℕ
× {𝐴}):ℕ⟶{𝐴} |
20 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 𝐴 ∈
ℂ) |
21 | 20 | snssd 4281 |
. . . . . . . 8
⊢ (⊤
→ {𝐴} ⊆
ℂ) |
22 | | fss 5969 |
. . . . . . . 8
⊢
(((ℕ × {𝐴}):ℕ⟶{𝐴} ∧ {𝐴} ⊆ ℂ) → (ℕ ×
{𝐴}):ℕ⟶ℂ) |
23 | 19, 21, 22 | sylancr 694 |
. . . . . . 7
⊢ (⊤
→ (ℕ × {𝐴}):ℕ⟶ℂ) |
24 | 23 | ffvelrnda 6267 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {𝐴})‘𝑘) ∈ ℂ) |
25 | | 2nn 11062 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
26 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 2 ∈ ℕ) |
27 | | nnmulcl 10920 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ) → (2 · 𝑛) ∈ ℕ) |
28 | 26, 27 | sylan 487 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (2 · 𝑛) ∈ ℕ) |
29 | 28 | peano2nnd 10914 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑛
∈ ℕ) → ((2 · 𝑛) + 1) ∈ ℕ) |
30 | 29 | nnrecred 10943 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ ℝ) |
31 | 30 | recnd 9947 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ ℂ) |
32 | 31, 15 | fmptd 6292 |
. . . . . . 7
⊢ (⊤
→ 𝐺:ℕ⟶ℂ) |
33 | 32 | ffvelrnda 6267 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ∈ ℂ) |
34 | | ffn 5958 |
. . . . . . . 8
⊢ ((ℕ
× {𝐴}):ℕ⟶ℂ → (ℕ
× {𝐴}) Fn
ℕ) |
35 | 23, 34 | syl 17 |
. . . . . . 7
⊢ (⊤
→ (ℕ × {𝐴}) Fn ℕ) |
36 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐺:ℕ⟶ℂ →
𝐺 Fn
ℕ) |
37 | 32, 36 | syl 17 |
. . . . . . 7
⊢ (⊤
→ 𝐺 Fn
ℕ) |
38 | 5 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℕ ∈ V) |
39 | | inidm 3784 |
. . . . . . 7
⊢ (ℕ
∩ ℕ) = ℕ |
40 | | eqidd 2611 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {𝐴})‘𝑘) = ((ℕ × {𝐴})‘𝑘)) |
41 | | eqidd 2611 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) = (𝐺‘𝑘)) |
42 | 35, 37, 38, 38, 39, 40, 41 | ofval 6804 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {𝐴}) ∘𝑓 ·
𝐺)‘𝑘) = (((ℕ × {𝐴})‘𝑘) · (𝐺‘𝑘))) |
43 | 1, 2, 12, 14, 17, 24, 33, 42 | climmul 14211 |
. . . . 5
⊢ (⊤
→ ((ℕ × {𝐴}) ∘𝑓 ·
𝐺) ⇝ (𝐴 · 0)) |
44 | 10 | mul01i 10105 |
. . . . 5
⊢ (𝐴 · 0) =
0 |
45 | 43, 44 | syl6breq 4624 |
. . . 4
⊢ (⊤
→ ((ℕ × {𝐴}) ∘𝑓 ·
𝐺) ⇝
0) |
46 | | 1ex 9914 |
. . . . . . 7
⊢ 1 ∈
V |
47 | 46 | fconst 6004 |
. . . . . 6
⊢ (ℕ
× {1}):ℕ⟶{1} |
48 | 3 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 1 ∈ ℂ) |
49 | 48 | snssd 4281 |
. . . . . 6
⊢ (⊤
→ {1} ⊆ ℂ) |
50 | | fss 5969 |
. . . . . 6
⊢
(((ℕ × {1}):ℕ⟶{1} ∧ {1} ⊆ ℂ)
→ (ℕ × {1}):ℕ⟶ℂ) |
51 | 47, 49, 50 | sylancr 694 |
. . . . 5
⊢ (⊤
→ (ℕ × {1}):ℕ⟶ℂ) |
52 | 51 | ffvelrnda 6267 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {1})‘𝑘) ∈ ℂ) |
53 | | mulcl 9899 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
54 | 53 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℂ ∧ 𝑦
∈ ℂ)) → (𝑥
· 𝑦) ∈
ℂ) |
55 | 54, 23, 32, 38, 38, 39 | off 6810 |
. . . . 5
⊢ (⊤
→ ((ℕ × {𝐴}) ∘𝑓 ·
𝐺):ℕ⟶ℂ) |
56 | 55 | ffvelrnda 6267 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {𝐴}) ∘𝑓 ·
𝐺)‘𝑘) ∈ ℂ) |
57 | 47 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (ℕ × {1}):ℕ⟶{1}) |
58 | | ffn 5958 |
. . . . . 6
⊢ ((ℕ
× {1}):ℕ⟶{1} → (ℕ × {1}) Fn
ℕ) |
59 | 57, 58 | syl 17 |
. . . . 5
⊢ (⊤
→ (ℕ × {1}) Fn ℕ) |
60 | | ffn 5958 |
. . . . . 6
⊢
(((ℕ × {𝐴}) ∘𝑓 ·
𝐺):ℕ⟶ℂ
→ ((ℕ × {𝐴}) ∘𝑓 ·
𝐺) Fn
ℕ) |
61 | 55, 60 | syl 17 |
. . . . 5
⊢ (⊤
→ ((ℕ × {𝐴}) ∘𝑓 ·
𝐺) Fn
ℕ) |
62 | | eqidd 2611 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {1})‘𝑘) = ((ℕ × {1})‘𝑘)) |
63 | | eqidd 2611 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {𝐴}) ∘𝑓 ·
𝐺)‘𝑘) = (((ℕ × {𝐴}) ∘𝑓 ·
𝐺)‘𝑘)) |
64 | 59, 61, 38, 38, 39, 62, 63 | ofval 6804 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓 +
((ℕ × {𝐴})
∘𝑓 · 𝐺))‘𝑘) = (((ℕ × {1})‘𝑘) + (((ℕ × {𝐴}) ∘𝑓
· 𝐺)‘𝑘))) |
65 | 1, 2, 7, 9, 45, 52, 56, 64 | climadd 14210 |
. . 3
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{𝐴})
∘𝑓 · 𝐺)) ⇝ (1 + 0)) |
66 | 65 | trud 1484 |
. 2
⊢ ((ℕ
× {1}) ∘𝑓 + ((ℕ × {𝐴}) ∘𝑓 ·
𝐺)) ⇝ (1 +
0) |
67 | | 1p0e1 11010 |
. 2
⊢ (1 + 0) =
1 |
68 | 66, 67 | breqtri 4608 |
1
⊢ ((ℕ
× {1}) ∘𝑓 + ((ℕ × {𝐴}) ∘𝑓 ·
𝐺)) ⇝
1 |