MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  basellem9 Structured version   Visualization version   GIF version
Theorem basellem9 26583
Description: Lemma for basel 26584. Since by basellem8 26582 𝐹 is bounded by two expressions that tend to π↑2 / 6, 𝐹 must also go to π↑2 / 6 by the squeeze theorem climsqz 15582. But the series 𝐹 is exactly the partial sums of π‘˜β†‘-2, so it follows that this is also the value of the infinite sum Ξ£π‘˜ ∈ β„•(π‘˜β†‘-2). (Contributed by Mario Carneiro, 28-Jul-2014.)
Hypotheses
Ref Expression
basel.g 𝐺 = (𝑛 ∈ β„• ↦ (1 / ((2 Β· 𝑛) + 1)))
basel.f 𝐹 = seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2)))
basel.h 𝐻 = ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺))
basel.j 𝐽 = (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))
basel.k 𝐾 = (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺))
Assertion
Ref Expression
basellem9 Ξ£π‘˜ ∈ β„• (π‘˜β†‘-2) = ((π↑2) / 6)
Distinct variable groups:   π‘˜,𝑛,𝐹   π‘˜,𝐺   π‘˜,𝐻   π‘˜,𝐽,𝑛   π‘˜,𝐾
Allowed substitution hints:   𝐺(𝑛)   𝐻(𝑛)   𝐾(𝑛)
Proof of Theorem basellem9
Dummy variables π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12862 . . 3 β„• = (β„€β‰₯β€˜1)
2 1zzd 12590 . . 3 (⊀ β†’ 1 ∈ β„€)
3 oveq1 7413 . . . . 5 (𝑛 = π‘˜ β†’ (𝑛↑-2) = (π‘˜β†‘-2))
4 eqid 2733 . . . . 5 (𝑛 ∈ β„• ↦ (𝑛↑-2)) = (𝑛 ∈ β„• ↦ (𝑛↑-2))
5 ovex 7439 . . . . 5 (π‘˜β†‘-2) ∈ V
63, 4, 5fvmpt 6996 . . . 4 (π‘˜ ∈ β„• β†’ ((𝑛 ∈ β„• ↦ (𝑛↑-2))β€˜π‘˜) = (π‘˜β†‘-2))
76adantl 483 . . 3 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (𝑛↑-2))β€˜π‘˜) = (π‘˜β†‘-2))
8 nnre 12216 . . . . . . . . 9 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ)
9 nnne0 12243 . . . . . . . . 9 (𝑛 ∈ β„• β†’ 𝑛 β‰  0)
10 2z 12591 . . . . . . . . . . 11 2 ∈ β„€
11 znegcl 12594 . . . . . . . . . . 11 (2 ∈ β„€ β†’ -2 ∈ β„€)
1210, 11ax-mp 5 . . . . . . . . . 10 -2 ∈ β„€
1312a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ -2 ∈ β„€)
148, 9, 13reexpclzd 14209 . . . . . . . 8 (𝑛 ∈ β„• β†’ (𝑛↑-2) ∈ ℝ)
1514adantl 483 . . . . . . 7 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (𝑛↑-2) ∈ ℝ)
1615, 4fmptd 7111 . . . . . 6 (⊀ β†’ (𝑛 ∈ β„• ↦ (𝑛↑-2)):β„•βŸΆβ„)
1716ffvelcdmda 7084 . . . . 5 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (𝑛↑-2))β€˜π‘˜) ∈ ℝ)
187, 17eqeltrrd 2835 . . . 4 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π‘˜β†‘-2) ∈ ℝ)
1918recnd 11239 . . 3 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π‘˜β†‘-2) ∈ β„‚)
201, 2, 17serfre 13994 . . . . . . . . . . 11 (⊀ β†’ seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2))):β„•βŸΆβ„)
21 basel.f . . . . . . . . . . . 12 𝐹 = seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2)))
2221feq1i 6706 . . . . . . . . . . 11 (𝐹:β„•βŸΆβ„ ↔ seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2))):β„•βŸΆβ„)
2320, 22sylibr 233 . . . . . . . . . 10 (⊀ β†’ 𝐹:β„•βŸΆβ„)
2423ffvelcdmda 7084 . . . . . . . . 9 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ ℝ)
2524recnd 11239 . . . . . . . 8 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ β„‚)
26 remulcl 11192 . . . . . . . . . . . . 13 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ Β· 𝑦) ∈ ℝ)
2726adantl 483 . . . . . . . . . . . 12 ((⊀ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)) β†’ (π‘₯ Β· 𝑦) ∈ ℝ)
28 ovex 7439 . . . . . . . . . . . . . . . 16 ((π↑2) / 6) ∈ V
2928fconst 6775 . . . . . . . . . . . . . . 15 (β„• Γ— {((π↑2) / 6)}):β„•βŸΆ{((π↑2) / 6)}
30 pire 25960 . . . . . . . . . . . . . . . . . . 19 Ο€ ∈ ℝ
3130resqcli 14147 . . . . . . . . . . . . . . . . . 18 (π↑2) ∈ ℝ
32 6re 12299 . . . . . . . . . . . . . . . . . 18 6 ∈ ℝ
33 6nn 12298 . . . . . . . . . . . . . . . . . . 19 6 ∈ β„•
3433nnne0i 12249 . . . . . . . . . . . . . . . . . 18 6 β‰  0
3531, 32, 34redivcli 11978 . . . . . . . . . . . . . . . . 17 ((π↑2) / 6) ∈ ℝ
3635a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ ((π↑2) / 6) ∈ ℝ)
3736snssd 4812 . . . . . . . . . . . . . . 15 (⊀ β†’ {((π↑2) / 6)} βŠ† ℝ)
38 fss 6732 . . . . . . . . . . . . . . 15 (((β„• Γ— {((π↑2) / 6)}):β„•βŸΆ{((π↑2) / 6)} ∧ {((π↑2) / 6)} βŠ† ℝ) β†’ (β„• Γ— {((π↑2) / 6)}):β„•βŸΆβ„)
3929, 37, 38sylancr 588 . . . . . . . . . . . . . 14 (⊀ β†’ (β„• Γ— {((π↑2) / 6)}):β„•βŸΆβ„)
40 resubcl 11521 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ βˆ’ 𝑦) ∈ ℝ)
4140adantl 483 . . . . . . . . . . . . . . 15 ((⊀ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)) β†’ (π‘₯ βˆ’ 𝑦) ∈ ℝ)
42 1ex 11207 . . . . . . . . . . . . . . . . 17 1 ∈ V
4342fconst 6775 . . . . . . . . . . . . . . . 16 (β„• Γ— {1}):β„•βŸΆ{1}
44 1red 11212 . . . . . . . . . . . . . . . . 17 (⊀ β†’ 1 ∈ ℝ)
4544snssd 4812 . . . . . . . . . . . . . . . 16 (⊀ β†’ {1} βŠ† ℝ)
46 fss 6732 . . . . . . . . . . . . . . . 16 (((β„• Γ— {1}):β„•βŸΆ{1} ∧ {1} βŠ† ℝ) β†’ (β„• Γ— {1}):β„•βŸΆβ„)
4743, 45, 46sylancr 588 . . . . . . . . . . . . . . 15 (⊀ β†’ (β„• Γ— {1}):β„•βŸΆβ„)
48 2nn 12282 . . . . . . . . . . . . . . . . . . . 20 2 ∈ β„•
4948a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊀ β†’ 2 ∈ β„•)
50 nnmulcl 12233 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ β„• ∧ 𝑛 ∈ β„•) β†’ (2 Β· 𝑛) ∈ β„•)
5149, 50sylan 581 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (2 Β· 𝑛) ∈ β„•)
5251peano2nnd 12226 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ 𝑛 ∈ β„•) β†’ ((2 Β· 𝑛) + 1) ∈ β„•)
5352nnrecred 12260 . . . . . . . . . . . . . . . 16 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (1 / ((2 Β· 𝑛) + 1)) ∈ ℝ)
54 basel.g . . . . . . . . . . . . . . . 16 𝐺 = (𝑛 ∈ β„• ↦ (1 / ((2 Β· 𝑛) + 1)))
5553, 54fmptd 7111 . . . . . . . . . . . . . . 15 (⊀ β†’ 𝐺:β„•βŸΆβ„)
56 nnex 12215 . . . . . . . . . . . . . . . 16 β„• ∈ V
5756a1i 11 . . . . . . . . . . . . . . 15 (⊀ β†’ β„• ∈ V)
58 inidm 4218 . . . . . . . . . . . . . . 15 (β„• ∩ β„•) = β„•
5941, 47, 55, 57, 57, 58off 7685 . . . . . . . . . . . . . 14 (⊀ β†’ ((β„• Γ— {1}) ∘f βˆ’ 𝐺):β„•βŸΆβ„)
6027, 39, 59, 57, 57, 58off 7685 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)):β„•βŸΆβ„)
61 basel.h . . . . . . . . . . . . . 14 𝐻 = ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺))
6261feq1i 6706 . . . . . . . . . . . . 13 (𝐻:β„•βŸΆβ„ ↔ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)):β„•βŸΆβ„)
6360, 62sylibr 233 . . . . . . . . . . . 12 (⊀ β†’ 𝐻:β„•βŸΆβ„)
64 readdcl 11190 . . . . . . . . . . . . . 14 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ + 𝑦) ∈ ℝ)
6564adantl 483 . . . . . . . . . . . . 13 ((⊀ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)) β†’ (π‘₯ + 𝑦) ∈ ℝ)
66 negex 11455 . . . . . . . . . . . . . . . 16 -2 ∈ V
6766fconst 6775 . . . . . . . . . . . . . . 15 (β„• Γ— {-2}):β„•βŸΆ{-2}
6812zrei 12561 . . . . . . . . . . . . . . . . 17 -2 ∈ ℝ
6968a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ -2 ∈ ℝ)
7069snssd 4812 . . . . . . . . . . . . . . 15 (⊀ β†’ {-2} βŠ† ℝ)
71 fss 6732 . . . . . . . . . . . . . . 15 (((β„• Γ— {-2}):β„•βŸΆ{-2} ∧ {-2} βŠ† ℝ) β†’ (β„• Γ— {-2}):β„•βŸΆβ„)
7267, 70, 71sylancr 588 . . . . . . . . . . . . . 14 (⊀ β†’ (β„• Γ— {-2}):β„•βŸΆβ„)
7327, 72, 55, 57, 57, 58off 7685 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {-2}) ∘f Β· 𝐺):β„•βŸΆβ„)
7465, 47, 73, 57, 57, 58off 7685 . . . . . . . . . . . 12 (⊀ β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)):β„•βŸΆβ„)
7527, 63, 74, 57, 57, 58off 7685 . . . . . . . . . . 11 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))):β„•βŸΆβ„)
76 basel.j . . . . . . . . . . . 12 𝐽 = (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))
7776feq1i 6706 . . . . . . . . . . 11 (𝐽:β„•βŸΆβ„ ↔ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))):β„•βŸΆβ„)
7875, 77sylibr 233 . . . . . . . . . 10 (⊀ β†’ 𝐽:β„•βŸΆβ„)
7978ffvelcdmda 7084 . . . . . . . . 9 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (π½β€˜π‘›) ∈ ℝ)
8079recnd 11239 . . . . . . . 8 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (π½β€˜π‘›) ∈ β„‚)
8125, 80npcand 11572 . . . . . . 7 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›)) + (π½β€˜π‘›)) = (πΉβ€˜π‘›))
8281mpteq2dva 5248 . . . . . 6 (⊀ β†’ (𝑛 ∈ β„• ↦ (((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›)) + (π½β€˜π‘›))) = (𝑛 ∈ β„• ↦ (πΉβ€˜π‘›)))
83 ovexd 7441 . . . . . . 7 ((⊀ ∧ 𝑛 ∈ β„•) β†’ ((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›)) ∈ V)
8423feqmptd 6958 . . . . . . . 8 (⊀ β†’ 𝐹 = (𝑛 ∈ β„• ↦ (πΉβ€˜π‘›)))
8578feqmptd 6958 . . . . . . . 8 (⊀ β†’ 𝐽 = (𝑛 ∈ β„• ↦ (π½β€˜π‘›)))
8657, 24, 79, 84, 85offval2 7687 . . . . . . 7 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽) = (𝑛 ∈ β„• ↦ ((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›))))
8757, 83, 79, 86, 85offval2 7687 . . . . . 6 (⊀ β†’ ((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽) = (𝑛 ∈ β„• ↦ (((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›)) + (π½β€˜π‘›))))
8882, 87, 843eqtr4d 2783 . . . . 5 (⊀ β†’ ((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽) = 𝐹)
8965, 47, 55, 57, 57, 58off 7685 . . . . . . . . . 10 (⊀ β†’ ((β„• Γ— {1}) ∘f + 𝐺):β„•βŸΆβ„)
90 recn 11197 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ π‘₯ ∈ β„‚)
91 recn 11197 . . . . . . . . . . . 12 (𝑦 ∈ ℝ β†’ 𝑦 ∈ β„‚)
92 recn 11197 . . . . . . . . . . . 12 (𝑧 ∈ ℝ β†’ 𝑧 ∈ β„‚)
93 subdi 11644 . . . . . . . . . . . 12 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ (π‘₯ Β· (𝑦 βˆ’ 𝑧)) = ((π‘₯ Β· 𝑦) βˆ’ (π‘₯ Β· 𝑧)))
9490, 91, 92, 93syl3an 1161 . . . . . . . . . . 11 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ (π‘₯ Β· (𝑦 βˆ’ 𝑧)) = ((π‘₯ Β· 𝑦) βˆ’ (π‘₯ Β· 𝑧)))
9594adantl 483 . . . . . . . . . 10 ((⊀ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) β†’ (π‘₯ Β· (𝑦 βˆ’ 𝑧)) = ((π‘₯ Β· 𝑦) βˆ’ (π‘₯ Β· 𝑧)))
9657, 63, 89, 74, 95caofdi 7706 . . . . . . . . 9 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) = ((𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺)) ∘f βˆ’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))))
97 basel.k . . . . . . . . . 10 𝐾 = (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺))
9897, 76oveq12i 7418 . . . . . . . . 9 (𝐾 ∘f βˆ’ 𝐽) = ((𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺)) ∘f βˆ’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))))
9996, 98eqtr4di 2791 . . . . . . . 8 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) = (𝐾 ∘f βˆ’ 𝐽))
10035recni 11225 . . . . . . . . . . . . . 14 ((π↑2) / 6) ∈ β„‚
1011eqimss2i 4043 . . . . . . . . . . . . . . 15 (β„€β‰₯β€˜1) βŠ† β„•
102101, 56climconst2 15489 . . . . . . . . . . . . . 14 ((((π↑2) / 6) ∈ β„‚ ∧ 1 ∈ β„€) β†’ (β„• Γ— {((π↑2) / 6)}) ⇝ ((π↑2) / 6))
103100, 2, 102sylancr 588 . . . . . . . . . . . . 13 (⊀ β†’ (β„• Γ— {((π↑2) / 6)}) ⇝ ((π↑2) / 6))
104 ovexd 7441 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)) ∈ V)
105 ax-resscn 11164 . . . . . . . . . . . . . . . 16 ℝ βŠ† β„‚
106 fss 6732 . . . . . . . . . . . . . . . 16 (((β„• Γ— {1}):β„•βŸΆβ„ ∧ ℝ βŠ† β„‚) β†’ (β„• Γ— {1}):β„•βŸΆβ„‚)
10747, 105, 106sylancl 587 . . . . . . . . . . . . . . 15 (⊀ β†’ (β„• Γ— {1}):β„•βŸΆβ„‚)
108 fss 6732 . . . . . . . . . . . . . . . 16 ((𝐺:β„•βŸΆβ„ ∧ ℝ βŠ† β„‚) β†’ 𝐺:β„•βŸΆβ„‚)
10955, 105, 108sylancl 587 . . . . . . . . . . . . . . 15 (⊀ β†’ 𝐺:β„•βŸΆβ„‚)
110 ofnegsub 12207 . . . . . . . . . . . . . . 15 ((β„• ∈ V ∧ (β„• Γ— {1}):β„•βŸΆβ„‚ ∧ 𝐺:β„•βŸΆβ„‚) β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-1}) ∘f Β· 𝐺)) = ((β„• Γ— {1}) ∘f βˆ’ 𝐺))
11156, 107, 109, 110mp3an2i 1467 . . . . . . . . . . . . . 14 (⊀ β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-1}) ∘f Β· 𝐺)) = ((β„• Γ— {1}) ∘f βˆ’ 𝐺))
112 neg1cn 12323 . . . . . . . . . . . . . . 15 -1 ∈ β„‚
11354, 112basellem7 26581 . . . . . . . . . . . . . 14 ((β„• Γ— {1}) ∘f + ((β„• Γ— {-1}) ∘f Β· 𝐺)) ⇝ 1
114111, 113eqbrtrrdi 5188 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {1}) ∘f βˆ’ 𝐺) ⇝ 1)
11539ffvelcdmda 7084 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {((π↑2) / 6)})β€˜π‘˜) ∈ ℝ)
116115recnd 11239 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {((π↑2) / 6)})β€˜π‘˜) ∈ β„‚)
11759ffvelcdmda 7084 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜) ∈ ℝ)
118117recnd 11239 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜) ∈ β„‚)
11939ffnd 6716 . . . . . . . . . . . . . 14 (⊀ β†’ (β„• Γ— {((π↑2) / 6)}) Fn β„•)
120 fnconstg 6777 . . . . . . . . . . . . . . . 16 (1 ∈ β„€ β†’ (β„• Γ— {1}) Fn β„•)
1212, 120syl 17 . . . . . . . . . . . . . . 15 (⊀ β†’ (β„• Γ— {1}) Fn β„•)
12255ffnd 6716 . . . . . . . . . . . . . . 15 (⊀ β†’ 𝐺 Fn β„•)
123121, 122, 57, 57, 58offn 7680 . . . . . . . . . . . . . 14 (⊀ β†’ ((β„• Γ— {1}) ∘f βˆ’ 𝐺) Fn β„•)
124 eqidd 2734 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {((π↑2) / 6)})β€˜π‘˜) = ((β„• Γ— {((π↑2) / 6)})β€˜π‘˜))
125 eqidd 2734 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜) = (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜))
126119, 123, 57, 57, 58, 124, 125ofval 7678 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺))β€˜π‘˜) = (((β„• Γ— {((π↑2) / 6)})β€˜π‘˜) Β· (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜)))
1271, 2, 103, 104, 114, 116, 118, 126climmul 15574 . . . . . . . . . . . 12 (⊀ β†’ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)) ⇝ (((π↑2) / 6) Β· 1))
128100mulridi 11215 . . . . . . . . . . . 12 (((π↑2) / 6) Β· 1) = ((π↑2) / 6)
129127, 128breqtrdi 5189 . . . . . . . . . . 11 (⊀ β†’ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)) ⇝ ((π↑2) / 6))
13061, 129eqbrtrid 5183 . . . . . . . . . 10 (⊀ β†’ 𝐻 ⇝ ((π↑2) / 6))
131 ovexd 7441 . . . . . . . . . 10 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) ∈ V)
132 3cn 12290 . . . . . . . . . . . . 13 3 ∈ β„‚
133101, 56climconst2 15489 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ 1 ∈ β„€) β†’ (β„• Γ— {3}) ⇝ 3)
134132, 2, 133sylancr 588 . . . . . . . . . . . 12 (⊀ β†’ (β„• Γ— {3}) ⇝ 3)
135 ovexd 7441 . . . . . . . . . . . 12 (⊀ β†’ ((β„• Γ— {3}) ∘f Β· 𝐺) ∈ V)
13654basellem6 26580 . . . . . . . . . . . . 13 𝐺 ⇝ 0
137136a1i 11 . . . . . . . . . . . 12 (⊀ β†’ 𝐺 ⇝ 0)
138 3ex 12291 . . . . . . . . . . . . . . . 16 3 ∈ V
139138fconst 6775 . . . . . . . . . . . . . . 15 (β„• Γ— {3}):β„•βŸΆ{3}
140 3re 12289 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ
141140a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ 3 ∈ ℝ)
142141snssd 4812 . . . . . . . . . . . . . . 15 (⊀ β†’ {3} βŠ† ℝ)
143 fss 6732 . . . . . . . . . . . . . . 15 (((β„• Γ— {3}):β„•βŸΆ{3} ∧ {3} βŠ† ℝ) β†’ (β„• Γ— {3}):β„•βŸΆβ„)
144139, 142, 143sylancr 588 . . . . . . . . . . . . . 14 (⊀ β†’ (β„• Γ— {3}):β„•βŸΆβ„)
145144ffvelcdmda 7084 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {3})β€˜π‘˜) ∈ ℝ)
146145recnd 11239 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {3})β€˜π‘˜) ∈ β„‚)
14755ffvelcdmda 7084 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) ∈ ℝ)
148147recnd 11239 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) ∈ β„‚)
149144ffnd 6716 . . . . . . . . . . . . 13 (⊀ β†’ (β„• Γ— {3}) Fn β„•)
150 eqidd 2734 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {3})β€˜π‘˜) = ((β„• Γ— {3})β€˜π‘˜))
151 eqidd 2734 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) = (πΊβ€˜π‘˜))
152149, 122, 57, 57, 58, 150, 151ofval 7678 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜) = (((β„• Γ— {3})β€˜π‘˜) Β· (πΊβ€˜π‘˜)))
1531, 2, 134, 135, 137, 146, 148, 152climmul 15574 . . . . . . . . . . 11 (⊀ β†’ ((β„• Γ— {3}) ∘f Β· 𝐺) ⇝ (3 Β· 0))
154132mul01i 11401 . . . . . . . . . . 11 (3 Β· 0) = 0
155153, 154breqtrdi 5189 . . . . . . . . . 10 (⊀ β†’ ((β„• Γ— {3}) ∘f Β· 𝐺) ⇝ 0)
15663ffvelcdmda 7084 . . . . . . . . . . 11 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜π‘˜) ∈ ℝ)
157156recnd 11239 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜π‘˜) ∈ β„‚)
15827, 144, 55, 57, 57, 58off 7685 . . . . . . . . . . . 12 (⊀ β†’ ((β„• Γ— {3}) ∘f Β· 𝐺):β„•βŸΆβ„)
159158ffvelcdmda 7084 . . . . . . . . . . 11 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜) ∈ ℝ)
160159recnd 11239 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜) ∈ β„‚)
16163ffnd 6716 . . . . . . . . . . 11 (⊀ β†’ 𝐻 Fn β„•)
16241, 89, 74, 57, 57, 58off 7685 . . . . . . . . . . . 12 (⊀ β†’ (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))):β„•βŸΆβ„)
163162ffnd 6716 . . . . . . . . . . 11 (⊀ β†’ (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))) Fn β„•)
164 eqidd 2734 . . . . . . . . . . 11 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜π‘˜) = (π»β€˜π‘˜))
165148mullidd 11229 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (1 Β· (πΊβ€˜π‘˜)) = (πΊβ€˜π‘˜))
166 2cn 12284 . . . . . . . . . . . . . . . . . 18 2 ∈ β„‚
167 mulneg1 11647 . . . . . . . . . . . . . . . . . 18 ((2 ∈ β„‚ ∧ (πΊβ€˜π‘˜) ∈ β„‚) β†’ (-2 Β· (πΊβ€˜π‘˜)) = -(2 Β· (πΊβ€˜π‘˜)))
168166, 148, 167sylancr 588 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (-2 Β· (πΊβ€˜π‘˜)) = -(2 Β· (πΊβ€˜π‘˜)))
169168negeqd 11451 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘˜ ∈ β„•) β†’ -(-2 Β· (πΊβ€˜π‘˜)) = --(2 Β· (πΊβ€˜π‘˜)))
170 mulcl 11191 . . . . . . . . . . . . . . . . . 18 ((2 ∈ β„‚ ∧ (πΊβ€˜π‘˜) ∈ β„‚) β†’ (2 Β· (πΊβ€˜π‘˜)) ∈ β„‚)
171166, 148, 170sylancr 588 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (πΊβ€˜π‘˜)) ∈ β„‚)
172171negnegd 11559 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘˜ ∈ β„•) β†’ --(2 Β· (πΊβ€˜π‘˜)) = (2 Β· (πΊβ€˜π‘˜)))
173169, 172eqtr2d 2774 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (πΊβ€˜π‘˜)) = -(-2 Β· (πΊβ€˜π‘˜)))
174165, 173oveq12d 7424 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 Β· (πΊβ€˜π‘˜)) + (2 Β· (πΊβ€˜π‘˜))) = ((πΊβ€˜π‘˜) + -(-2 Β· (πΊβ€˜π‘˜))))
175 remulcl 11192 . . . . . . . . . . . . . . . . 17 ((-2 ∈ ℝ ∧ (πΊβ€˜π‘˜) ∈ ℝ) β†’ (-2 Β· (πΊβ€˜π‘˜)) ∈ ℝ)
17668, 147, 175sylancr 588 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (-2 Β· (πΊβ€˜π‘˜)) ∈ ℝ)
177176recnd 11239 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (-2 Β· (πΊβ€˜π‘˜)) ∈ β„‚)
178148, 177negsubd 11574 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((πΊβ€˜π‘˜) + -(-2 Β· (πΊβ€˜π‘˜))) = ((πΊβ€˜π‘˜) βˆ’ (-2 Β· (πΊβ€˜π‘˜))))
179174, 178eqtrd 2773 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 Β· (πΊβ€˜π‘˜)) + (2 Β· (πΊβ€˜π‘˜))) = ((πΊβ€˜π‘˜) βˆ’ (-2 Β· (πΊβ€˜π‘˜))))
180 df-3 12273 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
181 ax-1cn 11165 . . . . . . . . . . . . . . . . 17 1 ∈ β„‚
182166, 181addcomi 11402 . . . . . . . . . . . . . . . 16 (2 + 1) = (1 + 2)
183180, 182eqtri 2761 . . . . . . . . . . . . . . 15 3 = (1 + 2)
184183oveq1i 7416 . . . . . . . . . . . . . 14 (3 Β· (πΊβ€˜π‘˜)) = ((1 + 2) Β· (πΊβ€˜π‘˜))
185 1cnd 11206 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ 1 ∈ β„‚)
186166a1i 11 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„‚)
187185, 186, 148adddird 11236 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 + 2) Β· (πΊβ€˜π‘˜)) = ((1 Β· (πΊβ€˜π‘˜)) + (2 Β· (πΊβ€˜π‘˜))))
188184, 187eqtrid 2785 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (3 Β· (πΊβ€˜π‘˜)) = ((1 Β· (πΊβ€˜π‘˜)) + (2 Β· (πΊβ€˜π‘˜))))
189185, 148, 177pnpcand 11605 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 + (πΊβ€˜π‘˜)) βˆ’ (1 + (-2 Β· (πΊβ€˜π‘˜)))) = ((πΊβ€˜π‘˜) βˆ’ (-2 Β· (πΊβ€˜π‘˜))))
190179, 188, 1893eqtr4rd 2784 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 + (πΊβ€˜π‘˜)) βˆ’ (1 + (-2 Β· (πΊβ€˜π‘˜)))) = (3 Β· (πΊβ€˜π‘˜)))
191121, 122, 57, 57, 58offn 7680 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {1}) ∘f + 𝐺) Fn β„•)
19212a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ -2 ∈ β„€)
193 fnconstg 6777 . . . . . . . . . . . . . . . 16 (-2 ∈ β„€ β†’ (β„• Γ— {-2}) Fn β„•)
194192, 193syl 17 . . . . . . . . . . . . . . 15 (⊀ β†’ (β„• Γ— {-2}) Fn β„•)
195194, 122, 57, 57, 58offn 7680 . . . . . . . . . . . . . 14 (⊀ β†’ ((β„• Γ— {-2}) ∘f Β· 𝐺) Fn β„•)
196121, 195, 57, 57, 58offn 7680 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)) Fn β„•)
19757, 44, 122, 151ofc1 7693 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + 𝐺)β€˜π‘˜) = (1 + (πΊβ€˜π‘˜)))
19857, 69, 122, 151ofc1 7693 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {-2}) ∘f Β· 𝐺)β€˜π‘˜) = (-2 Β· (πΊβ€˜π‘˜)))
19957, 44, 195, 198ofc1 7693 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜) = (1 + (-2 Β· (πΊβ€˜π‘˜))))
200191, 196, 57, 57, 58, 197, 199ofval 7678 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))β€˜π‘˜) = ((1 + (πΊβ€˜π‘˜)) βˆ’ (1 + (-2 Β· (πΊβ€˜π‘˜)))))
20157, 141, 122, 151ofc1 7693 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜) = (3 Β· (πΊβ€˜π‘˜)))
202190, 200, 2013eqtr4d 2783 . . . . . . . . . . 11 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))β€˜π‘˜) = (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜))
203161, 163, 57, 57, 58, 164, 202ofval 7678 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))))β€˜π‘˜) = ((π»β€˜π‘˜) Β· (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜)))
2041, 2, 130, 131, 155, 157, 160, 203climmul 15574 . . . . . . . . 9 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) ⇝ (((π↑2) / 6) Β· 0))
205100mul01i 11401 . . . . . . . . 9 (((π↑2) / 6) Β· 0) = 0
206204, 205breqtrdi 5189 . . . . . . . 8 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) ⇝ 0)
20799, 206eqbrtrrd 5172 . . . . . . 7 (⊀ β†’ (𝐾 ∘f βˆ’ 𝐽) ⇝ 0)
208 ovexd 7441 . . . . . . 7 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽) ∈ V)
20927, 63, 89, 57, 57, 58off 7685 . . . . . . . . . 10 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺)):β„•βŸΆβ„)
21097feq1i 6706 . . . . . . . . . 10 (𝐾:β„•βŸΆβ„ ↔ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺)):β„•βŸΆβ„)
211209, 210sylibr 233 . . . . . . . . 9 (⊀ β†’ 𝐾:β„•βŸΆβ„)
21241, 211, 78, 57, 57, 58off 7685 . . . . . . . 8 (⊀ β†’ (𝐾 ∘f βˆ’ 𝐽):β„•βŸΆβ„)
213212ffvelcdmda 7084 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐾 ∘f βˆ’ 𝐽)β€˜π‘˜) ∈ ℝ)
21441, 23, 78, 57, 57, 58off 7685 . . . . . . . 8 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽):β„•βŸΆβ„)
215214ffvelcdmda 7084 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) ∈ ℝ)
21623ffvelcdmda 7084 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ ℝ)
217211ffvelcdmda 7084 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΎβ€˜π‘˜) ∈ ℝ)
21878ffvelcdmda 7084 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ∈ ℝ)
219 eqid 2733 . . . . . . . . . . . 12 ((2 Β· π‘˜) + 1) = ((2 Β· π‘˜) + 1)
22054, 21, 61, 76, 97, 219basellem8 26582 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ ((π½β€˜π‘˜) ≀ (πΉβ€˜π‘˜) ∧ (πΉβ€˜π‘˜) ≀ (πΎβ€˜π‘˜)))
221220adantl 483 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((π½β€˜π‘˜) ≀ (πΉβ€˜π‘˜) ∧ (πΉβ€˜π‘˜) ≀ (πΎβ€˜π‘˜)))
222221simprd 497 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ≀ (πΎβ€˜π‘˜))
223216, 217, 218, 222lesub1dd 11827 . . . . . . . 8 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)) ≀ ((πΎβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)))
22423ffnd 6716 . . . . . . . . 9 (⊀ β†’ 𝐹 Fn β„•)
22578ffnd 6716 . . . . . . . . 9 (⊀ β†’ 𝐽 Fn β„•)
226 eqidd 2734 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘˜))
227 eqidd 2734 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) = (π½β€˜π‘˜))
228224, 225, 57, 57, 58, 226, 227ofval 7678 . . . . . . . 8 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) = ((πΉβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)))
229211ffnd 6716 . . . . . . . . 9 (⊀ β†’ 𝐾 Fn β„•)
230 eqidd 2734 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΎβ€˜π‘˜) = (πΎβ€˜π‘˜))
231229, 225, 57, 57, 58, 230, 227ofval 7678 . . . . . . . 8 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐾 ∘f βˆ’ 𝐽)β€˜π‘˜) = ((πΎβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)))
232223, 228, 2313brtr4d 5180 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) ≀ ((𝐾 ∘f βˆ’ 𝐽)β€˜π‘˜))
233221simpld 496 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ≀ (πΉβ€˜π‘˜))
234216, 218subge0d 11801 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (0 ≀ ((πΉβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)) ↔ (π½β€˜π‘˜) ≀ (πΉβ€˜π‘˜)))
235233, 234mpbird 257 . . . . . . . 8 ((⊀ ∧ π‘˜ ∈ β„•) β†’ 0 ≀ ((πΉβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)))
236235, 228breqtrrd 5176 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ 0 ≀ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜))
2371, 2, 207, 208, 213, 215, 232, 236climsqz2 15583 . . . . . 6 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽) ⇝ 0)
238 ovexd 7441 . . . . . 6 (⊀ β†’ ((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽) ∈ V)
239 ovexd 7441 . . . . . . . . 9 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))) ∈ V)
24068recni 11225 . . . . . . . . . . 11 -2 ∈ β„‚
24154, 240basellem7 26581 . . . . . . . . . 10 ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)) ⇝ 1
242241a1i 11 . . . . . . . . 9 (⊀ β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)) ⇝ 1)
24374ffvelcdmda 7084 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜) ∈ ℝ)
244243recnd 11239 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜) ∈ β„‚)
245 eqidd 2734 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜) = (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜))
246161, 196, 57, 57, 58, 164, 245ofval 7678 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))β€˜π‘˜) = ((π»β€˜π‘˜) Β· (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜)))
2471, 2, 130, 239, 242, 157, 244, 246climmul 15574 . . . . . . . 8 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))) ⇝ (((π↑2) / 6) Β· 1))
248247, 128breqtrdi 5189 . . . . . . 7 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))) ⇝ ((π↑2) / 6))
24976, 248eqbrtrid 5183 . . . . . 6 (⊀ β†’ 𝐽 ⇝ ((π↑2) / 6))
250215recnd 11239 . . . . . 6 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) ∈ β„‚)
251218recnd 11239 . . . . . 6 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ∈ β„‚)
252214ffnd 6716 . . . . . . 7 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽) Fn β„•)
253 eqidd 2734 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) = ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜))
254252, 225, 57, 57, 58, 253, 227ofval 7678 . . . . . 6 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽)β€˜π‘˜) = (((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) + (π½β€˜π‘˜)))
2551, 2, 237, 238, 249, 250, 251, 254climadd 15573 . . . . 5 (⊀ β†’ ((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽) ⇝ (0 + ((π↑2) / 6)))
25688, 255eqbrtrrd 5172 . . . 4 (⊀ β†’ 𝐹 ⇝ (0 + ((π↑2) / 6)))
257100addlidi 11399 . . . 4 (0 + ((π↑2) / 6)) = ((π↑2) / 6)
258256, 21, 2573brtr3g 5181 . . 3 (⊀ β†’ seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2))) ⇝ ((π↑2) / 6))
2591, 2, 7, 19, 258isumclim 15700 . 2 (⊀ β†’ Ξ£π‘˜ ∈ β„• (π‘˜β†‘-2) = ((π↑2) / 6))
260259mptru 1549 1 Ξ£π‘˜ ∈ β„• (π‘˜β†‘-2) = ((π↑2) / 6)
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  Vcvv 3475   βŠ† wss 3948  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674   Fn wfn 6536  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406   ∘f cof 7665  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   Β· cmul 11112   ≀ cle 11246   βˆ’ cmin 11441  -cneg 11442   / cdiv 11868  β„•cn 12209  2c2 12264  3c3 12265  6c6 12268  β„€cz 12555  β„€β‰₯cuz 12819  seqcseq 13963  β†‘cexp 14024   ⇝ cli 15425  Ξ£csu 15629  Ο€cpi 16007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-oadd 8467  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-dju 9893  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-xnn0 12542  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-tan 16012  df-pi 16013  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-hom 17218  df-cco 17219  df-rest 17365  df-topn 17366  df-0g 17384  df-gsum 17385  df-topgen 17386  df-pt 17387  df-prds 17390  df-xrs 17445  df-qtop 17450  df-imas 17451  df-xps 17453  df-mre 17527  df-mrc 17528  df-acs 17530  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-submnd 18669  df-mulg 18946  df-cntz 19176  df-cmn 19645  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-fbas 20934  df-fg 20935  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-lp 22632  df-perf 22633  df-cn 22723  df-cnp 22724  df-haus 22811  df-tx 23058  df-hmeo 23251  df-fil 23342  df-fm 23434  df-flim 23435  df-flf 23436  df-xms 23818  df-ms 23819  df-tms 23820  df-cncf 24386  df-0p 25179  df-limc 25375  df-dv 25376  df-ply 25694  df-idp 25695  df-coe 25696  df-dgr 25697  df-quot 25796
This theorem is referenced by:  basel  26584
  Copyright terms: Public domain W3C validator