basellem7

Description: Lemma for basel . The function 1 + A x. G for any fixed A goes to 1 . (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	basel.g	$⊢ G = (n \in ℕ ⟼ \frac{1}{2 n + 1})$
	basellem7.2	$⊢ A \in ℂ$
Assertion	basellem7	$⊢ ((ℕ \times \{1\}) +_{f} ((ℕ \times \{A\}) \times_{f} G)) ⇝ 1$

Proof

Step	Hyp	Ref	Expression
1		basel.g	$⊢ G = (n \in ℕ ⟼ \frac{1}{2 n + 1})$
2		basellem7.2	$⊢ A \in ℂ$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4		1zzd	$⊢ ⊤ \to 1 \in ℤ$
5		ax-1cn	$⊢ 1 \in ℂ$
6	3	eqimss2i	$⊢ ℤ_{\geq 1} \subseteq ℕ$
7		nnex	$⊢ ℕ \in V$
8	6 7	climconst2	$⊢ (1 \in ℂ \land 1 \in ℤ) \to (ℕ \times \{1\}) ⇝ 1$
9	5 4 8	sylancr	$⊢ ⊤ \to (ℕ \times \{1\}) ⇝ 1$
10		ovexd	$⊢ ⊤ \to (ℕ \times \{1\}) +_{f} ((ℕ \times \{A\}) \times_{f} G) \in V$
11	6 7	climconst2	$⊢ (A \in ℂ \land 1 \in ℤ) \to (ℕ \times \{A\}) ⇝ A$
12	2 4 11	sylancr	$⊢ ⊤ \to (ℕ \times \{A\}) ⇝ A$
13		ovexd	$⊢ ⊤ \to (ℕ \times \{A\}) \times_{f} G \in V$
14	1	basellem6	$⊢ G ⇝ 0$
15	14	a1i	$⊢ ⊤ \to G ⇝ 0$
16	2	elexi	$⊢ A \in V$
17	16	fconst	$⊢ (ℕ \times \{A\}) : ℕ ⟶ \{A\}$
18	2	a1i	$⊢ ⊤ \to A \in ℂ$
19	18	snssd	$⊢ ⊤ \to \{A\} \subseteq ℂ$
20		fss	$⊢ ((ℕ \times \{A\}) : ℕ ⟶ \{A\} \land \{A\} \subseteq ℂ) \to (ℕ \times \{A\}) : ℕ ⟶ ℂ$
21	17 19 20	sylancr	$⊢ ⊤ \to (ℕ \times \{A\}) : ℕ ⟶ ℂ$
22	21	ffvelrnda	$⊢ (⊤ \land k \in ℕ) \to (ℕ \times \{A\}) (k) \in ℂ$
23		2nn	$⊢ 2 \in ℕ$
24	23	a1i	$⊢ ⊤ \to 2 \in ℕ$
25		nnmulcl	$⊢ (2 \in ℕ \land n \in ℕ) \to 2 n \in ℕ$
26	24 25	sylan	$⊢ (⊤ \land n \in ℕ) \to 2 n \in ℕ$
27	26	peano2nnd	$⊢ (⊤ \land n \in ℕ) \to 2 n + 1 \in ℕ$
28	27	nnrecred	$⊢ (⊤ \land n \in ℕ) \to \frac{1}{2 n + 1} \in ℝ$
29	28	recnd	$⊢ (⊤ \land n \in ℕ) \to \frac{1}{2 n + 1} \in ℂ$
30	29 1	fmptd	$⊢ ⊤ \to G : ℕ ⟶ ℂ$
31	30	ffvelrnda	$⊢ (⊤ \land k \in ℕ) \to G (k) \in ℂ$
32	21	ffnd	$⊢ ⊤ \to (ℕ \times \{A\}) Fn ℕ$
33	30	ffnd	$⊢ ⊤ \to G Fn ℕ$
34	7	a1i	$⊢ ⊤ \to ℕ \in V$
35		inidm	$⊢ ℕ \cap ℕ = ℕ$
36		eqidd	$⊢ (⊤ \land k \in ℕ) \to (ℕ \times \{A\}) (k) = (ℕ \times \{A\}) (k)$
37		eqidd	$⊢ (⊤ \land k \in ℕ) \to G (k) = G (k)$
38	32 33 34 34 35 36 37	ofval	$⊢ (⊤ \land k \in ℕ) \to ((ℕ \times \{A\}) \times_{f} G) (k) = (ℕ \times \{A\}) (k) G (k)$
39	3 4 12 13 15 22 31 38	climmul	$⊢ ⊤ \to ((ℕ \times \{A\}) \times_{f} G) ⇝ A \cdot 0$
40	2	mul01i	$⊢ A \cdot 0 = 0$
41	39 40	breqtrdi	$⊢ ⊤ \to ((ℕ \times \{A\}) \times_{f} G) ⇝ 0$
42		1ex	$⊢ 1 \in V$
43	42	fconst	$⊢ (ℕ \times \{1\}) : ℕ ⟶ \{1\}$
44	5	a1i	$⊢ ⊤ \to 1 \in ℂ$
45	44	snssd	$⊢ ⊤ \to \{1\} \subseteq ℂ$
46		fss	$⊢ ((ℕ \times \{1\}) : ℕ ⟶ \{1\} \land \{1\} \subseteq ℂ) \to (ℕ \times \{1\}) : ℕ ⟶ ℂ$
47	43 45 46	sylancr	$⊢ ⊤ \to (ℕ \times \{1\}) : ℕ ⟶ ℂ$
48	47	ffvelrnda	$⊢ (⊤ \land k \in ℕ) \to (ℕ \times \{1\}) (k) \in ℂ$
49		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
50	49	adantl	$⊢ (⊤ \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
51	50 21 30 34 34 35	off	$⊢ ⊤ \to ((ℕ \times \{A\}) \times_{f} G) : ℕ ⟶ ℂ$
52	51	ffvelrnda	$⊢ (⊤ \land k \in ℕ) \to ((ℕ \times \{A\}) \times_{f} G) (k) \in ℂ$
53	43	a1i	$⊢ ⊤ \to (ℕ \times \{1\}) : ℕ ⟶ \{1\}$
54	53	ffnd	$⊢ ⊤ \to (ℕ \times \{1\}) Fn ℕ$
55	51	ffnd	$⊢ ⊤ \to ((ℕ \times \{A\}) \times_{f} G) Fn ℕ$
56		eqidd	$⊢ (⊤ \land k \in ℕ) \to (ℕ \times \{1\}) (k) = (ℕ \times \{1\}) (k)$
57		eqidd	$⊢ (⊤ \land k \in ℕ) \to ((ℕ \times \{A\}) \times_{f} G) (k) = ((ℕ \times \{A\}) \times_{f} G) (k)$
58	54 55 34 34 35 56 57	ofval	$⊢ (⊤ \land k \in ℕ) \to ((ℕ \times \{1\}) +_{f} ((ℕ \times \{A\}) \times_{f} G)) (k) = (ℕ \times \{1\}) (k) + ((ℕ \times \{A\}) \times_{f} G) (k)$
59	3 4 9 10 41 48 52 58	climadd	$⊢ ⊤ \to ((ℕ \times \{1\}) +_{f} ((ℕ \times \{A\}) \times_{f} G)) ⇝ (1 + 0)$
60	59	mptru	$⊢ ((ℕ \times \{1\}) +_{f} ((ℕ \times \{A\}) \times_{f} G)) ⇝ (1 + 0)$
61		1p0e1	$⊢ 1 + 0 = 1$
62	60 61	breqtri	$⊢ ((ℕ \times \{1\}) +_{f} ((ℕ \times \{A\}) \times_{f} G)) ⇝ 1$

Metamath Proof Explorer

Theorem basellem7

Proof