Metamath Proof Explorer

Theorem basellem9

Description: Lemma for basel . Since by basellem8 F is bounded by two expressions that tend to _pi ^ 2 / 6 , F must also go to _pi ^ 2 / 6 by the squeeze theorem climsqz . But the series F is exactly the partial sums of k ^ -u 2 , so it follows that this is also the value of the infinite sum sum_ k e. NN ( k ^ -u 2 ) . (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses basel.g ⊒ 𝐺 = ( 𝑛 ∈ β„• ↦ ( 1 / ( ( 2 Β· 𝑛 ) + 1 ) ) )
basel.f ⊒ 𝐹 = seq 1 ( + , ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) )
basel.h ⊒ 𝐻 = ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ∘f Β· ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) )
basel.j ⊒ 𝐽 = ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) )
basel.k ⊒ 𝐾 = ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) )
Assertion basellem9 Ξ£ π‘˜ ∈ β„• ( π‘˜ ↑ - 2 ) = ( ( Ο€ ↑ 2 ) / 6 )

Proof

Step Hyp Ref Expression
1 basel.g ⊒ 𝐺 = ( 𝑛 ∈ β„• ↦ ( 1 / ( ( 2 Β· 𝑛 ) + 1 ) ) )
2 basel.f ⊒ 𝐹 = seq 1 ( + , ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) )
3 basel.h ⊒ 𝐻 = ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ∘f Β· ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) )
4 basel.j ⊒ 𝐽 = ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) )
5 basel.k ⊒ 𝐾 = ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) )
6 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
7 1zzd ⊒ ( ⊀ β†’ 1 ∈ β„€ )
8 oveq1 ⊒ ( 𝑛 = π‘˜ β†’ ( 𝑛 ↑ - 2 ) = ( π‘˜ ↑ - 2 ) )
9 eqid ⊒ ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) = ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) )
10 ovex ⊒ ( π‘˜ ↑ - 2 ) ∈ V
11 8 9 10 fvmpt ⊒ ( π‘˜ ∈ β„• β†’ ( ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) β€˜ π‘˜ ) = ( π‘˜ ↑ - 2 ) )
12 11 adantl ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) β€˜ π‘˜ ) = ( π‘˜ ↑ - 2 ) )
13 nnre ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ )
14 nnne0 ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 β‰  0 )
15 2z ⊒ 2 ∈ β„€
16 znegcl ⊒ ( 2 ∈ β„€ β†’ - 2 ∈ β„€ )
17 15 16 ax-mp ⊒ - 2 ∈ β„€
18 17 a1i ⊒ ( 𝑛 ∈ β„• β†’ - 2 ∈ β„€ )
19 13 14 18 reexpclzd ⊒ ( 𝑛 ∈ β„• β†’ ( 𝑛 ↑ - 2 ) ∈ ℝ )
20 19 adantl ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( 𝑛 ↑ - 2 ) ∈ ℝ )
21 20 9 fmptd ⊒ ( ⊀ β†’ ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) : β„• ⟢ ℝ )
22 21 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) β€˜ π‘˜ ) ∈ ℝ )
23 12 22 eqeltrrd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( π‘˜ ↑ - 2 ) ∈ ℝ )
24 23 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( π‘˜ ↑ - 2 ) ∈ β„‚ )
25 6 7 22 serfre ⊒ ( ⊀ β†’ seq 1 ( + , ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) ) : β„• ⟢ ℝ )
26 2 feq1i ⊒ ( 𝐹 : β„• ⟢ ℝ ↔ seq 1 ( + , ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) ) : β„• ⟢ ℝ )
27 25 26 sylibr ⊒ ( ⊀ β†’ 𝐹 : β„• ⟢ ℝ )
28 27 ffvelcdmda ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( 𝐹 β€˜ 𝑛 ) ∈ ℝ )
29 28 recnd ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( 𝐹 β€˜ 𝑛 ) ∈ β„‚ )
30 remulcl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) β†’ ( π‘₯ Β· 𝑦 ) ∈ ℝ )
31 30 adantl ⊒ ( ( ⊀ ∧ ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) β†’ ( π‘₯ Β· 𝑦 ) ∈ ℝ )
32 ovex ⊒ ( ( Ο€ ↑ 2 ) / 6 ) ∈ V
33 32 fconst ⊒ ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) : β„• ⟢ { ( ( Ο€ ↑ 2 ) / 6 ) }
34 pire ⊒ Ο€ ∈ ℝ
35 34 resqcli ⊒ ( Ο€ ↑ 2 ) ∈ ℝ
36 6re ⊒ 6 ∈ ℝ
37 6nn ⊒ 6 ∈ β„•
38 37 nnne0i ⊒ 6 β‰  0
39 35 36 38 redivcli ⊒ ( ( Ο€ ↑ 2 ) / 6 ) ∈ ℝ
40 39 a1i ⊒ ( ⊀ β†’ ( ( Ο€ ↑ 2 ) / 6 ) ∈ ℝ )
41 40 snssd ⊒ ( ⊀ β†’ { ( ( Ο€ ↑ 2 ) / 6 ) } βŠ† ℝ )
42 fss ⊒ ( ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) : β„• ⟢ { ( ( Ο€ ↑ 2 ) / 6 ) } ∧ { ( ( Ο€ ↑ 2 ) / 6 ) } βŠ† ℝ ) β†’ ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) : β„• ⟢ ℝ )
43 33 41 42 sylancr ⊒ ( ⊀ β†’ ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) : β„• ⟢ ℝ )
44 resubcl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) β†’ ( π‘₯ βˆ’ 𝑦 ) ∈ ℝ )
45 44 adantl ⊒ ( ( ⊀ ∧ ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) β†’ ( π‘₯ βˆ’ 𝑦 ) ∈ ℝ )
46 1ex ⊒ 1 ∈ V
47 46 fconst ⊒ ( β„• Γ— { 1 } ) : β„• ⟢ { 1 }
48 1red ⊒ ( ⊀ β†’ 1 ∈ ℝ )
49 48 snssd ⊒ ( ⊀ β†’ { 1 } βŠ† ℝ )
50 fss ⊒ ( ( ( β„• Γ— { 1 } ) : β„• ⟢ { 1 } ∧ { 1 } βŠ† ℝ ) β†’ ( β„• Γ— { 1 } ) : β„• ⟢ ℝ )
51 47 49 50 sylancr ⊒ ( ⊀ β†’ ( β„• Γ— { 1 } ) : β„• ⟢ ℝ )
52 2nn ⊒ 2 ∈ β„•
53 52 a1i ⊒ ( ⊀ β†’ 2 ∈ β„• )
54 nnmulcl ⊒ ( ( 2 ∈ β„• ∧ 𝑛 ∈ β„• ) β†’ ( 2 Β· 𝑛 ) ∈ β„• )
55 53 54 sylan ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( 2 Β· 𝑛 ) ∈ β„• )
56 55 peano2nnd ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( ( 2 Β· 𝑛 ) + 1 ) ∈ β„• )
57 56 nnrecred ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( 1 / ( ( 2 Β· 𝑛 ) + 1 ) ) ∈ ℝ )
58 57 1 fmptd ⊒ ( ⊀ β†’ 𝐺 : β„• ⟢ ℝ )
59 nnex ⊒ β„• ∈ V
60 59 a1i ⊒ ( ⊀ β†’ β„• ∈ V )
61 inidm ⊒ ( β„• ∩ β„• ) = β„•
62 45 51 58 60 60 61 off ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) : β„• ⟢ ℝ )
63 31 43 62 60 60 61 off ⊒ ( ⊀ β†’ ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ∘f Β· ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) ) : β„• ⟢ ℝ )
64 3 feq1i ⊒ ( 𝐻 : β„• ⟢ ℝ ↔ ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ∘f Β· ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) ) : β„• ⟢ ℝ )
65 63 64 sylibr ⊒ ( ⊀ β†’ 𝐻 : β„• ⟢ ℝ )
66 readdcl ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) β†’ ( π‘₯ + 𝑦 ) ∈ ℝ )
67 66 adantl ⊒ ( ( ⊀ ∧ ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) β†’ ( π‘₯ + 𝑦 ) ∈ ℝ )
68 negex ⊒ - 2 ∈ V
69 68 fconst ⊒ ( β„• Γ— { - 2 } ) : β„• ⟢ { - 2 }
70 17 zrei ⊒ - 2 ∈ ℝ
71 70 a1i ⊒ ( ⊀ β†’ - 2 ∈ ℝ )
72 71 snssd ⊒ ( ⊀ β†’ { - 2 } βŠ† ℝ )
73 fss ⊒ ( ( ( β„• Γ— { - 2 } ) : β„• ⟢ { - 2 } ∧ { - 2 } βŠ† ℝ ) β†’ ( β„• Γ— { - 2 } ) : β„• ⟢ ℝ )
74 69 72 73 sylancr ⊒ ( ⊀ β†’ ( β„• Γ— { - 2 } ) : β„• ⟢ ℝ )
75 31 74 58 60 60 61 off ⊒ ( ⊀ β†’ ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) : β„• ⟢ ℝ )
76 67 51 75 60 60 61 off ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) : β„• ⟢ ℝ )
77 31 65 76 60 60 61 off ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) : β„• ⟢ ℝ )
78 4 feq1i ⊒ ( 𝐽 : β„• ⟢ ℝ ↔ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) : β„• ⟢ ℝ )
79 77 78 sylibr ⊒ ( ⊀ β†’ 𝐽 : β„• ⟢ ℝ )
80 79 ffvelcdmda ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( 𝐽 β€˜ 𝑛 ) ∈ ℝ )
81 80 recnd ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( 𝐽 β€˜ 𝑛 ) ∈ β„‚ )
82 29 81 npcand ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( ( ( 𝐹 β€˜ 𝑛 ) βˆ’ ( 𝐽 β€˜ 𝑛 ) ) + ( 𝐽 β€˜ 𝑛 ) ) = ( 𝐹 β€˜ 𝑛 ) )
83 82 mpteq2dva ⊒ ( ⊀ β†’ ( 𝑛 ∈ β„• ↦ ( ( ( 𝐹 β€˜ 𝑛 ) βˆ’ ( 𝐽 β€˜ 𝑛 ) ) + ( 𝐽 β€˜ 𝑛 ) ) ) = ( 𝑛 ∈ β„• ↦ ( 𝐹 β€˜ 𝑛 ) ) )
84 ovexd ⊒ ( ( ⊀ ∧ 𝑛 ∈ β„• ) β†’ ( ( 𝐹 β€˜ 𝑛 ) βˆ’ ( 𝐽 β€˜ 𝑛 ) ) ∈ V )
85 27 feqmptd ⊒ ( ⊀ β†’ 𝐹 = ( 𝑛 ∈ β„• ↦ ( 𝐹 β€˜ 𝑛 ) ) )
86 79 feqmptd ⊒ ( ⊀ β†’ 𝐽 = ( 𝑛 ∈ β„• ↦ ( 𝐽 β€˜ 𝑛 ) ) )
87 60 28 80 85 86 offval2 ⊒ ( ⊀ β†’ ( 𝐹 ∘f βˆ’ 𝐽 ) = ( 𝑛 ∈ β„• ↦ ( ( 𝐹 β€˜ 𝑛 ) βˆ’ ( 𝐽 β€˜ 𝑛 ) ) ) )
88 60 84 80 87 86 offval2 ⊒ ( ⊀ β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) ∘f + 𝐽 ) = ( 𝑛 ∈ β„• ↦ ( ( ( 𝐹 β€˜ 𝑛 ) βˆ’ ( 𝐽 β€˜ 𝑛 ) ) + ( 𝐽 β€˜ 𝑛 ) ) ) )
89 83 88 85 3eqtr4d ⊒ ( ⊀ β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) ∘f + 𝐽 ) = 𝐹 )
90 67 51 58 60 60 61 off ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) : β„• ⟢ ℝ )
91 recn ⊒ ( π‘₯ ∈ ℝ β†’ π‘₯ ∈ β„‚ )
92 recn ⊒ ( 𝑦 ∈ ℝ β†’ 𝑦 ∈ β„‚ )
93 recn ⊒ ( 𝑧 ∈ ℝ β†’ 𝑧 ∈ β„‚ )
94 subdi ⊒ ( ( π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚ ∧ 𝑧 ∈ β„‚ ) β†’ ( π‘₯ Β· ( 𝑦 βˆ’ 𝑧 ) ) = ( ( π‘₯ Β· 𝑦 ) βˆ’ ( π‘₯ Β· 𝑧 ) ) )
95 91 92 93 94 syl3an ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) β†’ ( π‘₯ Β· ( 𝑦 βˆ’ 𝑧 ) ) = ( ( π‘₯ Β· 𝑦 ) βˆ’ ( π‘₯ Β· 𝑧 ) ) )
96 95 adantl ⊒ ( ( ⊀ ∧ ( π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) β†’ ( π‘₯ Β· ( 𝑦 βˆ’ 𝑧 ) ) = ( ( π‘₯ Β· 𝑦 ) βˆ’ ( π‘₯ Β· 𝑧 ) ) )
97 60 65 90 76 96 caofdi ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ) = ( ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ) ∘f βˆ’ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ) )
98 5 4 oveq12i ⊒ ( 𝐾 ∘f βˆ’ 𝐽 ) = ( ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ) ∘f βˆ’ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) )
99 97 98 eqtr4di ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ) = ( 𝐾 ∘f βˆ’ 𝐽 ) )
100 39 recni ⊒ ( ( Ο€ ↑ 2 ) / 6 ) ∈ β„‚
101 6 eqimss2i ⊒ ( β„€β‰₯ β€˜ 1 ) βŠ† β„•
102 101 59 climconst2 ⊒ ( ( ( ( Ο€ ↑ 2 ) / 6 ) ∈ β„‚ ∧ 1 ∈ β„€ ) β†’ ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ⇝ ( ( Ο€ ↑ 2 ) / 6 ) )
103 100 7 102 sylancr ⊒ ( ⊀ β†’ ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ⇝ ( ( Ο€ ↑ 2 ) / 6 ) )
104 ovexd ⊒ ( ⊀ β†’ ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ∘f Β· ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) ) ∈ V )
105 ax-resscn ⊒ ℝ βŠ† β„‚
106 fss ⊒ ( ( ( β„• Γ— { 1 } ) : β„• ⟢ ℝ ∧ ℝ βŠ† β„‚ ) β†’ ( β„• Γ— { 1 } ) : β„• ⟢ β„‚ )
107 51 105 106 sylancl ⊒ ( ⊀ β†’ ( β„• Γ— { 1 } ) : β„• ⟢ β„‚ )
108 fss ⊒ ( ( 𝐺 : β„• ⟢ ℝ ∧ ℝ βŠ† β„‚ ) β†’ 𝐺 : β„• ⟢ β„‚ )
109 58 105 108 sylancl ⊒ ( ⊀ β†’ 𝐺 : β„• ⟢ β„‚ )
110 ofnegsub ⊒ ( ( β„• ∈ V ∧ ( β„• Γ— { 1 } ) : β„• ⟢ β„‚ ∧ 𝐺 : β„• ⟢ β„‚ ) β†’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 1 } ) ∘f Β· 𝐺 ) ) = ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) )
111 59 107 109 110 mp3an2i ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 1 } ) ∘f Β· 𝐺 ) ) = ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) )
112 neg1cn ⊒ - 1 ∈ β„‚
113 1 112 basellem7 ⊒ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 1 } ) ∘f Β· 𝐺 ) ) ⇝ 1
114 111 113 eqbrtrrdi ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) ⇝ 1 )
115 43 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) β€˜ π‘˜ ) ∈ ℝ )
116 115 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) β€˜ π‘˜ ) ∈ β„‚ )
117 62 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) β€˜ π‘˜ ) ∈ ℝ )
118 117 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) β€˜ π‘˜ ) ∈ β„‚ )
119 43 ffnd ⊒ ( ⊀ β†’ ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) Fn β„• )
120 fnconstg ⊒ ( 1 ∈ β„€ β†’ ( β„• Γ— { 1 } ) Fn β„• )
121 7 120 syl ⊒ ( ⊀ β†’ ( β„• Γ— { 1 } ) Fn β„• )
122 58 ffnd ⊒ ( ⊀ β†’ 𝐺 Fn β„• )
123 121 122 60 60 61 offn ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) Fn β„• )
124 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) β€˜ π‘˜ ) = ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) β€˜ π‘˜ ) )
125 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) β€˜ π‘˜ ) = ( ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) β€˜ π‘˜ ) )
126 119 123 60 60 61 124 125 ofval ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ∘f Β· ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) ) β€˜ π‘˜ ) = ( ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) β€˜ π‘˜ ) Β· ( ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) β€˜ π‘˜ ) ) )
127 6 7 103 104 114 116 118 126 climmul ⊒ ( ⊀ β†’ ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ∘f Β· ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) ) ⇝ ( ( ( Ο€ ↑ 2 ) / 6 ) Β· 1 ) )
128 100 mulridi ⊒ ( ( ( Ο€ ↑ 2 ) / 6 ) Β· 1 ) = ( ( Ο€ ↑ 2 ) / 6 )
129 127 128 breqtrdi ⊒ ( ⊀ β†’ ( ( β„• Γ— { ( ( Ο€ ↑ 2 ) / 6 ) } ) ∘f Β· ( ( β„• Γ— { 1 } ) ∘f βˆ’ 𝐺 ) ) ⇝ ( ( Ο€ ↑ 2 ) / 6 ) )
130 3 129 eqbrtrid ⊒ ( ⊀ β†’ 𝐻 ⇝ ( ( Ο€ ↑ 2 ) / 6 ) )
131 ovexd ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ) ∈ V )
132 3cn ⊒ 3 ∈ β„‚
133 101 59 climconst2 ⊒ ( ( 3 ∈ β„‚ ∧ 1 ∈ β„€ ) β†’ ( β„• Γ— { 3 } ) ⇝ 3 )
134 132 7 133 sylancr ⊒ ( ⊀ β†’ ( β„• Γ— { 3 } ) ⇝ 3 )
135 ovexd ⊒ ( ⊀ β†’ ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) ∈ V )
136 1 basellem6 ⊒ 𝐺 ⇝ 0
137 136 a1i ⊒ ( ⊀ β†’ 𝐺 ⇝ 0 )
138 3ex ⊒ 3 ∈ V
139 138 fconst ⊒ ( β„• Γ— { 3 } ) : β„• ⟢ { 3 }
140 3re ⊒ 3 ∈ ℝ
141 140 a1i ⊒ ( ⊀ β†’ 3 ∈ ℝ )
142 141 snssd ⊒ ( ⊀ β†’ { 3 } βŠ† ℝ )
143 fss ⊒ ( ( ( β„• Γ— { 3 } ) : β„• ⟢ { 3 } ∧ { 3 } βŠ† ℝ ) β†’ ( β„• Γ— { 3 } ) : β„• ⟢ ℝ )
144 139 142 143 sylancr ⊒ ( ⊀ β†’ ( β„• Γ— { 3 } ) : β„• ⟢ ℝ )
145 144 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( β„• Γ— { 3 } ) β€˜ π‘˜ ) ∈ ℝ )
146 145 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( β„• Γ— { 3 } ) β€˜ π‘˜ ) ∈ β„‚ )
147 58 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐺 β€˜ π‘˜ ) ∈ ℝ )
148 147 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐺 β€˜ π‘˜ ) ∈ β„‚ )
149 144 ffnd ⊒ ( ⊀ β†’ ( β„• Γ— { 3 } ) Fn β„• )
150 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( β„• Γ— { 3 } ) β€˜ π‘˜ ) = ( ( β„• Γ— { 3 } ) β€˜ π‘˜ ) )
151 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐺 β€˜ π‘˜ ) = ( 𝐺 β€˜ π‘˜ ) )
152 149 122 60 60 61 150 151 ofval ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) β€˜ π‘˜ ) = ( ( ( β„• Γ— { 3 } ) β€˜ π‘˜ ) Β· ( 𝐺 β€˜ π‘˜ ) ) )
153 6 7 134 135 137 146 148 152 climmul ⊒ ( ⊀ β†’ ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) ⇝ ( 3 Β· 0 ) )
154 132 mul01i ⊒ ( 3 · 0 ) = 0
155 153 154 breqtrdi ⊒ ( ⊀ β†’ ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) ⇝ 0 )
156 65 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐻 β€˜ π‘˜ ) ∈ ℝ )
157 156 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐻 β€˜ π‘˜ ) ∈ β„‚ )
158 31 144 58 60 60 61 off ⊒ ( ⊀ β†’ ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) : β„• ⟢ ℝ )
159 158 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) β€˜ π‘˜ ) ∈ ℝ )
160 159 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) β€˜ π‘˜ ) ∈ β„‚ )
161 65 ffnd ⊒ ( ⊀ β†’ 𝐻 Fn β„• )
162 45 90 76 60 60 61 off ⊒ ( ⊀ β†’ ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) : β„• ⟢ ℝ )
163 162 ffnd ⊒ ( ⊀ β†’ ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) Fn β„• )
164 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐻 β€˜ π‘˜ ) = ( 𝐻 β€˜ π‘˜ ) )
165 148 mullidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 1 Β· ( 𝐺 β€˜ π‘˜ ) ) = ( 𝐺 β€˜ π‘˜ ) )
166 2cn ⊒ 2 ∈ β„‚
167 mulneg1 ⊒ ( ( 2 ∈ β„‚ ∧ ( 𝐺 β€˜ π‘˜ ) ∈ β„‚ ) β†’ ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) = - ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) )
168 166 148 167 sylancr ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) = - ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) )
169 168 negeqd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ - ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) = - - ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) )
170 mulcl ⊒ ( ( 2 ∈ β„‚ ∧ ( 𝐺 β€˜ π‘˜ ) ∈ β„‚ ) β†’ ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ∈ β„‚ )
171 166 148 170 sylancr ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ∈ β„‚ )
172 171 negnegd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ - - ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) = ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) )
173 169 172 eqtr2d ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) = - ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) )
174 165 173 oveq12d ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 1 Β· ( 𝐺 β€˜ π‘˜ ) ) + ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) = ( ( 𝐺 β€˜ π‘˜ ) + - ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) )
175 remulcl ⊒ ( ( - 2 ∈ ℝ ∧ ( 𝐺 β€˜ π‘˜ ) ∈ ℝ ) β†’ ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ∈ ℝ )
176 70 147 175 sylancr ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ∈ ℝ )
177 176 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ∈ β„‚ )
178 148 177 negsubd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐺 β€˜ π‘˜ ) + - ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) = ( ( 𝐺 β€˜ π‘˜ ) βˆ’ ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) )
179 174 178 eqtrd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 1 Β· ( 𝐺 β€˜ π‘˜ ) ) + ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) = ( ( 𝐺 β€˜ π‘˜ ) βˆ’ ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) )
180 df-3 ⊒ 3 = ( 2 + 1 )
181 ax-1cn ⊒ 1 ∈ β„‚
182 166 181 addcomi ⊒ ( 2 + 1 ) = ( 1 + 2 )
183 180 182 eqtri ⊒ 3 = ( 1 + 2 )
184 183 oveq1i ⊒ ( 3 Β· ( 𝐺 β€˜ π‘˜ ) ) = ( ( 1 + 2 ) Β· ( 𝐺 β€˜ π‘˜ ) )
185 1cnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ 1 ∈ β„‚ )
186 166 a1i ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ 2 ∈ β„‚ )
187 185 186 148 adddird ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 1 + 2 ) Β· ( 𝐺 β€˜ π‘˜ ) ) = ( ( 1 Β· ( 𝐺 β€˜ π‘˜ ) ) + ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) )
188 184 187 eqtrid ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 3 Β· ( 𝐺 β€˜ π‘˜ ) ) = ( ( 1 Β· ( 𝐺 β€˜ π‘˜ ) ) + ( 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) )
189 185 148 177 pnpcand ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 1 + ( 𝐺 β€˜ π‘˜ ) ) βˆ’ ( 1 + ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) ) = ( ( 𝐺 β€˜ π‘˜ ) βˆ’ ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) )
190 179 188 189 3eqtr4rd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 1 + ( 𝐺 β€˜ π‘˜ ) ) βˆ’ ( 1 + ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) ) = ( 3 Β· ( 𝐺 β€˜ π‘˜ ) ) )
191 121 122 60 60 61 offn ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) Fn β„• )
192 17 a1i ⊒ ( ⊀ β†’ - 2 ∈ β„€ )
193 fnconstg ⊒ ( - 2 ∈ β„€ β†’ ( β„• Γ— { - 2 } ) Fn β„• )
194 192 193 syl ⊒ ( ⊀ β†’ ( β„• Γ— { - 2 } ) Fn β„• )
195 194 122 60 60 61 offn ⊒ ( ⊀ β†’ ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) Fn β„• )
196 121 195 60 60 61 offn ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) Fn β„• )
197 60 48 122 151 ofc1 ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) β€˜ π‘˜ ) = ( 1 + ( 𝐺 β€˜ π‘˜ ) ) )
198 60 71 122 151 ofc1 ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) β€˜ π‘˜ ) = ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) )
199 60 48 195 198 ofc1 ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) β€˜ π‘˜ ) = ( 1 + ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) )
200 191 196 60 60 61 197 199 ofval ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) β€˜ π‘˜ ) = ( ( 1 + ( 𝐺 β€˜ π‘˜ ) ) βˆ’ ( 1 + ( - 2 Β· ( 𝐺 β€˜ π‘˜ ) ) ) ) )
201 60 141 122 151 ofc1 ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) β€˜ π‘˜ ) = ( 3 Β· ( 𝐺 β€˜ π‘˜ ) ) )
202 190 200 201 3eqtr4d ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) β€˜ π‘˜ ) = ( ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) β€˜ π‘˜ ) )
203 161 163 60 60 61 164 202 ofval ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐻 ∘f Β· ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ) β€˜ π‘˜ ) = ( ( 𝐻 β€˜ π‘˜ ) Β· ( ( ( β„• Γ— { 3 } ) ∘f Β· 𝐺 ) β€˜ π‘˜ ) ) )
204 6 7 130 131 155 157 160 203 climmul ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ) ⇝ ( ( ( Ο€ ↑ 2 ) / 6 ) Β· 0 ) )
205 100 mul01i ⊒ ( ( ( Ο€ ↑ 2 ) / 6 ) Β· 0 ) = 0
206 204 205 breqtrdi ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ∘f βˆ’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ) ⇝ 0 )
207 99 206 eqbrtrrd ⊒ ( ⊀ β†’ ( 𝐾 ∘f βˆ’ 𝐽 ) ⇝ 0 )
208 ovexd ⊒ ( ⊀ β†’ ( 𝐹 ∘f βˆ’ 𝐽 ) ∈ V )
209 31 65 90 60 60 61 off ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ) : β„• ⟢ ℝ )
210 5 feq1i ⊒ ( 𝐾 : β„• ⟢ ℝ ↔ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + 𝐺 ) ) : β„• ⟢ ℝ )
211 209 210 sylibr ⊒ ( ⊀ β†’ 𝐾 : β„• ⟢ ℝ )
212 45 211 79 60 60 61 off ⊒ ( ⊀ β†’ ( 𝐾 ∘f βˆ’ 𝐽 ) : β„• ⟢ ℝ )
213 212 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐾 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) ∈ ℝ )
214 45 27 79 60 60 61 off ⊒ ( ⊀ β†’ ( 𝐹 ∘f βˆ’ 𝐽 ) : β„• ⟢ ℝ )
215 214 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) ∈ ℝ )
216 27 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ ℝ )
217 211 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐾 β€˜ π‘˜ ) ∈ ℝ )
218 79 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐽 β€˜ π‘˜ ) ∈ ℝ )
219 eqid ⊒ ( ( 2 Β· π‘˜ ) + 1 ) = ( ( 2 Β· π‘˜ ) + 1 )
220 1 2 3 4 5 219 basellem8 ⊒ ( π‘˜ ∈ β„• β†’ ( ( 𝐽 β€˜ π‘˜ ) ≀ ( 𝐹 β€˜ π‘˜ ) ∧ ( 𝐹 β€˜ π‘˜ ) ≀ ( 𝐾 β€˜ π‘˜ ) ) )
221 220 adantl ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐽 β€˜ π‘˜ ) ≀ ( 𝐹 β€˜ π‘˜ ) ∧ ( 𝐹 β€˜ π‘˜ ) ≀ ( 𝐾 β€˜ π‘˜ ) ) )
222 221 simprd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐹 β€˜ π‘˜ ) ≀ ( 𝐾 β€˜ π‘˜ ) )
223 216 217 218 222 lesub1dd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐹 β€˜ π‘˜ ) βˆ’ ( 𝐽 β€˜ π‘˜ ) ) ≀ ( ( 𝐾 β€˜ π‘˜ ) βˆ’ ( 𝐽 β€˜ π‘˜ ) ) )
224 27 ffnd ⊒ ( ⊀ β†’ 𝐹 Fn β„• )
225 79 ffnd ⊒ ( ⊀ β†’ 𝐽 Fn β„• )
226 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐹 β€˜ π‘˜ ) = ( 𝐹 β€˜ π‘˜ ) )
227 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐽 β€˜ π‘˜ ) = ( 𝐽 β€˜ π‘˜ ) )
228 224 225 60 60 61 226 227 ofval ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) = ( ( 𝐹 β€˜ π‘˜ ) βˆ’ ( 𝐽 β€˜ π‘˜ ) ) )
229 211 ffnd ⊒ ( ⊀ β†’ 𝐾 Fn β„• )
230 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐾 β€˜ π‘˜ ) = ( 𝐾 β€˜ π‘˜ ) )
231 229 225 60 60 61 230 227 ofval ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐾 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) = ( ( 𝐾 β€˜ π‘˜ ) βˆ’ ( 𝐽 β€˜ π‘˜ ) ) )
232 223 228 231 3brtr4d ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) ≀ ( ( 𝐾 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) )
233 221 simpld ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐽 β€˜ π‘˜ ) ≀ ( 𝐹 β€˜ π‘˜ ) )
234 216 218 subge0d ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 0 ≀ ( ( 𝐹 β€˜ π‘˜ ) βˆ’ ( 𝐽 β€˜ π‘˜ ) ) ↔ ( 𝐽 β€˜ π‘˜ ) ≀ ( 𝐹 β€˜ π‘˜ ) ) )
235 233 234 mpbird ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ 0 ≀ ( ( 𝐹 β€˜ π‘˜ ) βˆ’ ( 𝐽 β€˜ π‘˜ ) ) )
236 235 228 breqtrrd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ 0 ≀ ( ( 𝐹 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) )
237 6 7 207 208 213 215 232 236 climsqz2 ⊒ ( ⊀ β†’ ( 𝐹 ∘f βˆ’ 𝐽 ) ⇝ 0 )
238 ovexd ⊒ ( ⊀ β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) ∘f + 𝐽 ) ∈ V )
239 ovexd ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ∈ V )
240 70 recni ⊒ - 2 ∈ β„‚
241 1 240 basellem7 ⊒ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ⇝ 1
242 241 a1i ⊒ ( ⊀ β†’ ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ⇝ 1 )
243 76 ffvelcdmda ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) β€˜ π‘˜ ) ∈ ℝ )
244 243 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) β€˜ π‘˜ ) ∈ β„‚ )
245 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) β€˜ π‘˜ ) = ( ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) β€˜ π‘˜ ) )
246 161 196 60 60 61 164 245 ofval ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) β€˜ π‘˜ ) = ( ( 𝐻 β€˜ π‘˜ ) Β· ( ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) β€˜ π‘˜ ) ) )
247 6 7 130 239 242 157 244 246 climmul ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ⇝ ( ( ( Ο€ ↑ 2 ) / 6 ) Β· 1 ) )
248 247 128 breqtrdi ⊒ ( ⊀ β†’ ( 𝐻 ∘f Β· ( ( β„• Γ— { 1 } ) ∘f + ( ( β„• Γ— { - 2 } ) ∘f Β· 𝐺 ) ) ) ⇝ ( ( Ο€ ↑ 2 ) / 6 ) )
249 4 248 eqbrtrid ⊒ ( ⊀ β†’ 𝐽 ⇝ ( ( Ο€ ↑ 2 ) / 6 ) )
250 215 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) ∈ β„‚ )
251 218 recnd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐽 β€˜ π‘˜ ) ∈ β„‚ )
252 214 ffnd ⊒ ( ⊀ β†’ ( 𝐹 ∘f βˆ’ 𝐽 ) Fn β„• )
253 eqidd ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) = ( ( 𝐹 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) )
254 252 225 60 60 61 253 227 ofval ⊒ ( ( ⊀ ∧ π‘˜ ∈ β„• ) β†’ ( ( ( 𝐹 ∘f βˆ’ 𝐽 ) ∘f + 𝐽 ) β€˜ π‘˜ ) = ( ( ( 𝐹 ∘f βˆ’ 𝐽 ) β€˜ π‘˜ ) + ( 𝐽 β€˜ π‘˜ ) ) )
255 6 7 237 238 249 250 251 254 climadd ⊒ ( ⊀ β†’ ( ( 𝐹 ∘f βˆ’ 𝐽 ) ∘f + 𝐽 ) ⇝ ( 0 + ( ( Ο€ ↑ 2 ) / 6 ) ) )
256 89 255 eqbrtrrd ⊒ ( ⊀ β†’ 𝐹 ⇝ ( 0 + ( ( Ο€ ↑ 2 ) / 6 ) ) )
257 100 addlidi ⊒ ( 0 + ( ( Ο€ ↑ 2 ) / 6 ) ) = ( ( Ο€ ↑ 2 ) / 6 )
258 256 2 257 3brtr3g ⊒ ( ⊀ β†’ seq 1 ( + , ( 𝑛 ∈ β„• ↦ ( 𝑛 ↑ - 2 ) ) ) ⇝ ( ( Ο€ ↑ 2 ) / 6 ) )
259 6 7 12 24 258 isumclim ⊒ ( ⊀ β†’ Ξ£ π‘˜ ∈ β„• ( π‘˜ ↑ - 2 ) = ( ( Ο€ ↑ 2 ) / 6 ) )
260 259 mptru ⊒ Ξ£ π‘˜ ∈ β„• ( π‘˜ ↑ - 2 ) = ( ( Ο€ ↑ 2 ) / 6 )