Theorem rpnnen2lem3

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013)

	Ref	Expression
Hypothesis	rpnnen2.1	$$⊢F=\left(x\in 𝒫\mathbb{N}⟼\left(n\in \mathbb{N}⟼if\left(n\in x,{\left(\frac{1}{3}\right)}^n,0\right)\right)\right)$$
Assertion	rpnnen2lem3	$$⊢seq1\left(+,F\left(\mathbb{N}\right)\right)⇝\left(\frac{1}{2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rpnnen2.1	$$⊢F=\left(x\in 𝒫\mathbb{N}⟼\left(n\in \mathbb{N}⟼if\left(n\in x,{\left(\frac{1}{3}\right)}^n,0\right)\right)\right)$$
2		1re	$$⊢1\in ℝ$$
3		3nn	$$⊢3\in \mathbb{N}$$
4		nndivre	$$⊢\left(1\in ℝ\wedge 3\in \mathbb{N}\right)\to \frac{1}{3}\in ℝ$$
5	2 3 4	mp2an	$$⊢\frac{1}{3}\in ℝ$$
6	5	recni	$$⊢\frac{1}{3}\in ℂ$$
7	6	a1i	$$⊢\top \to \frac{1}{3}\in ℂ$$
8		0re	$$⊢0\in ℝ$$
9		3re	$$⊢3\in ℝ$$
10		3pos	$$⊢0<3$$
11	9 10	recgt0ii	$$⊢0<\frac{1}{3}$$
12	8 5 11	ltleii	$$⊢0\le \frac{1}{3}$$
13		absid	$$⊢\left(\frac{1}{3}\in ℝ\wedge 0\le \frac{1}{3}\right)\to \left|\frac{1}{3}\right|=\frac{1}{3}$$
14	5 12 13	mp2an	$$⊢\left|\frac{1}{3}\right|=\frac{1}{3}$$
15		1lt3	$$⊢1<3$$
16		recgt1	$$⊢\left(3\in ℝ\wedge 0<3\right)\to \left(1<3\leftrightarrow \frac{1}{3}<1\right)$$
17	9 10 16	mp2an	$$⊢1<3\leftrightarrow \frac{1}{3}<1$$
18	15 17	mpbi	$$⊢\frac{1}{3}<1$$
19	14 18	eqbrtri	$$⊢\left|\frac{1}{3}\right|<1$$
20	19	a1i	$$⊢\top \to \left|\frac{1}{3}\right|<1$$
21		1nn0	$$⊢1\in {\mathbb{N}}_0$$
22	21	a1i	$$⊢\top \to 1\in {\mathbb{N}}_0$$
23		ssid	$$⊢\mathbb{N}\subseteq \mathbb{N}$$
24		simpr	$$⊢\left(\top \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to k\in {\mathbb{Z}}_{\ge 1}$$
25		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
26	24 25	eleqtrrdi	$$⊢\left(\top \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to k\in \mathbb{N}$$
27	1	rpnnen2lem1	$$⊢\left(\mathbb{N}\subseteq \mathbb{N}\wedge k\in \mathbb{N}\right)\to F\left(\mathbb{N}\right)\left(k\right)=if\left(k\in \mathbb{N},{\left(\frac{1}{3}\right)}^k,0\right)$$
28	23 26 27	sylancr	$$⊢\left(\top \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to F\left(\mathbb{N}\right)\left(k\right)=if\left(k\in \mathbb{N},{\left(\frac{1}{3}\right)}^k,0\right)$$
29	26	iftrued	$$⊢\left(\top \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to if\left(k\in \mathbb{N},{\left(\frac{1}{3}\right)}^k,0\right)={\left(\frac{1}{3}\right)}^k$$
30	28 29	eqtrd	$$⊢\left(\top \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to F\left(\mathbb{N}\right)\left(k\right)={\left(\frac{1}{3}\right)}^k$$
31	7 20 22 30	geolim2	$$⊢\top \to seq1\left(+,F\left(\mathbb{N}\right)\right)⇝\left(\frac{{\left(\frac{1}{3}\right)}^1}{1-\left(\frac{1}{3}\right)}\right)$$
32	31	mptru	$$⊢seq1\left(+,F\left(\mathbb{N}\right)\right)⇝\left(\frac{{\left(\frac{1}{3}\right)}^1}{1-\left(\frac{1}{3}\right)}\right)$$
33		exp1	$$⊢\frac{1}{3}\in ℂ\to {\left(\frac{1}{3}\right)}^1=\frac{1}{3}$$
34	6 33	ax-mp	$$⊢{\left(\frac{1}{3}\right)}^1=\frac{1}{3}$$
35		3cn	$$⊢3\in ℂ$$
36		ax-1cn	$$⊢1\in ℂ$$
37		3ne0	$$⊢3\ne 0$$
38	35 37	pm3.2i	$$⊢\left(3\in ℂ\wedge 3\ne 0\right)$$
39		divsubdir	$$⊢\left(3\in ℂ\wedge 1\in ℂ\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{3-1}{3}=\left(\frac{3}{3}\right)-\left(\frac{1}{3}\right)$$
40	35 36 38 39	mp3an	$$⊢\frac{3-1}{3}=\left(\frac{3}{3}\right)-\left(\frac{1}{3}\right)$$
41		3m1e2	$$⊢3-1=2$$
42	41	oveq1i	$$⊢\frac{3-1}{3}=\frac{2}{3}$$
43	35 37	dividi	$$⊢\frac{3}{3}=1$$
44	43	oveq1i	$$⊢\left(\frac{3}{3}\right)-\left(\frac{1}{3}\right)=1-\left(\frac{1}{3}\right)$$
45	40 42 44	3eqtr3ri	$$⊢1-\left(\frac{1}{3}\right)=\frac{2}{3}$$
46	34 45	oveq12i	$$⊢\frac{{\left(\frac{1}{3}\right)}^1}{1-\left(\frac{1}{3}\right)}=\frac{\frac{1}{3}}{\frac{2}{3}}$$
47		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
48		divcan7	$$⊢\left(1\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{\frac{1}{3}}{\frac{2}{3}}=\frac{1}{2}$$
49	36 47 38 48	mp3an	$$⊢\frac{\frac{1}{3}}{\frac{2}{3}}=\frac{1}{2}$$
50	46 49	eqtri	$$⊢\frac{{\left(\frac{1}{3}\right)}^1}{1-\left(\frac{1}{3}\right)}=\frac{1}{2}$$
51	32 50	breqtri	$$⊢seq1\left(+,F\left(\mathbb{N}\right)\right)⇝\left(\frac{1}{2}\right)$$