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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) |
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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 𝐽 ‘ 𝑛 ) ∈ ℝ ) |
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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ‘ 𝑘 ) ∈ ℝ ) |
116 |
115
|
recnd |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ‘ 𝑘 ) ∈ ℂ ) |
117 |
62
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℕ × { 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
|
mulid1i |
⊢ ( ( ( π ↑ 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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 3 } ) ‘ 𝑘 ) ∈ ℝ ) |
146 |
145
|
recnd |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 3 } ) ‘ 𝑘 ) ∈ ℂ ) |
147 |
58
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ ) |
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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) ∈ ℝ ) |
157 |
156
|
recnd |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) ∈ ℂ ) |
158 |
31 144 58 60 60 61
|
off |
⊢ ( ⊤ → ( ( ℕ × { 3 } ) ∘f · 𝐺 ) : ℕ ⟶ ℝ ) |
159 |
158
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℕ × { 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
|
mulid2d |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐾 ∘f − 𝐽 ) ‘ 𝑘 ) ∈ ℝ ) |
214 |
45 27 79 60 60 61
|
off |
⊢ ( ⊤ → ( 𝐹 ∘f − 𝐽 ) : ℕ ⟶ ℝ ) |
215 |
214
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ∘f − 𝐽 ) ‘ 𝑘 ) ∈ ℝ ) |
216 |
27
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) |
217 |
211
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐾 ‘ 𝑘 ) ∈ ℝ ) |
218 |
79
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐽 ‘ 𝑘 ) ∈ ℝ ) |
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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℕ × { 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
|
addid2i |
⊢ ( 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 ) |