Theorem 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	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
	basellem7.2	⊢ 𝐴 ∈ ℂ
Assertion	basellem7	⊢ ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ) ⇝ 1

Proof

Step	Hyp	Ref	Expression
1		basel.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
2		basellem7.2	⊢ 𝐴 ∈ ℂ
3		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
4		1zzd	⊢ ( ⊤ → 1 ∈ ℤ )
5		ax-1cn	⊢ 1 ∈ ℂ
6	3	eqimss2i	⊢ ( ℤ≥ ‘ 1 ) ⊆ ℕ
7		nnex	⊢ ℕ ∈ V
8	6 7	climconst2	⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { 1 } ) ⇝ 1 )
9	5 4 8	sylancr	⊢ ( ⊤ → ( ℕ × { 1 } ) ⇝ 1 )
10		ovexd	⊢ ( ⊤ → ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ) ∈ V )
11	6 7	climconst2	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { 𝐴 } ) ⇝ 𝐴 )
12	2 4 11	sylancr	⊢ ( ⊤ → ( ℕ × { 𝐴 } ) ⇝ 𝐴 )
13		ovexd	⊢ ( ⊤ → ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ∈ V )
14	1	basellem6	⊢ 𝐺 ⇝ 0
15	14	a1i	⊢ ( ⊤ → 𝐺 ⇝ 0 )
16	2	elexi	⊢ 𝐴 ∈ V
17	16	fconst	⊢ ( ℕ × { 𝐴 } ) : ℕ ⟶ { 𝐴 }
18	2	a1i	⊢ ( ⊤ → 𝐴 ∈ ℂ )
19	18	snssd	⊢ ( ⊤ → { 𝐴 } ⊆ ℂ )
20		fss	⊢ ( ( ( ℕ × { 𝐴 } ) : ℕ ⟶ { 𝐴 } ∧ { 𝐴 } ⊆ ℂ ) → ( ℕ × { 𝐴 } ) : ℕ ⟶ ℂ )
21	17 19 20	sylancr	⊢ ( ⊤ → ( ℕ × { 𝐴 } ) : ℕ ⟶ ℂ )
22	21	ffvelrnda	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 𝐴 } ) ‘ 𝑘 ) ∈ ℂ )
23		2nn	⊢ 2 ∈ ℕ
24	23	a1i	⊢ ( ⊤ → 2 ∈ ℕ )
25		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 2 · 𝑛 ) ∈ ℕ )
26	24 25	sylan	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 2 · 𝑛 ) ∈ ℕ )
27	26	peano2nnd	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
28	27	nnrecred	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ )
29	28	recnd	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
30	29 1	fmptd	⊢ ( ⊤ → 𝐺 : ℕ ⟶ ℂ )
31	30	ffvelrnda	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
32	21	ffnd	⊢ ( ⊤ → ( ℕ × { 𝐴 } ) Fn ℕ )
33	30	ffnd	⊢ ( ⊤ → 𝐺 Fn ℕ )
34	7	a1i	⊢ ( ⊤ → ℕ ∈ V )
35		inidm	⊢ ( ℕ ∩ ℕ ) = ℕ
36		eqidd	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 𝐴 } ) ‘ 𝑘 ) = ( ( ℕ × { 𝐴 } ) ‘ 𝑘 ) )
37		eqidd	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
38	32 33 34 34 35 36 37	ofval	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ‘ 𝑘 ) = ( ( ( ℕ × { 𝐴 } ) ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
39	3 4 12 13 15 22 31 38	climmul	⊢ ( ⊤ → ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ⇝ ( 𝐴 · 0 ) )
40	2	mul01i	⊢ ( 𝐴 · 0 ) = 0
41	39 40	breqtrdi	⊢ ( ⊤ → ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ⇝ 0 )
42		1ex	⊢ 1 ∈ V
43	42	fconst	⊢ ( ℕ × { 1 } ) : ℕ ⟶ { 1 }
44	5	a1i	⊢ ( ⊤ → 1 ∈ ℂ )
45	44	snssd	⊢ ( ⊤ → { 1 } ⊆ ℂ )
46		fss	⊢ ( ( ( ℕ × { 1 } ) : ℕ ⟶ { 1 } ∧ { 1 } ⊆ ℂ ) → ( ℕ × { 1 } ) : ℕ ⟶ ℂ )
47	43 45 46	sylancr	⊢ ( ⊤ → ( ℕ × { 1 } ) : ℕ ⟶ ℂ )
48	47	ffvelrnda	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 1 } ) ‘ 𝑘 ) ∈ ℂ )
49		mulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
50	49	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
51	50 21 30 34 34 35	off	⊢ ( ⊤ → ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) : ℕ ⟶ ℂ )
52	51	ffvelrnda	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ‘ 𝑘 ) ∈ ℂ )
53	43	a1i	⊢ ( ⊤ → ( ℕ × { 1 } ) : ℕ ⟶ { 1 } )
54	53	ffnd	⊢ ( ⊤ → ( ℕ × { 1 } ) Fn ℕ )
55	51	ffnd	⊢ ( ⊤ → ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) Fn ℕ )
56		eqidd	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 1 } ) ‘ 𝑘 ) = ( ( ℕ × { 1 } ) ‘ 𝑘 ) )
57		eqidd	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ‘ 𝑘 ) = ( ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ‘ 𝑘 ) )
58	54 55 34 34 35 56 57	ofval	⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ) ‘ 𝑘 ) = ( ( ( ℕ × { 1 } ) ‘ 𝑘 ) + ( ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ‘ 𝑘 ) ) )
59	3 4 9 10 41 48 52 58	climadd	⊢ ( ⊤ → ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ) ⇝ ( 1 + 0 ) )
60	59	mptru	⊢ ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ) ⇝ ( 1 + 0 )
61		1p0e1	⊢ ( 1 + 0 ) = 1
62	60 61	breqtri	⊢ ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { 𝐴 } ) ∘f · 𝐺 ) ) ⇝ 1