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	$⊢ G = (n \in ℕ ⟼ \frac{1}{2 n + 1})$
	basel.f	$⊢ F = seq 1 (+ (n \in ℕ ⟼ n^{- 2}))$
	basel.h	$⊢ H = (ℕ \times \{\frac{π^{2}}{6}\}) \times_{f} ((ℕ \times \{1\}) -_{f} G)$
	basel.j	$⊢ J = H \times_{f} ((ℕ \times \{1\}) +_{f} ((ℕ \times \{- 2\}) \times_{f} G))$
	basel.k	$⊢ K = H \times_{f} ((ℕ \times \{1\}) +_{f} G)$
Assertion	basellem9	$⊢ \sum_{k \in ℕ} k^{- 2} = \frac{π^{2}}{6}$

Proof

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

Metamath Proof Explorer

Theorem basellem9

Proof