MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  basellem9 Structured version   Visualization version   GIF version
Theorem basellem9 26936
Description: Lemma for basel 26937. Since by basellem8 26935 𝐹 is bounded by two expressions that tend to π↑2 / 6, 𝐹 must also go to π↑2 / 6 by the squeeze theorem climsqz 15581. 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 12861 . . 3 β„• = (β„€β‰₯β€˜1)
2 1zzd 12589 . . 3 (⊀ β†’ 1 ∈ β„€)
3 oveq1 7408 . . . . 5 (𝑛 = π‘˜ β†’ (𝑛↑-2) = (π‘˜β†‘-2))
4 eqid 2724 . . . . 5 (𝑛 ∈ β„• ↦ (𝑛↑-2)) = (𝑛 ∈ β„• ↦ (𝑛↑-2))
5 ovex 7434 . . . . 5 (π‘˜β†‘-2) ∈ V
63, 4, 5fvmpt 6988 . . . 4 (π‘˜ ∈ β„• β†’ ((𝑛 ∈ β„• ↦ (𝑛↑-2))β€˜π‘˜) = (π‘˜β†‘-2))
76adantl 481 . . 3 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (𝑛↑-2))β€˜π‘˜) = (π‘˜β†‘-2))
8 nnre 12215 . . . . . . . . 9 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ)
9 nnne0 12242 . . . . . . . . 9 (𝑛 ∈ β„• β†’ 𝑛 β‰  0)
10 2z 12590 . . . . . . . . . . 11 2 ∈ β„€
11 znegcl 12593 . . . . . . . . . . 11 (2 ∈ β„€ β†’ -2 ∈ β„€)
1210, 11ax-mp 5 . . . . . . . . . 10 -2 ∈ β„€
1312a1i 11 . . . . . . . . 9 (𝑛 ∈ β„• β†’ -2 ∈ β„€)
148, 9, 13reexpclzd 14208 . . . . . . . 8 (𝑛 ∈ β„• β†’ (𝑛↑-2) ∈ ℝ)
1514adantl 481 . . . . . . 7 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (𝑛↑-2) ∈ ℝ)
1615, 4fmptd 7105 . . . . . 6 (⊀ β†’ (𝑛 ∈ β„• ↦ (𝑛↑-2)):β„•βŸΆβ„)
1716ffvelcdmda 7076 . . . . 5 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (𝑛↑-2))β€˜π‘˜) ∈ ℝ)
187, 17eqeltrrd 2826 . . . 4 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π‘˜β†‘-2) ∈ ℝ)
1918recnd 11238 . . 3 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π‘˜β†‘-2) ∈ β„‚)
201, 2, 17serfre 13993 . . . . . . . . . . 11 (⊀ β†’ seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2))):β„•βŸΆβ„)
21 basel.f . . . . . . . . . . . 12 𝐹 = seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2)))
2221feq1i 6698 . . . . . . . . . . 11 (𝐹:β„•βŸΆβ„ ↔ seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2))):β„•βŸΆβ„)
2320, 22sylibr 233 . . . . . . . . . 10 (⊀ β†’ 𝐹:β„•βŸΆβ„)
2423ffvelcdmda 7076 . . . . . . . . 9 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ ℝ)
2524recnd 11238 . . . . . . . 8 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ β„‚)
26 remulcl 11190 . . . . . . . . . . . . 13 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ Β· 𝑦) ∈ ℝ)
2726adantl 481 . . . . . . . . . . . 12 ((⊀ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)) β†’ (π‘₯ Β· 𝑦) ∈ ℝ)
28 ovex 7434 . . . . . . . . . . . . . . . 16 ((π↑2) / 6) ∈ V
2928fconst 6767 . . . . . . . . . . . . . . 15 (β„• Γ— {((π↑2) / 6)}):β„•βŸΆ{((π↑2) / 6)}
30 pire 26309 . . . . . . . . . . . . . . . . . . 19 Ο€ ∈ ℝ
3130resqcli 14146 . . . . . . . . . . . . . . . . . 18 (π↑2) ∈ ℝ
32 6re 12298 . . . . . . . . . . . . . . . . . 18 6 ∈ ℝ
33 6nn 12297 . . . . . . . . . . . . . . . . . . 19 6 ∈ β„•
3433nnne0i 12248 . . . . . . . . . . . . . . . . . 18 6 β‰  0
3531, 32, 34redivcli 11977 . . . . . . . . . . . . . . . . 17 ((π↑2) / 6) ∈ ℝ
3635a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ ((π↑2) / 6) ∈ ℝ)
3736snssd 4804 . . . . . . . . . . . . . . 15 (⊀ β†’ {((π↑2) / 6)} βŠ† ℝ)
38 fss 6724 . . . . . . . . . . . . . . 15 (((β„• Γ— {((π↑2) / 6)}):β„•βŸΆ{((π↑2) / 6)} ∧ {((π↑2) / 6)} βŠ† ℝ) β†’ (β„• Γ— {((π↑2) / 6)}):β„•βŸΆβ„)
3929, 37, 38sylancr 586 . . . . . . . . . . . . . 14 (⊀ β†’ (β„• Γ— {((π↑2) / 6)}):β„•βŸΆβ„)
40 resubcl 11520 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ βˆ’ 𝑦) ∈ ℝ)
4140adantl 481 . . . . . . . . . . . . . . 15 ((⊀ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)) β†’ (π‘₯ βˆ’ 𝑦) ∈ ℝ)
42 1ex 11206 . . . . . . . . . . . . . . . . 17 1 ∈ V
4342fconst 6767 . . . . . . . . . . . . . . . 16 (β„• Γ— {1}):β„•βŸΆ{1}
44 1red 11211 . . . . . . . . . . . . . . . . 17 (⊀ β†’ 1 ∈ ℝ)
4544snssd 4804 . . . . . . . . . . . . . . . 16 (⊀ β†’ {1} βŠ† ℝ)
46 fss 6724 . . . . . . . . . . . . . . . 16 (((β„• Γ— {1}):β„•βŸΆ{1} ∧ {1} βŠ† ℝ) β†’ (β„• Γ— {1}):β„•βŸΆβ„)
4743, 45, 46sylancr 586 . . . . . . . . . . . . . . 15 (⊀ β†’ (β„• Γ— {1}):β„•βŸΆβ„)
48 2nn 12281 . . . . . . . . . . . . . . . . . . . 20 2 ∈ β„•
4948a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊀ β†’ 2 ∈ β„•)
50 nnmulcl 12232 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ β„• ∧ 𝑛 ∈ β„•) β†’ (2 Β· 𝑛) ∈ β„•)
5149, 50sylan 579 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (2 Β· 𝑛) ∈ β„•)
5251peano2nnd 12225 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ 𝑛 ∈ β„•) β†’ ((2 Β· 𝑛) + 1) ∈ β„•)
5352nnrecred 12259 . . . . . . . . . . . . . . . 16 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (1 / ((2 Β· 𝑛) + 1)) ∈ ℝ)
54 basel.g . . . . . . . . . . . . . . . 16 𝐺 = (𝑛 ∈ β„• ↦ (1 / ((2 Β· 𝑛) + 1)))
5553, 54fmptd 7105 . . . . . . . . . . . . . . 15 (⊀ β†’ 𝐺:β„•βŸΆβ„)
56 nnex 12214 . . . . . . . . . . . . . . . 16 β„• ∈ V
5756a1i 11 . . . . . . . . . . . . . . 15 (⊀ β†’ β„• ∈ V)
58 inidm 4210 . . . . . . . . . . . . . . 15 (β„• ∩ β„•) = β„•
5941, 47, 55, 57, 57, 58off 7681 . . . . . . . . . . . . . 14 (⊀ β†’ ((β„• Γ— {1}) ∘f βˆ’ 𝐺):β„•βŸΆβ„)
6027, 39, 59, 57, 57, 58off 7681 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)):β„•βŸΆβ„)
61 basel.h . . . . . . . . . . . . . 14 𝐻 = ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺))
6261feq1i 6698 . . . . . . . . . . . . 13 (𝐻:β„•βŸΆβ„ ↔ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)):β„•βŸΆβ„)
6360, 62sylibr 233 . . . . . . . . . . . 12 (⊀ β†’ 𝐻:β„•βŸΆβ„)
64 readdcl 11188 . . . . . . . . . . . . . 14 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ + 𝑦) ∈ ℝ)
6564adantl 481 . . . . . . . . . . . . 13 ((⊀ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)) β†’ (π‘₯ + 𝑦) ∈ ℝ)
66 negex 11454 . . . . . . . . . . . . . . . 16 -2 ∈ V
6766fconst 6767 . . . . . . . . . . . . . . 15 (β„• Γ— {-2}):β„•βŸΆ{-2}
6812zrei 12560 . . . . . . . . . . . . . . . . 17 -2 ∈ ℝ
6968a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ -2 ∈ ℝ)
7069snssd 4804 . . . . . . . . . . . . . . 15 (⊀ β†’ {-2} βŠ† ℝ)
71 fss 6724 . . . . . . . . . . . . . . 15 (((β„• Γ— {-2}):β„•βŸΆ{-2} ∧ {-2} βŠ† ℝ) β†’ (β„• Γ— {-2}):β„•βŸΆβ„)
7267, 70, 71sylancr 586 . . . . . . . . . . . . . 14 (⊀ β†’ (β„• Γ— {-2}):β„•βŸΆβ„)
7327, 72, 55, 57, 57, 58off 7681 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {-2}) ∘f Β· 𝐺):β„•βŸΆβ„)
7465, 47, 73, 57, 57, 58off 7681 . . . . . . . . . . . 12 (⊀ β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)):β„•βŸΆβ„)
7527, 63, 74, 57, 57, 58off 7681 . . . . . . . . . . 11 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))):β„•βŸΆβ„)
76 basel.j . . . . . . . . . . . 12 𝐽 = (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))
7776feq1i 6698 . . . . . . . . . . 11 (𝐽:β„•βŸΆβ„ ↔ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))):β„•βŸΆβ„)
7875, 77sylibr 233 . . . . . . . . . 10 (⊀ β†’ 𝐽:β„•βŸΆβ„)
7978ffvelcdmda 7076 . . . . . . . . 9 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (π½β€˜π‘›) ∈ ℝ)
8079recnd 11238 . . . . . . . 8 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (π½β€˜π‘›) ∈ β„‚)
8125, 80npcand 11571 . . . . . . 7 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›)) + (π½β€˜π‘›)) = (πΉβ€˜π‘›))
8281mpteq2dva 5238 . . . . . 6 (⊀ β†’ (𝑛 ∈ β„• ↦ (((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›)) + (π½β€˜π‘›))) = (𝑛 ∈ β„• ↦ (πΉβ€˜π‘›)))
83 ovexd 7436 . . . . . . 7 ((⊀ ∧ 𝑛 ∈ β„•) β†’ ((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›)) ∈ V)
8423feqmptd 6950 . . . . . . . 8 (⊀ β†’ 𝐹 = (𝑛 ∈ β„• ↦ (πΉβ€˜π‘›)))
8578feqmptd 6950 . . . . . . . 8 (⊀ β†’ 𝐽 = (𝑛 ∈ β„• ↦ (π½β€˜π‘›)))
8657, 24, 79, 84, 85offval2 7683 . . . . . . 7 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽) = (𝑛 ∈ β„• ↦ ((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›))))
8757, 83, 79, 86, 85offval2 7683 . . . . . 6 (⊀ β†’ ((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽) = (𝑛 ∈ β„• ↦ (((πΉβ€˜π‘›) βˆ’ (π½β€˜π‘›)) + (π½β€˜π‘›))))
8882, 87, 843eqtr4d 2774 . . . . 5 (⊀ β†’ ((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽) = 𝐹)
8965, 47, 55, 57, 57, 58off 7681 . . . . . . . . . 10 (⊀ β†’ ((β„• Γ— {1}) ∘f + 𝐺):β„•βŸΆβ„)
90 recn 11195 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ π‘₯ ∈ β„‚)
91 recn 11195 . . . . . . . . . . . 12 (𝑦 ∈ ℝ β†’ 𝑦 ∈ β„‚)
92 recn 11195 . . . . . . . . . . . 12 (𝑧 ∈ ℝ β†’ 𝑧 ∈ β„‚)
93 subdi 11643 . . . . . . . . . . . 12 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ (π‘₯ Β· (𝑦 βˆ’ 𝑧)) = ((π‘₯ Β· 𝑦) βˆ’ (π‘₯ Β· 𝑧)))
9490, 91, 92, 93syl3an 1157 . . . . . . . . . . 11 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ (π‘₯ Β· (𝑦 βˆ’ 𝑧)) = ((π‘₯ Β· 𝑦) βˆ’ (π‘₯ Β· 𝑧)))
9594adantl 481 . . . . . . . . . 10 ((⊀ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) β†’ (π‘₯ Β· (𝑦 βˆ’ 𝑧)) = ((π‘₯ Β· 𝑦) βˆ’ (π‘₯ Β· 𝑧)))
9657, 63, 89, 74, 95caofdi 7702 . . . . . . . . 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 7413 . . . . . . . . 9 (𝐾 ∘f βˆ’ 𝐽) = ((𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺)) ∘f βˆ’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))))
9996, 98eqtr4di 2782 . . . . . . . 8 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) = (𝐾 ∘f βˆ’ 𝐽))
10035recni 11224 . . . . . . . . . . . . . 14 ((π↑2) / 6) ∈ β„‚
1011eqimss2i 4035 . . . . . . . . . . . . . . 15 (β„€β‰₯β€˜1) βŠ† β„•
102101, 56climconst2 15488 . . . . . . . . . . . . . 14 ((((π↑2) / 6) ∈ β„‚ ∧ 1 ∈ β„€) β†’ (β„• Γ— {((π↑2) / 6)}) ⇝ ((π↑2) / 6))
103100, 2, 102sylancr 586 . . . . . . . . . . . . 13 (⊀ β†’ (β„• Γ— {((π↑2) / 6)}) ⇝ ((π↑2) / 6))
104 ovexd 7436 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)) ∈ V)
105 ax-resscn 11162 . . . . . . . . . . . . . . . 16 ℝ βŠ† β„‚
106 fss 6724 . . . . . . . . . . . . . . . 16 (((β„• Γ— {1}):β„•βŸΆβ„ ∧ ℝ βŠ† β„‚) β†’ (β„• Γ— {1}):β„•βŸΆβ„‚)
10747, 105, 106sylancl 585 . . . . . . . . . . . . . . 15 (⊀ β†’ (β„• Γ— {1}):β„•βŸΆβ„‚)
108 fss 6724 . . . . . . . . . . . . . . . 16 ((𝐺:β„•βŸΆβ„ ∧ ℝ βŠ† β„‚) β†’ 𝐺:β„•βŸΆβ„‚)
10955, 105, 108sylancl 585 . . . . . . . . . . . . . . 15 (⊀ β†’ 𝐺:β„•βŸΆβ„‚)
110 ofnegsub 12206 . . . . . . . . . . . . . . 15 ((β„• ∈ V ∧ (β„• Γ— {1}):β„•βŸΆβ„‚ ∧ 𝐺:β„•βŸΆβ„‚) β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-1}) ∘f Β· 𝐺)) = ((β„• Γ— {1}) ∘f βˆ’ 𝐺))
11156, 107, 109, 110mp3an2i 1462 . . . . . . . . . . . . . 14 (⊀ β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-1}) ∘f Β· 𝐺)) = ((β„• Γ— {1}) ∘f βˆ’ 𝐺))
112 neg1cn 12322 . . . . . . . . . . . . . . 15 -1 ∈ β„‚
11354, 112basellem7 26934 . . . . . . . . . . . . . 14 ((β„• Γ— {1}) ∘f + ((β„• Γ— {-1}) ∘f Β· 𝐺)) ⇝ 1
114111, 113eqbrtrrdi 5178 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {1}) ∘f βˆ’ 𝐺) ⇝ 1)
11539ffvelcdmda 7076 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {((π↑2) / 6)})β€˜π‘˜) ∈ ℝ)
116115recnd 11238 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {((π↑2) / 6)})β€˜π‘˜) ∈ β„‚)
11759ffvelcdmda 7076 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜) ∈ ℝ)
118117recnd 11238 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜) ∈ β„‚)
11939ffnd 6708 . . . . . . . . . . . . . 14 (⊀ β†’ (β„• Γ— {((π↑2) / 6)}) Fn β„•)
120 fnconstg 6769 . . . . . . . . . . . . . . . 16 (1 ∈ β„€ β†’ (β„• Γ— {1}) Fn β„•)
1212, 120syl 17 . . . . . . . . . . . . . . 15 (⊀ β†’ (β„• Γ— {1}) Fn β„•)
12255ffnd 6708 . . . . . . . . . . . . . . 15 (⊀ β†’ 𝐺 Fn β„•)
123121, 122, 57, 57, 58offn 7676 . . . . . . . . . . . . . 14 (⊀ β†’ ((β„• Γ— {1}) ∘f βˆ’ 𝐺) Fn β„•)
124 eqidd 2725 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {((π↑2) / 6)})β€˜π‘˜) = ((β„• Γ— {((π↑2) / 6)})β€˜π‘˜))
125 eqidd 2725 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜) = (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜))
126119, 123, 57, 57, 58, 124, 125ofval 7674 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺))β€˜π‘˜) = (((β„• Γ— {((π↑2) / 6)})β€˜π‘˜) Β· (((β„• Γ— {1}) ∘f βˆ’ 𝐺)β€˜π‘˜)))
1271, 2, 103, 104, 114, 116, 118, 126climmul 15573 . . . . . . . . . . . 12 (⊀ β†’ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)) ⇝ (((π↑2) / 6) Β· 1))
128100mulridi 11214 . . . . . . . . . . . 12 (((π↑2) / 6) Β· 1) = ((π↑2) / 6)
129127, 128breqtrdi 5179 . . . . . . . . . . 11 (⊀ β†’ ((β„• Γ— {((π↑2) / 6)}) ∘f Β· ((β„• Γ— {1}) ∘f βˆ’ 𝐺)) ⇝ ((π↑2) / 6))
13061, 129eqbrtrid 5173 . . . . . . . . . 10 (⊀ β†’ 𝐻 ⇝ ((π↑2) / 6))
131 ovexd 7436 . . . . . . . . . 10 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) ∈ V)
132 3cn 12289 . . . . . . . . . . . . 13 3 ∈ β„‚
133101, 56climconst2 15488 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ 1 ∈ β„€) β†’ (β„• Γ— {3}) ⇝ 3)
134132, 2, 133sylancr 586 . . . . . . . . . . . 12 (⊀ β†’ (β„• Γ— {3}) ⇝ 3)
135 ovexd 7436 . . . . . . . . . . . 12 (⊀ β†’ ((β„• Γ— {3}) ∘f Β· 𝐺) ∈ V)
13654basellem6 26933 . . . . . . . . . . . . 13 𝐺 ⇝ 0
137136a1i 11 . . . . . . . . . . . 12 (⊀ β†’ 𝐺 ⇝ 0)
138 3ex 12290 . . . . . . . . . . . . . . . 16 3 ∈ V
139138fconst 6767 . . . . . . . . . . . . . . 15 (β„• Γ— {3}):β„•βŸΆ{3}
140 3re 12288 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ
141140a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ 3 ∈ ℝ)
142141snssd 4804 . . . . . . . . . . . . . . 15 (⊀ β†’ {3} βŠ† ℝ)
143 fss 6724 . . . . . . . . . . . . . . 15 (((β„• Γ— {3}):β„•βŸΆ{3} ∧ {3} βŠ† ℝ) β†’ (β„• Γ— {3}):β„•βŸΆβ„)
144139, 142, 143sylancr 586 . . . . . . . . . . . . . 14 (⊀ β†’ (β„• Γ— {3}):β„•βŸΆβ„)
145144ffvelcdmda 7076 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {3})β€˜π‘˜) ∈ ℝ)
146145recnd 11238 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {3})β€˜π‘˜) ∈ β„‚)
14755ffvelcdmda 7076 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) ∈ ℝ)
148147recnd 11238 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) ∈ β„‚)
149144ffnd 6708 . . . . . . . . . . . . 13 (⊀ β†’ (β„• Γ— {3}) Fn β„•)
150 eqidd 2725 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((β„• Γ— {3})β€˜π‘˜) = ((β„• Γ— {3})β€˜π‘˜))
151 eqidd 2725 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) = (πΊβ€˜π‘˜))
152149, 122, 57, 57, 58, 150, 151ofval 7674 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜) = (((β„• Γ— {3})β€˜π‘˜) Β· (πΊβ€˜π‘˜)))
1531, 2, 134, 135, 137, 146, 148, 152climmul 15573 . . . . . . . . . . 11 (⊀ β†’ ((β„• Γ— {3}) ∘f Β· 𝐺) ⇝ (3 Β· 0))
154132mul01i 11400 . . . . . . . . . . 11 (3 Β· 0) = 0
155153, 154breqtrdi 5179 . . . . . . . . . 10 (⊀ β†’ ((β„• Γ— {3}) ∘f Β· 𝐺) ⇝ 0)
15663ffvelcdmda 7076 . . . . . . . . . . 11 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜π‘˜) ∈ ℝ)
157156recnd 11238 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜π‘˜) ∈ β„‚)
15827, 144, 55, 57, 57, 58off 7681 . . . . . . . . . . . 12 (⊀ β†’ ((β„• Γ— {3}) ∘f Β· 𝐺):β„•βŸΆβ„)
159158ffvelcdmda 7076 . . . . . . . . . . 11 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜) ∈ ℝ)
160159recnd 11238 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜) ∈ β„‚)
16163ffnd 6708 . . . . . . . . . . 11 (⊀ β†’ 𝐻 Fn β„•)
16241, 89, 74, 57, 57, 58off 7681 . . . . . . . . . . . 12 (⊀ β†’ (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))):β„•βŸΆβ„)
163162ffnd 6708 . . . . . . . . . . 11 (⊀ β†’ (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))) Fn β„•)
164 eqidd 2725 . . . . . . . . . . 11 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π»β€˜π‘˜) = (π»β€˜π‘˜))
165148mullidd 11228 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (1 Β· (πΊβ€˜π‘˜)) = (πΊβ€˜π‘˜))
166 2cn 12283 . . . . . . . . . . . . . . . . . 18 2 ∈ β„‚
167 mulneg1 11646 . . . . . . . . . . . . . . . . . 18 ((2 ∈ β„‚ ∧ (πΊβ€˜π‘˜) ∈ β„‚) β†’ (-2 Β· (πΊβ€˜π‘˜)) = -(2 Β· (πΊβ€˜π‘˜)))
168166, 148, 167sylancr 586 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (-2 Β· (πΊβ€˜π‘˜)) = -(2 Β· (πΊβ€˜π‘˜)))
169168negeqd 11450 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘˜ ∈ β„•) β†’ -(-2 Β· (πΊβ€˜π‘˜)) = --(2 Β· (πΊβ€˜π‘˜)))
170 mulcl 11189 . . . . . . . . . . . . . . . . . 18 ((2 ∈ β„‚ ∧ (πΊβ€˜π‘˜) ∈ β„‚) β†’ (2 Β· (πΊβ€˜π‘˜)) ∈ β„‚)
171166, 148, 170sylancr 586 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (πΊβ€˜π‘˜)) ∈ β„‚)
172171negnegd 11558 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘˜ ∈ β„•) β†’ --(2 Β· (πΊβ€˜π‘˜)) = (2 Β· (πΊβ€˜π‘˜)))
173169, 172eqtr2d 2765 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (πΊβ€˜π‘˜)) = -(-2 Β· (πΊβ€˜π‘˜)))
174165, 173oveq12d 7419 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 Β· (πΊβ€˜π‘˜)) + (2 Β· (πΊβ€˜π‘˜))) = ((πΊβ€˜π‘˜) + -(-2 Β· (πΊβ€˜π‘˜))))
175 remulcl 11190 . . . . . . . . . . . . . . . . 17 ((-2 ∈ ℝ ∧ (πΊβ€˜π‘˜) ∈ ℝ) β†’ (-2 Β· (πΊβ€˜π‘˜)) ∈ ℝ)
17668, 147, 175sylancr 586 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (-2 Β· (πΊβ€˜π‘˜)) ∈ ℝ)
177176recnd 11238 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (-2 Β· (πΊβ€˜π‘˜)) ∈ β„‚)
178148, 177negsubd 11573 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((πΊβ€˜π‘˜) + -(-2 Β· (πΊβ€˜π‘˜))) = ((πΊβ€˜π‘˜) βˆ’ (-2 Β· (πΊβ€˜π‘˜))))
179174, 178eqtrd 2764 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 Β· (πΊβ€˜π‘˜)) + (2 Β· (πΊβ€˜π‘˜))) = ((πΊβ€˜π‘˜) βˆ’ (-2 Β· (πΊβ€˜π‘˜))))
180 df-3 12272 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
181 ax-1cn 11163 . . . . . . . . . . . . . . . . 17 1 ∈ β„‚
182166, 181addcomi 11401 . . . . . . . . . . . . . . . 16 (2 + 1) = (1 + 2)
183180, 182eqtri 2752 . . . . . . . . . . . . . . 15 3 = (1 + 2)
184183oveq1i 7411 . . . . . . . . . . . . . 14 (3 Β· (πΊβ€˜π‘˜)) = ((1 + 2) Β· (πΊβ€˜π‘˜))
185 1cnd 11205 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ 1 ∈ β„‚)
186166a1i 11 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„‚)
187185, 186, 148adddird 11235 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 + 2) Β· (πΊβ€˜π‘˜)) = ((1 Β· (πΊβ€˜π‘˜)) + (2 Β· (πΊβ€˜π‘˜))))
188184, 187eqtrid 2776 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (3 Β· (πΊβ€˜π‘˜)) = ((1 Β· (πΊβ€˜π‘˜)) + (2 Β· (πΊβ€˜π‘˜))))
189185, 148, 177pnpcand 11604 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 + (πΊβ€˜π‘˜)) βˆ’ (1 + (-2 Β· (πΊβ€˜π‘˜)))) = ((πΊβ€˜π‘˜) βˆ’ (-2 Β· (πΊβ€˜π‘˜))))
190179, 188, 1893eqtr4rd 2775 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((1 + (πΊβ€˜π‘˜)) βˆ’ (1 + (-2 Β· (πΊβ€˜π‘˜)))) = (3 Β· (πΊβ€˜π‘˜)))
191121, 122, 57, 57, 58offn 7676 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {1}) ∘f + 𝐺) Fn β„•)
19212a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ -2 ∈ β„€)
193 fnconstg 6769 . . . . . . . . . . . . . . . 16 (-2 ∈ β„€ β†’ (β„• Γ— {-2}) Fn β„•)
194192, 193syl 17 . . . . . . . . . . . . . . 15 (⊀ β†’ (β„• Γ— {-2}) Fn β„•)
195194, 122, 57, 57, 58offn 7676 . . . . . . . . . . . . . 14 (⊀ β†’ ((β„• Γ— {-2}) ∘f Β· 𝐺) Fn β„•)
196121, 195, 57, 57, 58offn 7676 . . . . . . . . . . . . 13 (⊀ β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)) Fn β„•)
19757, 44, 122, 151ofc1 7689 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + 𝐺)β€˜π‘˜) = (1 + (πΊβ€˜π‘˜)))
19857, 69, 122, 151ofc1 7689 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {-2}) ∘f Β· 𝐺)β€˜π‘˜) = (-2 Β· (πΊβ€˜π‘˜)))
19957, 44, 195, 198ofc1 7689 . . . . . . . . . . . . 13 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜) = (1 + (-2 Β· (πΊβ€˜π‘˜))))
200191, 196, 57, 57, 58, 197, 199ofval 7674 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))β€˜π‘˜) = ((1 + (πΊβ€˜π‘˜)) βˆ’ (1 + (-2 Β· (πΊβ€˜π‘˜)))))
20157, 141, 122, 151ofc1 7689 . . . . . . . . . . . 12 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜) = (3 Β· (πΊβ€˜π‘˜)))
202190, 200, 2013eqtr4d 2774 . . . . . . . . . . 11 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))β€˜π‘˜) = (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜))
203161, 163, 57, 57, 58, 164, 202ofval 7674 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))))β€˜π‘˜) = ((π»β€˜π‘˜) Β· (((β„• Γ— {3}) ∘f Β· 𝐺)β€˜π‘˜)))
2041, 2, 130, 131, 155, 157, 160, 203climmul 15573 . . . . . . . . 9 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) ⇝ (((π↑2) / 6) Β· 0))
205100mul01i 11400 . . . . . . . . 9 (((π↑2) / 6) Β· 0) = 0
206204, 205breqtrdi 5179 . . . . . . . 8 (⊀ β†’ (𝐻 ∘f Β· (((β„• Γ— {1}) ∘f + 𝐺) ∘f βˆ’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))) ⇝ 0)
20799, 206eqbrtrrd 5162 . . . . . . 7 (⊀ β†’ (𝐾 ∘f βˆ’ 𝐽) ⇝ 0)
208 ovexd 7436 . . . . . . 7 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽) ∈ V)
20927, 63, 89, 57, 57, 58off 7681 . . . . . . . . . 10 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺)):β„•βŸΆβ„)
21097feq1i 6698 . . . . . . . . . 10 (𝐾:β„•βŸΆβ„ ↔ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + 𝐺)):β„•βŸΆβ„)
211209, 210sylibr 233 . . . . . . . . 9 (⊀ β†’ 𝐾:β„•βŸΆβ„)
21241, 211, 78, 57, 57, 58off 7681 . . . . . . . 8 (⊀ β†’ (𝐾 ∘f βˆ’ 𝐽):β„•βŸΆβ„)
213212ffvelcdmda 7076 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐾 ∘f βˆ’ 𝐽)β€˜π‘˜) ∈ ℝ)
21441, 23, 78, 57, 57, 58off 7681 . . . . . . . 8 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽):β„•βŸΆβ„)
215214ffvelcdmda 7076 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) ∈ ℝ)
21623ffvelcdmda 7076 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ ℝ)
217211ffvelcdmda 7076 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΎβ€˜π‘˜) ∈ ℝ)
21878ffvelcdmda 7076 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ∈ ℝ)
219 eqid 2724 . . . . . . . . . . . 12 ((2 Β· π‘˜) + 1) = ((2 Β· π‘˜) + 1)
22054, 21, 61, 76, 97, 219basellem8 26935 . . . . . . . . . . 11 (π‘˜ ∈ β„• β†’ ((π½β€˜π‘˜) ≀ (πΉβ€˜π‘˜) ∧ (πΉβ€˜π‘˜) ≀ (πΎβ€˜π‘˜)))
221220adantl 481 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((π½β€˜π‘˜) ≀ (πΉβ€˜π‘˜) ∧ (πΉβ€˜π‘˜) ≀ (πΎβ€˜π‘˜)))
222221simprd 495 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ≀ (πΎβ€˜π‘˜))
223216, 217, 218, 222lesub1dd 11826 . . . . . . . 8 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)) ≀ ((πΎβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)))
22423ffnd 6708 . . . . . . . . 9 (⊀ β†’ 𝐹 Fn β„•)
22578ffnd 6708 . . . . . . . . 9 (⊀ β†’ 𝐽 Fn β„•)
226 eqidd 2725 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘˜))
227 eqidd 2725 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) = (π½β€˜π‘˜))
228224, 225, 57, 57, 58, 226, 227ofval 7674 . . . . . . . 8 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) = ((πΉβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)))
229211ffnd 6708 . . . . . . . . 9 (⊀ β†’ 𝐾 Fn β„•)
230 eqidd 2725 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (πΎβ€˜π‘˜) = (πΎβ€˜π‘˜))
231229, 225, 57, 57, 58, 230, 227ofval 7674 . . . . . . . 8 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐾 ∘f βˆ’ 𝐽)β€˜π‘˜) = ((πΎβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)))
232223, 228, 2313brtr4d 5170 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) ≀ ((𝐾 ∘f βˆ’ 𝐽)β€˜π‘˜))
233221simpld 494 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ≀ (πΉβ€˜π‘˜))
234216, 218subge0d 11800 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (0 ≀ ((πΉβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)) ↔ (π½β€˜π‘˜) ≀ (πΉβ€˜π‘˜)))
235233, 234mpbird 257 . . . . . . . 8 ((⊀ ∧ π‘˜ ∈ β„•) β†’ 0 ≀ ((πΉβ€˜π‘˜) βˆ’ (π½β€˜π‘˜)))
236235, 228breqtrrd 5166 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ 0 ≀ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜))
2371, 2, 207, 208, 213, 215, 232, 236climsqz2 15582 . . . . . 6 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽) ⇝ 0)
238 ovexd 7436 . . . . . 6 (⊀ β†’ ((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽) ∈ V)
239 ovexd 7436 . . . . . . . . 9 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))) ∈ V)
24068recni 11224 . . . . . . . . . . 11 -2 ∈ β„‚
24154, 240basellem7 26934 . . . . . . . . . 10 ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)) ⇝ 1
242241a1i 11 . . . . . . . . 9 (⊀ β†’ ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)) ⇝ 1)
24374ffvelcdmda 7076 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜) ∈ ℝ)
244243recnd 11238 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜) ∈ β„‚)
245 eqidd 2725 . . . . . . . . . 10 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜) = (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜))
246161, 196, 57, 57, 58, 164, 245ofval 7674 . . . . . . . . 9 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺)))β€˜π‘˜) = ((π»β€˜π‘˜) Β· (((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))β€˜π‘˜)))
2471, 2, 130, 239, 242, 157, 244, 246climmul 15573 . . . . . . . 8 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))) ⇝ (((π↑2) / 6) Β· 1))
248247, 128breqtrdi 5179 . . . . . . 7 (⊀ β†’ (𝐻 ∘f Β· ((β„• Γ— {1}) ∘f + ((β„• Γ— {-2}) ∘f Β· 𝐺))) ⇝ ((π↑2) / 6))
24976, 248eqbrtrid 5173 . . . . . 6 (⊀ β†’ 𝐽 ⇝ ((π↑2) / 6))
250215recnd 11238 . . . . . 6 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) ∈ β„‚)
251218recnd 11238 . . . . . 6 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ∈ β„‚)
252214ffnd 6708 . . . . . . 7 (⊀ β†’ (𝐹 ∘f βˆ’ 𝐽) Fn β„•)
253 eqidd 2725 . . . . . . 7 ((⊀ ∧ π‘˜ ∈ β„•) β†’ ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) = ((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜))
254252, 225, 57, 57, 58, 253, 227ofval 7674 . . . . . 6 ((⊀ ∧ π‘˜ ∈ β„•) β†’ (((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽)β€˜π‘˜) = (((𝐹 ∘f βˆ’ 𝐽)β€˜π‘˜) + (π½β€˜π‘˜)))
2551, 2, 237, 238, 249, 250, 251, 254climadd 15572 . . . . 5 (⊀ β†’ ((𝐹 ∘f βˆ’ 𝐽) ∘f + 𝐽) ⇝ (0 + ((π↑2) / 6)))
25688, 255eqbrtrrd 5162 . . . 4 (⊀ β†’ 𝐹 ⇝ (0 + ((π↑2) / 6)))
257100addlidi 11398 . . . 4 (0 + ((π↑2) / 6)) = ((π↑2) / 6)
258256, 21, 2573brtr3g 5171 . . 3 (⊀ β†’ seq1( + , (𝑛 ∈ β„• ↦ (𝑛↑-2))) ⇝ ((π↑2) / 6))
2591, 2, 7, 19, 258isumclim 15699 . 2 (⊀ β†’ Ξ£π‘˜ ∈ β„• (π‘˜β†‘-2) = ((π↑2) / 6))
260259mptru 1540 1 Ξ£π‘˜ ∈ β„• (π‘˜β†‘-2) = ((π↑2) / 6)
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 395   ∧ w3a 1084   = wceq 1533  βŠ€wtru 1534   ∈ wcel 2098  Vcvv 3466   βŠ† wss 3940  {csn 4620   class class class wbr 5138   ↦ cmpt 5221   Γ— cxp 5664   Fn wfn 6528  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401   ∘f cof 7661  β„‚cc 11103  β„cr 11104  0cc0 11105  1c1 11106   + caddc 11108   Β· cmul 11110   ≀ cle 11245   βˆ’ cmin 11440  -cneg 11441   / cdiv 11867  β„•cn 12208  2c2 12263  3c3 12264  6c6 12267  β„€cz 12554  β„€β‰₯cuz 12818  seqcseq 13962  β†‘cexp 14023   ⇝ cli 15424  Ξ£csu 15628  Ο€cpi 16006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9631  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183  ax-addf 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-er 8698  df-map 8817  df-pm 8818  df-ixp 8887  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fsupp 9357  df-fi 9401  df-sup 9432  df-inf 9433  df-oi 9500  df-dju 9891  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-tan 16011  df-pi 16012  df-struct 17078  df-sets 17095  df-slot 17113  df-ndx 17125  df-base 17143  df-ress 17172  df-plusg 17208  df-mulr 17209  df-starv 17210  df-sca 17211  df-vsca 17212  df-ip 17213  df-tset 17214  df-ple 17215  df-ds 17217  df-unif 17218  df-hom 17219  df-cco 17220  df-rest 17366  df-topn 17367  df-0g 17385  df-gsum 17386  df-topgen 17387  df-pt 17388  df-prds 17391  df-xrs 17446  df-qtop 17451  df-imas 17452  df-xps 17454  df-mre 17528  df-mrc 17529  df-acs 17531  df-mgm 18562  df-sgrp 18641  df-mnd 18657  df-submnd 18703  df-mulg 18985  df-cntz 19222  df-cmn 19691  df-psmet 21219  df-xmet 21220  df-met 21221  df-bl 21222  df-mopn 21223  df-fbas 21224  df-fg 21225  df-cnfld 21228  df-top 22717  df-topon 22734  df-topsp 22756  df-bases 22770  df-cld 22844  df-ntr 22845  df-cls 22846  df-nei 22923  df-lp 22961  df-perf 22962  df-cn 23052  df-cnp 23053  df-haus 23140  df-tx 23387  df-hmeo 23580  df-fil 23671  df-fm 23763  df-flim 23764  df-flf 23765  df-xms 24147  df-ms 24148  df-tms 24149  df-cncf 24719  df-0p 25520  df-limc 25716  df-dv 25717  df-ply 26041  df-idp 26042  df-coe 26043  df-dgr 26044  df-quot 26144
This theorem is referenced by:  basel  26937
  Copyright terms: Public domain W3C validator