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 )