Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . 3
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | oveq1 6556 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑛↑-2) = (𝑘↑-2)) |
4 | | eqid 2610 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ (𝑛↑-2)) = (𝑛 ∈ ℕ ↦ (𝑛↑-2)) |
5 | | ovex 6577 |
. . . . 5
⊢ (𝑘↑-2) ∈
V |
6 | 3, 4, 5 | fvmpt 6191 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2)) |
7 | 6 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2)) |
8 | | nnre 10904 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
9 | | nnne0 10930 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
10 | | 2z 11286 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
11 | | znegcl 11289 |
. . . . . . . . . . 11
⊢ (2 ∈
ℤ → -2 ∈ ℤ) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
⊢ -2 ∈
ℤ |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → -2 ∈
ℤ) |
14 | 8, 9, 13 | reexpclzd 12896 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛↑-2) ∈
ℝ) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (𝑛↑-2) ∈ ℝ) |
16 | 15, 4 | fmptd 6292 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (𝑛↑-2)):ℕ⟶ℝ) |
17 | 16 | ffvelrnda 6267 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (𝑛↑-2))‘𝑘) ∈ ℝ) |
18 | 7, 17 | eqeltrrd 2689 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝑘↑-2) ∈ ℝ) |
19 | 18 | recnd 9947 |
. . 3
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝑘↑-2) ∈ ℂ) |
20 | 1, 2, 17 | serfre 12692 |
. . . . . . . . . . 11
⊢ (⊤
→ seq1( + , (𝑛 ∈
ℕ ↦ (𝑛↑-2))):ℕ⟶ℝ) |
21 | | basel.f |
. . . . . . . . . . . 12
⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2))) |
22 | 21 | feq1i 5949 |
. . . . . . . . . . 11
⊢ (𝐹:ℕ⟶ℝ ↔
seq1( + , (𝑛 ∈ ℕ
↦ (𝑛↑-2))):ℕ⟶ℝ) |
23 | 20, 22 | sylibr 223 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐹:ℕ⟶ℝ) |
24 | 23 | ffvelrnda 6267 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (𝐹‘𝑛) ∈ ℝ) |
25 | 24 | recnd 9947 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (𝐹‘𝑛) ∈ ℂ) |
26 | | remulcl 9900 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
27 | 26 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 𝑦
∈ ℝ)) → (𝑥
· 𝑦) ∈
ℝ) |
28 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢
((π↑2) / 6) ∈ V |
29 | 28 | fconst 6004 |
. . . . . . . . . . . . . . 15
⊢ (ℕ
× {((π↑2) / 6)}):ℕ⟶{((π↑2) /
6)} |
30 | | pire 24014 |
. . . . . . . . . . . . . . . . . . 19
⊢ π
∈ ℝ |
31 | 30 | resqcli 12811 |
. . . . . . . . . . . . . . . . . 18
⊢
(π↑2) ∈ ℝ |
32 | | 6re 10978 |
. . . . . . . . . . . . . . . . . 18
⊢ 6 ∈
ℝ |
33 | | 6nn 11066 |
. . . . . . . . . . . . . . . . . . 19
⊢ 6 ∈
ℕ |
34 | 33 | nnne0i 10932 |
. . . . . . . . . . . . . . . . . 18
⊢ 6 ≠
0 |
35 | 31, 32, 34 | redivcli 10671 |
. . . . . . . . . . . . . . . . 17
⊢
((π↑2) / 6) ∈ ℝ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ((π↑2) / 6) ∈ ℝ) |
37 | 36 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ {((π↑2) / 6)} ⊆ ℝ) |
38 | | fss 5969 |
. . . . . . . . . . . . . . 15
⊢
(((ℕ × {((π↑2) / 6)}):ℕ⟶{((π↑2)
/ 6)} ∧ {((π↑2) / 6)} ⊆ ℝ) → (ℕ ×
{((π↑2) / 6)}):ℕ⟶ℝ) |
39 | 29, 37, 38 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℕ × {((π↑2) /
6)}):ℕ⟶ℝ) |
40 | | resubcl 10224 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 − 𝑦) ∈ ℝ) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 𝑦
∈ ℝ)) → (𝑥
− 𝑦) ∈
ℝ) |
42 | | 1ex 9914 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
V |
43 | 42 | fconst 6004 |
. . . . . . . . . . . . . . . 16
⊢ (ℕ
× {1}):ℕ⟶{1} |
44 | | 1red 9934 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ 1 ∈ ℝ) |
45 | 44 | snssd 4281 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ {1} ⊆ ℝ) |
46 | | fss 5969 |
. . . . . . . . . . . . . . . 16
⊢
(((ℕ × {1}):ℕ⟶{1} ∧ {1} ⊆ ℝ)
→ (ℕ × {1}):ℕ⟶ℝ) |
47 | 43, 45, 46 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (ℕ × {1}):ℕ⟶ℝ) |
48 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℕ |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⊤
→ 2 ∈ ℕ) |
50 | | nnmulcl 10920 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ) → (2 · 𝑛) ∈ ℕ) |
51 | 49, 50 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (2 · 𝑛) ∈ ℕ) |
52 | 51 | peano2nnd 10914 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑛
∈ ℕ) → ((2 · 𝑛) + 1) ∈ ℕ) |
53 | 52 | nnrecred 10943 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ ℝ) |
54 | | basel.g |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 ·
𝑛) + 1))) |
55 | 53, 54 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ 𝐺:ℕ⟶ℝ) |
56 | | nnex 10903 |
. . . . . . . . . . . . . . . 16
⊢ ℕ
∈ V |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ℕ ∈ V) |
58 | | inidm 3784 |
. . . . . . . . . . . . . . 15
⊢ (ℕ
∩ ℕ) = ℕ |
59 | 41, 47, 55, 57, 57, 58 | off 6810 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 − 𝐺):ℕ⟶ℝ) |
60 | 27, 39, 59, 57, 57, 58 | off 6810 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ((ℕ × {((π↑2) / 6)}) ∘𝑓
· ((ℕ × {1}) ∘𝑓 − 𝐺)):ℕ⟶ℝ) |
61 | | basel.h |
. . . . . . . . . . . . . 14
⊢ 𝐻 = ((ℕ ×
{((π↑2) / 6)}) ∘𝑓 · ((ℕ ×
{1}) ∘𝑓 − 𝐺)) |
62 | 61 | feq1i 5949 |
. . . . . . . . . . . . 13
⊢ (𝐻:ℕ⟶ℝ ↔
((ℕ × {((π↑2) / 6)}) ∘𝑓 ·
((ℕ × {1}) ∘𝑓 − 𝐺)):ℕ⟶ℝ) |
63 | 60, 62 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (⊤
→ 𝐻:ℕ⟶ℝ) |
64 | | readdcl 9898 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
65 | 64 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 𝑦
∈ ℝ)) → (𝑥
+ 𝑦) ∈
ℝ) |
66 | | negex 10158 |
. . . . . . . . . . . . . . . 16
⊢ -2 ∈
V |
67 | 66 | fconst 6004 |
. . . . . . . . . . . . . . 15
⊢ (ℕ
× {-2}):ℕ⟶{-2} |
68 | 12 | zrei 11260 |
. . . . . . . . . . . . . . . . 17
⊢ -2 ∈
ℝ |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ -2 ∈ ℝ) |
70 | 69 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ {-2} ⊆ ℝ) |
71 | | fss 5969 |
. . . . . . . . . . . . . . 15
⊢
(((ℕ × {-2}):ℕ⟶{-2} ∧ {-2} ⊆ ℝ)
→ (ℕ × {-2}):ℕ⟶ℝ) |
72 | 67, 70, 71 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℕ × {-2}):ℕ⟶ℝ) |
73 | 27, 72, 55, 57, 57, 58 | off 6810 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ((ℕ × {-2}) ∘𝑓 · 𝐺):ℕ⟶ℝ) |
74 | 65, 47, 73, 57, 57, 58 | off 6810 |
. . . . . . . . . . . 12
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{-2}) ∘𝑓 · 𝐺)):ℕ⟶ℝ) |
75 | 27, 63, 74, 57, 57, 58 | off 6810 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))):ℕ⟶ℝ) |
76 | | basel.j |
. . . . . . . . . . . 12
⊢ 𝐽 = (𝐻 ∘𝑓 ·
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))) |
77 | 76 | feq1i 5949 |
. . . . . . . . . . 11
⊢ (𝐽:ℕ⟶ℝ ↔
(𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))):ℕ⟶ℝ) |
78 | 75, 77 | sylibr 223 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐽:ℕ⟶ℝ) |
79 | 78 | ffvelrnda 6267 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (𝐽‘𝑛) ∈ ℝ) |
80 | 79 | recnd 9947 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (𝐽‘𝑛) ∈ ℂ) |
81 | 25, 80 | npcand 10275 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (((𝐹‘𝑛) − (𝐽‘𝑛)) + (𝐽‘𝑛)) = (𝐹‘𝑛)) |
82 | 81 | mpteq2dva 4672 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (((𝐹‘𝑛) − (𝐽‘𝑛)) + (𝐽‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))) |
83 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝐹‘𝑛) − (𝐽‘𝑛)) ∈ V |
84 | 83 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℕ) → ((𝐹‘𝑛) − (𝐽‘𝑛)) ∈ V) |
85 | 23 | feqmptd 6159 |
. . . . . . . 8
⊢ (⊤
→ 𝐹 = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))) |
86 | 78 | feqmptd 6159 |
. . . . . . . 8
⊢ (⊤
→ 𝐽 = (𝑛 ∈ ℕ ↦ (𝐽‘𝑛))) |
87 | 57, 24, 79, 85, 86 | offval2 6812 |
. . . . . . 7
⊢ (⊤
→ (𝐹
∘𝑓 − 𝐽) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛) − (𝐽‘𝑛)))) |
88 | 57, 84, 79, 87, 86 | offval2 6812 |
. . . . . 6
⊢ (⊤
→ ((𝐹
∘𝑓 − 𝐽) ∘𝑓 + 𝐽) = (𝑛 ∈ ℕ ↦ (((𝐹‘𝑛) − (𝐽‘𝑛)) + (𝐽‘𝑛)))) |
89 | 82, 88, 85 | 3eqtr4d 2654 |
. . . . 5
⊢ (⊤
→ ((𝐹
∘𝑓 − 𝐽) ∘𝑓 + 𝐽) = 𝐹) |
90 | 65, 47, 55, 57, 57, 58 | off 6810 |
. . . . . . . . . 10
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + 𝐺):ℕ⟶ℝ) |
91 | | recn 9905 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
92 | | recn 9905 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
93 | | recn 9905 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℂ) |
94 | | subdi 10342 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 · (𝑦 − 𝑧)) = ((𝑥 · 𝑦) − (𝑥 · 𝑧))) |
95 | 91, 92, 93, 94 | syl3an 1360 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 · (𝑦 − 𝑧)) = ((𝑥 · 𝑦) − (𝑥 · 𝑧))) |
96 | 95 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 𝑦
∈ ℝ ∧ 𝑧
∈ ℝ)) → (𝑥
· (𝑦 − 𝑧)) = ((𝑥 · 𝑦) − (𝑥 · 𝑧))) |
97 | 57, 63, 90, 74, 96 | caofdi 6831 |
. . . . . . . . 9
⊢ (⊤
→ (𝐻
∘𝑓 · (((ℕ × {1})
∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))) = ((𝐻 ∘𝑓 ·
((ℕ × {1}) ∘𝑓 + 𝐺)) ∘𝑓 −
(𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))))) |
98 | | basel.k |
. . . . . . . . . 10
⊢ 𝐾 = (𝐻 ∘𝑓 ·
((ℕ × {1}) ∘𝑓 + 𝐺)) |
99 | 98, 76 | oveq12i 6561 |
. . . . . . . . 9
⊢ (𝐾 ∘𝑓
− 𝐽) = ((𝐻 ∘𝑓
· ((ℕ × {1}) ∘𝑓 + 𝐺)) ∘𝑓 −
(𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))) |
100 | 97, 99 | syl6eqr 2662 |
. . . . . . . 8
⊢ (⊤
→ (𝐻
∘𝑓 · (((ℕ × {1})
∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))) = (𝐾 ∘𝑓 − 𝐽)) |
101 | 35 | recni 9931 |
. . . . . . . . . . . . . 14
⊢
((π↑2) / 6) ∈ ℂ |
102 | 1 | eqimss2i 3623 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘1) ⊆ ℕ |
103 | 102, 56 | climconst2 14127 |
. . . . . . . . . . . . . 14
⊢
((((π↑2) / 6) ∈ ℂ ∧ 1 ∈ ℤ) →
(ℕ × {((π↑2) / 6)}) ⇝ ((π↑2) /
6)) |
104 | 101, 2, 103 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℕ × {((π↑2) / 6)}) ⇝ ((π↑2) /
6)) |
105 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ ((ℕ
× {((π↑2) / 6)}) ∘𝑓 · ((ℕ
× {1}) ∘𝑓 − 𝐺)) ∈ V |
106 | 105 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ((ℕ × {((π↑2) / 6)}) ∘𝑓
· ((ℕ × {1}) ∘𝑓 − 𝐺)) ∈ V) |
107 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
⊆ ℂ |
108 | | fss 5969 |
. . . . . . . . . . . . . . . 16
⊢
(((ℕ × {1}):ℕ⟶ℝ ∧ ℝ ⊆
ℂ) → (ℕ × {1}):ℕ⟶ℂ) |
109 | 47, 107, 108 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (ℕ × {1}):ℕ⟶ℂ) |
110 | | fss 5969 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ⟶ℝ ∧
ℝ ⊆ ℂ) → 𝐺:ℕ⟶ℂ) |
111 | 55, 107, 110 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ 𝐺:ℕ⟶ℂ) |
112 | | ofnegsub 10895 |
. . . . . . . . . . . . . . 15
⊢ ((ℕ
∈ V ∧ (ℕ × {1}):ℕ⟶ℂ ∧ 𝐺:ℕ⟶ℂ) →
((ℕ × {1}) ∘𝑓 + ((ℕ × {-1})
∘𝑓 · 𝐺)) = ((ℕ × {1})
∘𝑓 − 𝐺)) |
113 | 57, 109, 111, 112 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{-1}) ∘𝑓 · 𝐺)) = ((ℕ × {1})
∘𝑓 − 𝐺)) |
114 | | neg1cn 11001 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ |
115 | 54, 114 | basellem7 24613 |
. . . . . . . . . . . . . 14
⊢ ((ℕ
× {1}) ∘𝑓 + ((ℕ × {-1})
∘𝑓 · 𝐺)) ⇝ 1 |
116 | 113, 115 | syl6eqbrr 4623 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 − 𝐺) ⇝ 1) |
117 | 39 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {((π↑2) / 6)})‘𝑘) ∈
ℝ) |
118 | 117 | recnd 9947 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {((π↑2) / 6)})‘𝑘) ∈
ℂ) |
119 | 59 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓
− 𝐺)‘𝑘) ∈
ℝ) |
120 | 119 | recnd 9947 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓
− 𝐺)‘𝑘) ∈
ℂ) |
121 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ ((ℕ
× {((π↑2) / 6)}):ℕ⟶ℝ → (ℕ ×
{((π↑2) / 6)}) Fn ℕ) |
122 | 39, 121 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℕ × {((π↑2) / 6)}) Fn ℕ) |
123 | | fnconstg 6006 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ → (ℕ × {1}) Fn ℕ) |
124 | 2, 123 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (ℕ × {1}) Fn ℕ) |
125 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:ℕ⟶ℝ →
𝐺 Fn
ℕ) |
126 | 55, 125 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ 𝐺 Fn
ℕ) |
127 | 124, 126,
57, 57, 58 | offn 6806 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 − 𝐺) Fn ℕ) |
128 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {((π↑2) / 6)})‘𝑘) = ((ℕ ×
{((π↑2) / 6)})‘𝑘)) |
129 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓
− 𝐺)‘𝑘) = (((ℕ × {1})
∘𝑓 − 𝐺)‘𝑘)) |
130 | 122, 127,
57, 57, 58, 128, 129 | ofval 6804 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {((π↑2) / 6)})
∘𝑓 · ((ℕ × {1})
∘𝑓 − 𝐺))‘𝑘) = (((ℕ × {((π↑2) /
6)})‘𝑘) ·
(((ℕ × {1}) ∘𝑓 − 𝐺)‘𝑘))) |
131 | 1, 2, 104, 106, 116, 118, 120, 130 | climmul 14211 |
. . . . . . . . . . . 12
⊢ (⊤
→ ((ℕ × {((π↑2) / 6)}) ∘𝑓
· ((ℕ × {1}) ∘𝑓 − 𝐺)) ⇝ (((π↑2) / 6)
· 1)) |
132 | 101 | mulid1i 9921 |
. . . . . . . . . . . 12
⊢
(((π↑2) / 6) · 1) = ((π↑2) / 6) |
133 | 131, 132 | syl6breq 4624 |
. . . . . . . . . . 11
⊢ (⊤
→ ((ℕ × {((π↑2) / 6)}) ∘𝑓
· ((ℕ × {1}) ∘𝑓 − 𝐺)) ⇝ ((π↑2) /
6)) |
134 | 61, 133 | syl5eqbr 4618 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐻 ⇝
((π↑2) / 6)) |
135 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝐻 ∘𝑓
· (((ℕ × {1}) ∘𝑓 + 𝐺) ∘𝑓
− ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{-2}) ∘𝑓 · 𝐺)))) ∈ V |
136 | 135 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (𝐻
∘𝑓 · (((ℕ × {1})
∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))) ∈ V) |
137 | | 3cn 10972 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
138 | 102, 56 | climconst2 14127 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {3}) ⇝
3) |
139 | 137, 2, 138 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℕ × {3}) ⇝ 3) |
140 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((ℕ
× {3}) ∘𝑓 · 𝐺) ∈ V |
141 | 140 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ((ℕ × {3}) ∘𝑓 · 𝐺) ∈ V) |
142 | 54 | basellem6 24612 |
. . . . . . . . . . . . 13
⊢ 𝐺 ⇝ 0 |
143 | 142 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 𝐺 ⇝
0) |
144 | | 3ex 10973 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
V |
145 | 144 | fconst 6004 |
. . . . . . . . . . . . . . 15
⊢ (ℕ
× {3}):ℕ⟶{3} |
146 | | 3re 10971 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℝ |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ 3 ∈ ℝ) |
148 | 147 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ {3} ⊆ ℝ) |
149 | | fss 5969 |
. . . . . . . . . . . . . . 15
⊢
(((ℕ × {3}):ℕ⟶{3} ∧ {3} ⊆ ℝ)
→ (ℕ × {3}):ℕ⟶ℝ) |
150 | 145, 148,
149 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℕ × {3}):ℕ⟶ℝ) |
151 | 150 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {3})‘𝑘) ∈ ℝ) |
152 | 151 | recnd 9947 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {3})‘𝑘) ∈ ℂ) |
153 | 55 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
154 | 153 | recnd 9947 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ∈ ℂ) |
155 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ ((ℕ
× {3}):ℕ⟶ℝ → (ℕ × {3}) Fn
ℕ) |
156 | 150, 155 | syl 17 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℕ × {3}) Fn ℕ) |
157 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((ℕ × {3})‘𝑘) = ((ℕ × {3})‘𝑘)) |
158 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) = (𝐺‘𝑘)) |
159 | 156, 126,
57, 57, 58, 157, 158 | ofval 6804 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {3}) ∘𝑓
· 𝐺)‘𝑘) = (((ℕ ×
{3})‘𝑘) ·
(𝐺‘𝑘))) |
160 | 1, 2, 139, 141, 143, 152, 154, 159 | climmul 14211 |
. . . . . . . . . . 11
⊢ (⊤
→ ((ℕ × {3}) ∘𝑓 · 𝐺) ⇝ (3 ·
0)) |
161 | 137 | mul01i 10105 |
. . . . . . . . . . 11
⊢ (3
· 0) = 0 |
162 | 160, 161 | syl6breq 4624 |
. . . . . . . . . 10
⊢ (⊤
→ ((ℕ × {3}) ∘𝑓 · 𝐺) ⇝ 0) |
163 | 63 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐻‘𝑘) ∈ ℝ) |
164 | 163 | recnd 9947 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐻‘𝑘) ∈ ℂ) |
165 | 27, 150, 55, 57, 57, 58 | off 6810 |
. . . . . . . . . . . 12
⊢ (⊤
→ ((ℕ × {3}) ∘𝑓 · 𝐺):ℕ⟶ℝ) |
166 | 165 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {3}) ∘𝑓
· 𝐺)‘𝑘) ∈
ℝ) |
167 | 166 | recnd 9947 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {3}) ∘𝑓
· 𝐺)‘𝑘) ∈
ℂ) |
168 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐻:ℕ⟶ℝ →
𝐻 Fn
ℕ) |
169 | 63, 168 | syl 17 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐻 Fn
ℕ) |
170 | 41, 90, 74, 57, 57, 58 | off 6810 |
. . . . . . . . . . . 12
⊢ (⊤
→ (((ℕ × {1}) ∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))):ℕ⟶ℝ) |
171 | | ffn 5958 |
. . . . . . . . . . . 12
⊢
((((ℕ × {1}) ∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))):ℕ⟶ℝ → (((ℕ
× {1}) ∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))) Fn ℕ) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . 11
⊢ (⊤
→ (((ℕ × {1}) ∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))) Fn ℕ) |
173 | | eqidd 2611 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐻‘𝑘) = (𝐻‘𝑘)) |
174 | 154 | mulid2d 9937 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 · (𝐺‘𝑘)) = (𝐺‘𝑘)) |
175 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℂ |
176 | | mulneg1 10345 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℂ ∧ (𝐺‘𝑘) ∈ ℂ) → (-2 · (𝐺‘𝑘)) = -(2 · (𝐺‘𝑘))) |
177 | 175, 154,
176 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (-2 · (𝐺‘𝑘)) = -(2 · (𝐺‘𝑘))) |
178 | 177 | negeqd 10154 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑘
∈ ℕ) → -(-2 · (𝐺‘𝑘)) = --(2 · (𝐺‘𝑘))) |
179 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℂ ∧ (𝐺‘𝑘) ∈ ℂ) → (2 · (𝐺‘𝑘)) ∈ ℂ) |
180 | 175, 154,
179 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (2 · (𝐺‘𝑘)) ∈ ℂ) |
181 | 180 | negnegd 10262 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑘
∈ ℕ) → --(2 · (𝐺‘𝑘)) = (2 · (𝐺‘𝑘))) |
182 | 178, 181 | eqtr2d 2645 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (2 · (𝐺‘𝑘)) = -(-2 · (𝐺‘𝑘))) |
183 | 174, 182 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((1 · (𝐺‘𝑘)) + (2 · (𝐺‘𝑘))) = ((𝐺‘𝑘) + -(-2 · (𝐺‘𝑘)))) |
184 | | remulcl 9900 |
. . . . . . . . . . . . . . . . 17
⊢ ((-2
∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → (-2 · (𝐺‘𝑘)) ∈ ℝ) |
185 | 68, 153, 184 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (-2 · (𝐺‘𝑘)) ∈ ℝ) |
186 | 185 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (-2 · (𝐺‘𝑘)) ∈ ℂ) |
187 | 154, 186 | negsubd 10277 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐺‘𝑘) + -(-2 · (𝐺‘𝑘))) = ((𝐺‘𝑘) − (-2 · (𝐺‘𝑘)))) |
188 | 183, 187 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((1 · (𝐺‘𝑘)) + (2 · (𝐺‘𝑘))) = ((𝐺‘𝑘) − (-2 · (𝐺‘𝑘)))) |
189 | | df-3 10957 |
. . . . . . . . . . . . . . . 16
⊢ 3 = (2 +
1) |
190 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
191 | 175, 190 | addcomi 10106 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 1) =
(1 + 2) |
192 | 189, 191 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ 3 = (1 +
2) |
193 | 192 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (3
· (𝐺‘𝑘)) = ((1 + 2) · (𝐺‘𝑘)) |
194 | | 1cnd 9935 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 1 ∈ ℂ) |
195 | 175 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 2 ∈ ℂ) |
196 | 194, 195,
154 | adddird 9944 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((1 + 2) · (𝐺‘𝑘)) = ((1 · (𝐺‘𝑘)) + (2 · (𝐺‘𝑘)))) |
197 | 193, 196 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (3 · (𝐺‘𝑘)) = ((1 · (𝐺‘𝑘)) + (2 · (𝐺‘𝑘)))) |
198 | 194, 154,
186 | pnpcand 10308 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((1 + (𝐺‘𝑘)) − (1 + (-2 · (𝐺‘𝑘)))) = ((𝐺‘𝑘) − (-2 · (𝐺‘𝑘)))) |
199 | 188, 197,
198 | 3eqtr4rd 2655 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((1 + (𝐺‘𝑘)) − (1 + (-2 · (𝐺‘𝑘)))) = (3 · (𝐺‘𝑘))) |
200 | 124, 126,
57, 57, 58 | offn 6806 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + 𝐺) Fn ℕ) |
201 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ -2 ∈ ℤ) |
202 | | fnconstg 6006 |
. . . . . . . . . . . . . . . 16
⊢ (-2
∈ ℤ → (ℕ × {-2}) Fn ℕ) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (ℕ × {-2}) Fn ℕ) |
204 | 203, 126,
57, 57, 58 | offn 6806 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ ((ℕ × {-2}) ∘𝑓 · 𝐺) Fn ℕ) |
205 | 124, 204,
57, 57, 58 | offn 6806 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{-2}) ∘𝑓 · 𝐺)) Fn ℕ) |
206 | 57, 44, 126, 158 | ofc1 6818 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓 +
𝐺)‘𝑘) = (1 + (𝐺‘𝑘))) |
207 | 57, 69, 126, 158 | ofc1 6818 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {-2}) ∘𝑓
· 𝐺)‘𝑘) = (-2 · (𝐺‘𝑘))) |
208 | 57, 44, 204, 207 | ofc1 6818 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓 +
((ℕ × {-2}) ∘𝑓 · 𝐺))‘𝑘) = (1 + (-2 · (𝐺‘𝑘)))) |
209 | 200, 205,
57, 57, 58, 206, 208 | ofval 6804 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((((ℕ × {1}) ∘𝑓 +
𝐺)
∘𝑓 − ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))‘𝑘) = ((1 + (𝐺‘𝑘)) − (1 + (-2 · (𝐺‘𝑘))))) |
210 | 57, 147, 126, 158 | ofc1 6818 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {3}) ∘𝑓
· 𝐺)‘𝑘) = (3 · (𝐺‘𝑘))) |
211 | 199, 209,
210 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((((ℕ × {1}) ∘𝑓 +
𝐺)
∘𝑓 − ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))‘𝑘) = (((ℕ × {3})
∘𝑓 · 𝐺)‘𝑘)) |
212 | 169, 172,
57, 57, 58, 173, 211 | ofval 6804 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐻
∘𝑓 · (((ℕ × {1})
∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))))‘𝑘) = ((𝐻‘𝑘) · (((ℕ × {3})
∘𝑓 · 𝐺)‘𝑘))) |
213 | 1, 2, 134, 136, 162, 164, 167, 212 | climmul 14211 |
. . . . . . . . 9
⊢ (⊤
→ (𝐻
∘𝑓 · (((ℕ × {1})
∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))) ⇝ (((π↑2) / 6) ·
0)) |
214 | 101 | mul01i 10105 |
. . . . . . . . 9
⊢
(((π↑2) / 6) · 0) = 0 |
215 | 213, 214 | syl6breq 4624 |
. . . . . . . 8
⊢ (⊤
→ (𝐻
∘𝑓 · (((ℕ × {1})
∘𝑓 + 𝐺) ∘𝑓 −
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))) ⇝ 0) |
216 | 100, 215 | eqbrtrrd 4607 |
. . . . . . 7
⊢ (⊤
→ (𝐾
∘𝑓 − 𝐽) ⇝ 0) |
217 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐹 ∘𝑓
− 𝐽) ∈
V |
218 | 217 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (𝐹
∘𝑓 − 𝐽) ∈ V) |
219 | 27, 63, 90, 57, 57, 58 | off 6810 |
. . . . . . . . . 10
⊢ (⊤
→ (𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + 𝐺)):ℕ⟶ℝ) |
220 | 98 | feq1i 5949 |
. . . . . . . . . 10
⊢ (𝐾:ℕ⟶ℝ ↔
(𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + 𝐺)):ℕ⟶ℝ) |
221 | 219, 220 | sylibr 223 |
. . . . . . . . 9
⊢ (⊤
→ 𝐾:ℕ⟶ℝ) |
222 | 41, 221, 78, 57, 57, 58 | off 6810 |
. . . . . . . 8
⊢ (⊤
→ (𝐾
∘𝑓 − 𝐽):ℕ⟶ℝ) |
223 | 222 | ffvelrnda 6267 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐾
∘𝑓 − 𝐽)‘𝑘) ∈ ℝ) |
224 | 41, 23, 78, 57, 57, 58 | off 6810 |
. . . . . . . 8
⊢ (⊤
→ (𝐹
∘𝑓 − 𝐽):ℕ⟶ℝ) |
225 | 224 | ffvelrnda 6267 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐹
∘𝑓 − 𝐽)‘𝑘) ∈ ℝ) |
226 | 23 | ffvelrnda 6267 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
227 | 221 | ffvelrnda 6267 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐾‘𝑘) ∈ ℝ) |
228 | 78 | ffvelrnda 6267 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐽‘𝑘) ∈ ℝ) |
229 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑘) + 1) = ((2
· 𝑘) +
1) |
230 | 54, 21, 61, 76, 98, 229 | basellem8 24614 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((𝐽‘𝑘) ≤ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ≤ (𝐾‘𝑘))) |
231 | 230 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐽‘𝑘) ≤ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ≤ (𝐾‘𝑘))) |
232 | 231 | simprd 478 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) ≤ (𝐾‘𝑘)) |
233 | 226, 227,
228, 232 | lesub1dd 10522 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐹‘𝑘) − (𝐽‘𝑘)) ≤ ((𝐾‘𝑘) − (𝐽‘𝑘))) |
234 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:ℕ⟶ℝ →
𝐹 Fn
ℕ) |
235 | 23, 234 | syl 17 |
. . . . . . . . 9
⊢ (⊤
→ 𝐹 Fn
ℕ) |
236 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐽:ℕ⟶ℝ →
𝐽 Fn
ℕ) |
237 | 78, 236 | syl 17 |
. . . . . . . . 9
⊢ (⊤
→ 𝐽 Fn
ℕ) |
238 | | eqidd 2611 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
239 | | eqidd 2611 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐽‘𝑘) = (𝐽‘𝑘)) |
240 | 235, 237,
57, 57, 58, 238, 239 | ofval 6804 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐹
∘𝑓 − 𝐽)‘𝑘) = ((𝐹‘𝑘) − (𝐽‘𝑘))) |
241 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐾:ℕ⟶ℝ →
𝐾 Fn
ℕ) |
242 | 221, 241 | syl 17 |
. . . . . . . . 9
⊢ (⊤
→ 𝐾 Fn
ℕ) |
243 | | eqidd 2611 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐾‘𝑘) = (𝐾‘𝑘)) |
244 | 242, 237,
57, 57, 58, 243, 239 | ofval 6804 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐾
∘𝑓 − 𝐽)‘𝑘) = ((𝐾‘𝑘) − (𝐽‘𝑘))) |
245 | 233, 240,
244 | 3brtr4d 4615 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐹
∘𝑓 − 𝐽)‘𝑘) ≤ ((𝐾 ∘𝑓 − 𝐽)‘𝑘)) |
246 | 231 | simpld 474 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐽‘𝑘) ≤ (𝐹‘𝑘)) |
247 | 226, 228 | subge0d 10496 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (0 ≤ ((𝐹‘𝑘) − (𝐽‘𝑘)) ↔ (𝐽‘𝑘) ≤ (𝐹‘𝑘))) |
248 | 246, 247 | mpbird 246 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 0 ≤ ((𝐹‘𝑘) − (𝐽‘𝑘))) |
249 | 248, 240 | breqtrrd 4611 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 0 ≤ ((𝐹 ∘𝑓 − 𝐽)‘𝑘)) |
250 | 1, 2, 216, 218, 223, 225, 245, 249 | climsqz2 14220 |
. . . . . 6
⊢ (⊤
→ (𝐹
∘𝑓 − 𝐽) ⇝ 0) |
251 | | ovex 6577 |
. . . . . . 7
⊢ ((𝐹 ∘𝑓
− 𝐽)
∘𝑓 + 𝐽) ∈ V |
252 | 251 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ((𝐹
∘𝑓 − 𝐽) ∘𝑓 + 𝐽) ∈ V) |
253 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐻 ∘𝑓
· ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{-2}) ∘𝑓 · 𝐺))) ∈ V |
254 | 253 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))) ∈ V) |
255 | 68 | recni 9931 |
. . . . . . . . . . 11
⊢ -2 ∈
ℂ |
256 | 54, 255 | basellem7 24613 |
. . . . . . . . . 10
⊢ ((ℕ
× {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)) ⇝ 1 |
257 | 256 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{-2}) ∘𝑓 · 𝐺)) ⇝ 1) |
258 | 74 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓 +
((ℕ × {-2}) ∘𝑓 · 𝐺))‘𝑘) ∈ ℝ) |
259 | 258 | recnd 9947 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓 +
((ℕ × {-2}) ∘𝑓 · 𝐺))‘𝑘) ∈ ℂ) |
260 | | eqidd 2611 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((ℕ × {1}) ∘𝑓 +
((ℕ × {-2}) ∘𝑓 · 𝐺))‘𝑘) = (((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))‘𝑘)) |
261 | 169, 205,
57, 57, 58, 173, 260 | ofval 6804 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺)))‘𝑘) = ((𝐻‘𝑘) · (((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))‘𝑘))) |
262 | 1, 2, 134, 254, 257, 164, 259, 261 | climmul 14211 |
. . . . . . . 8
⊢ (⊤
→ (𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))) ⇝ (((π↑2) / 6) ·
1)) |
263 | 262, 132 | syl6breq 4624 |
. . . . . . 7
⊢ (⊤
→ (𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))) ⇝ ((π↑2) /
6)) |
264 | 76, 263 | syl5eqbr 4618 |
. . . . . 6
⊢ (⊤
→ 𝐽 ⇝
((π↑2) / 6)) |
265 | 225 | recnd 9947 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐹
∘𝑓 − 𝐽)‘𝑘) ∈ ℂ) |
266 | 228 | recnd 9947 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐽‘𝑘) ∈ ℂ) |
267 | | ffn 5958 |
. . . . . . . 8
⊢ ((𝐹 ∘𝑓
− 𝐽):ℕ⟶ℝ → (𝐹 ∘𝑓
− 𝐽) Fn
ℕ) |
268 | 224, 267 | syl 17 |
. . . . . . 7
⊢ (⊤
→ (𝐹
∘𝑓 − 𝐽) Fn ℕ) |
269 | | eqidd 2611 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐹
∘𝑓 − 𝐽)‘𝑘) = ((𝐹 ∘𝑓 − 𝐽)‘𝑘)) |
270 | 268, 237,
57, 57, 58, 269, 239 | ofval 6804 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (((𝐹
∘𝑓 − 𝐽) ∘𝑓 + 𝐽)‘𝑘) = (((𝐹 ∘𝑓 − 𝐽)‘𝑘) + (𝐽‘𝑘))) |
271 | 1, 2, 250, 252, 264, 265, 266, 270 | climadd 14210 |
. . . . 5
⊢ (⊤
→ ((𝐹
∘𝑓 − 𝐽) ∘𝑓 + 𝐽) ⇝ (0 + ((π↑2) /
6))) |
272 | 89, 271 | eqbrtrrd 4607 |
. . . 4
⊢ (⊤
→ 𝐹 ⇝ (0 +
((π↑2) / 6))) |
273 | 101 | addid2i 10103 |
. . . 4
⊢ (0 +
((π↑2) / 6)) = ((π↑2) / 6) |
274 | 272, 21, 273 | 3brtr3g 4616 |
. . 3
⊢ (⊤
→ seq1( + , (𝑛 ∈
ℕ ↦ (𝑛↑-2))) ⇝ ((π↑2) /
6)) |
275 | 1, 2, 7, 19, 274 | isumclim 14330 |
. 2
⊢ (⊤
→ Σ𝑘 ∈
ℕ (𝑘↑-2) =
((π↑2) / 6)) |
276 | 275 | trud 1484 |
1
⊢
Σ𝑘 ∈
ℕ (𝑘↑-2) =
((π↑2) / 6) |