Theorem rpnnen2lem9

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

	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	rpnnen2lem9	$$⊢M\in \mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=0+\left(\frac{{\left(\frac{1}{3}\right)}^{M+1}}{1-\left(\frac{1}{3}\right)}\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		eqid	$$⊢{\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}$$
3		nnz	$$⊢M\in \mathbb{N}\to M\in \mathbb{Z}$$
4		eqidd	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)$$
5		eluznn	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to k\in \mathbb{N}$$
6		difss	$$⊢\mathbb{N}\setminus \left\{M\right\}\subseteq \mathbb{N}$$
7	1	rpnnen2lem2	$$⊢\mathbb{N}\setminus \left\{M\right\}\subseteq \mathbb{N}\to F\left(\mathbb{N}\setminus \left\{M\right\}\right):\mathbb{N}⟶ℝ$$
8	6 7	ax-mp	$$⊢F\left(\mathbb{N}\setminus \left\{M\right\}\right):\mathbb{N}⟶ℝ$$
9	8	ffvelcdmi	$$⊢k\in \mathbb{N}\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)\in ℝ$$
10	9	recnd	$$⊢k\in \mathbb{N}\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)\in ℂ$$
11	5 10	syl	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)\in ℂ$$
12	1	rpnnen2lem5	$$⊢\left(\mathbb{N}\setminus \left\{M\right\}\subseteq \mathbb{N}\wedge M\in \mathbb{N}\right)\to seqM\left(+,F\left(\mathbb{N}\setminus \left\{M\right\}\right)\right)\in \mathrm{dom}⇝$$
13	6 12	mpan	$$⊢M\in \mathbb{N}\to seqM\left(+,F\left(\mathbb{N}\setminus \left\{M\right\}\right)\right)\in \mathrm{dom}⇝$$
14	2 3 4 11 13	isum1p	$$⊢M\in \mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(M\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)$$
15	1	rpnnen2lem1	$$⊢\left(\mathbb{N}\setminus \left\{M\right\}\subseteq \mathbb{N}\wedge M\in \mathbb{N}\right)\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(M\right)=if\left(M\in \left(\mathbb{N}\setminus \left\{M\right\}\right),{\left(\frac{1}{3}\right)}^M,0\right)$$
16	6 15	mpan	$$⊢M\in \mathbb{N}\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(M\right)=if\left(M\in \left(\mathbb{N}\setminus \left\{M\right\}\right),{\left(\frac{1}{3}\right)}^M,0\right)$$
17		neldifsnd	$$⊢M\in \mathbb{N}\to \neg M\in \left(\mathbb{N}\setminus \left\{M\right\}\right)$$
18	17	iffalsed	$$⊢M\in \mathbb{N}\to if\left(M\in \left(\mathbb{N}\setminus \left\{M\right\}\right),{\left(\frac{1}{3}\right)}^M,0\right)=0$$
19	16 18	eqtrd	$$⊢M\in \mathbb{N}\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(M\right)=0$$
20		eqid	$$⊢{\mathbb{Z}}_{\ge \left(M+1\right)}={\mathbb{Z}}_{\ge \left(M+1\right)}$$
21		peano2nn	$$⊢M\in \mathbb{N}\to M+1\in \mathbb{N}$$
22	21	nnzd	$$⊢M\in \mathbb{N}\to M+1\in \mathbb{Z}$$
23		eqidd	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)$$
24		eluznn	$$⊢\left(M+1\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to k\in \mathbb{N}$$
25	21 24	sylan	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to k\in \mathbb{N}$$
26	25 10	syl	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)\in ℂ$$
27		1re	$$⊢1\in ℝ$$
28		3nn	$$⊢3\in \mathbb{N}$$
29		nndivre	$$⊢\left(1\in ℝ\wedge 3\in \mathbb{N}\right)\to \frac{1}{3}\in ℝ$$
30	27 28 29	mp2an	$$⊢\frac{1}{3}\in ℝ$$
31	30	recni	$$⊢\frac{1}{3}\in ℂ$$
32	31	a1i	$$⊢M\in \mathbb{N}\to \frac{1}{3}\in ℂ$$
33		0re	$$⊢0\in ℝ$$
34		3re	$$⊢3\in ℝ$$
35		3pos	$$⊢0<3$$
36	34 35	recgt0ii	$$⊢0<\frac{1}{3}$$
37	33 30 36	ltleii	$$⊢0\le \frac{1}{3}$$
38		absid	$$⊢\left(\frac{1}{3}\in ℝ\wedge 0\le \frac{1}{3}\right)\to \left|\frac{1}{3}\right|=\frac{1}{3}$$
39	30 37 38	mp2an	$$⊢\left|\frac{1}{3}\right|=\frac{1}{3}$$
40		1lt3	$$⊢1<3$$
41		recgt1	$$⊢\left(3\in ℝ\wedge 0<3\right)\to \left(1<3\leftrightarrow \frac{1}{3}<1\right)$$
42	34 35 41	mp2an	$$⊢1<3\leftrightarrow \frac{1}{3}<1$$
43	40 42	mpbi	$$⊢\frac{1}{3}<1$$
44	39 43	eqbrtri	$$⊢\left|\frac{1}{3}\right|<1$$
45	44	a1i	$$⊢M\in \mathbb{N}\to \left|\frac{1}{3}\right|<1$$
46	21	nnnn0d	$$⊢M\in \mathbb{N}\to M+1\in {\mathbb{N}}_0$$
47	1	rpnnen2lem1	$$⊢\left(\mathbb{N}\setminus \left\{M\right\}\subseteq \mathbb{N}\wedge k\in \mathbb{N}\right)\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=if\left(k\in \left(\mathbb{N}\setminus \left\{M\right\}\right),{\left(\frac{1}{3}\right)}^k,0\right)$$
48	6 47	mpan	$$⊢k\in \mathbb{N}\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=if\left(k\in \left(\mathbb{N}\setminus \left\{M\right\}\right),{\left(\frac{1}{3}\right)}^k,0\right)$$
49	25 48	syl	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=if\left(k\in \left(\mathbb{N}\setminus \left\{M\right\}\right),{\left(\frac{1}{3}\right)}^k,0\right)$$
50		nnre	$$⊢M\in \mathbb{N}\to M\in ℝ$$
51	50	adantr	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to M\in ℝ$$
52		eluzle	$$⊢k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\to M+1\le k$$
53	52	adantl	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to M+1\le k$$
54		nnltp1le	$$⊢\left(M\in \mathbb{N}\wedge k\in \mathbb{N}\right)\to \left(M<k\leftrightarrow M+1\le k\right)$$
55	25 54	syldan	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to \left(M<k\leftrightarrow M+1\le k\right)$$
56	53 55	mpbird	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to M<k$$
57	51 56	gtned	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to k\ne M$$
58		eldifsn	$$⊢k\in \left(\mathbb{N}\setminus \left\{M\right\}\right)\leftrightarrow \left(k\in \mathbb{N}\wedge k\ne M\right)$$
59	25 57 58	sylanbrc	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to k\in \left(\mathbb{N}\setminus \left\{M\right\}\right)$$
60	59	iftrued	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to if\left(k\in \left(\mathbb{N}\setminus \left\{M\right\}\right),{\left(\frac{1}{3}\right)}^k,0\right)={\left(\frac{1}{3}\right)}^k$$
61	49 60	eqtrd	$$⊢\left(M\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)={\left(\frac{1}{3}\right)}^k$$
62	32 45 46 61	geolim2	$$⊢M\in \mathbb{N}\to seq\left(M+1\right)\left(+,F\left(\mathbb{N}\setminus \left\{M\right\}\right)\right)⇝\left(\frac{{\left(\frac{1}{3}\right)}^{M+1}}{1-\left(\frac{1}{3}\right)}\right)$$
63	20 22 23 26 62	isumclim	$$⊢M\in \mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=\frac{{\left(\frac{1}{3}\right)}^{M+1}}{1-\left(\frac{1}{3}\right)}$$
64	19 63	oveq12d	$$⊢M\in \mathbb{N}\to F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(M\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=0+\left(\frac{{\left(\frac{1}{3}\right)}^{M+1}}{1-\left(\frac{1}{3}\right)}\right)$$
65	14 64	eqtrd	$$⊢M\in \mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(\mathbb{N}\setminus \left\{M\right\}\right)\left(k\right)=0+\left(\frac{{\left(\frac{1}{3}\right)}^{M+1}}{1-\left(\frac{1}{3}\right)}\right)$$