Theorem rpnnen2lem11

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

	Ref	Expression
Hypotheses	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)$$
	rpnnen2.2	$$⊢\phi \to A\subseteq \mathbb{N}$$
	rpnnen2.3	$$⊢\phi \to B\subseteq \mathbb{N}$$
	rpnnen2.4	$$⊢\phi \to m\in \left(A\setminus B\right)$$
	rpnnen2.5	$$⊢\phi \to \forall n\in \mathbb{N}\left(n<m\to \left(n\in A\leftrightarrow n\in B\right)\right)$$
	rpnnen2.6	$$⊢\psi \leftrightarrow \sum _{k\in \mathbb{N}}F\left(A\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(B\right)\left(k\right)$$
Assertion	rpnnen2lem11	$$⊢\phi \to \neg \psi$$

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		rpnnen2.2	$$⊢\phi \to A\subseteq \mathbb{N}$$
3		rpnnen2.3	$$⊢\phi \to B\subseteq \mathbb{N}$$
4		rpnnen2.4	$$⊢\phi \to m\in \left(A\setminus B\right)$$
5		rpnnen2.5	$$⊢\phi \to \forall n\in \mathbb{N}\left(n<m\to \left(n\in A\leftrightarrow n\in B\right)\right)$$
6		rpnnen2.6	$$⊢\psi \leftrightarrow \sum _{k\in \mathbb{N}}F\left(A\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(B\right)\left(k\right)$$
7		eldifi	$$⊢m\in \left(A\setminus B\right)\to m\in A$$
8		ssel2	$$⊢\left(A\subseteq \mathbb{N}\wedge m\in A\right)\to m\in \mathbb{N}$$
9	7 8	sylan2	$$⊢\left(A\subseteq \mathbb{N}\wedge m\in \left(A\setminus B\right)\right)\to m\in \mathbb{N}$$
10	2 4 9	syl2anc	$$⊢\phi \to m\in \mathbb{N}$$
11	1	rpnnen2lem6	$$⊢\left(B\subseteq \mathbb{N}\wedge m\in \mathbb{N}\right)\to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)\in ℝ$$
12	3 10 11	syl2anc	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)\in ℝ$$
13		3nn	$$⊢3\in \mathbb{N}$$
14		nnrecre	$$⊢3\in \mathbb{N}\to \frac{1}{3}\in ℝ$$
15	13 14	ax-mp	$$⊢\frac{1}{3}\in ℝ$$
16	10	nnnn0d	$$⊢\phi \to m\in {\mathbb{N}}_0$$
17		reexpcl	$$⊢\left(\frac{1}{3}\in ℝ\wedge m\in {\mathbb{N}}_0\right)\to {\left(\frac{1}{3}\right)}^m\in ℝ$$
18	15 16 17	sylancr	$$⊢\phi \to {\left(\frac{1}{3}\right)}^m\in ℝ$$
19	1	rpnnen2lem6	$$⊢\left(A\subseteq \mathbb{N}\wedge m\in \mathbb{N}\right)\to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)\in ℝ$$
20	2 10 19	syl2anc	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)\in ℝ$$
21		nnrp	$$⊢3\in \mathbb{N}\to 3\in {ℝ}^{+}$$
22		rpreccl	$$⊢3\in {ℝ}^{+}\to \frac{1}{3}\in {ℝ}^{+}$$
23	13 21 22	mp2b	$$⊢\frac{1}{3}\in {ℝ}^{+}$$
24	10	nnzd	$$⊢\phi \to m\in \mathbb{Z}$$
25		rpexpcl	$$⊢\left(\frac{1}{3}\in {ℝ}^{+}\wedge m\in \mathbb{Z}\right)\to {\left(\frac{1}{3}\right)}^m\in {ℝ}^{+}$$
26	23 24 25	sylancr	$$⊢\phi \to {\left(\frac{1}{3}\right)}^m\in {ℝ}^{+}$$
27	26	rpred	$$⊢\phi \to {\left(\frac{1}{3}\right)}^m\in ℝ$$
28	27	rehalfcld	$$⊢\phi \to \frac{{\left(\frac{1}{3}\right)}^m}{2}\in ℝ$$
29	4	snssd	$$⊢\phi \to \left\{m\right\}\subseteq A\setminus B$$
30	2	ssdifd	$$⊢\phi \to A\setminus B\subseteq \mathbb{N}\setminus B$$
31	29 30	sstrd	$$⊢\phi \to \left\{m\right\}\subseteq \mathbb{N}\setminus B$$
32	10	snssd	$$⊢\phi \to \left\{m\right\}\subseteq \mathbb{N}$$
33		ssconb	$$⊢\left(B\subseteq \mathbb{N}\wedge \left\{m\right\}\subseteq \mathbb{N}\right)\to \left(B\subseteq \mathbb{N}\setminus \left\{m\right\}\leftrightarrow \left\{m\right\}\subseteq \mathbb{N}\setminus B\right)$$
34	3 32 33	syl2anc	$$⊢\phi \to \left(B\subseteq \mathbb{N}\setminus \left\{m\right\}\leftrightarrow \left\{m\right\}\subseteq \mathbb{N}\setminus B\right)$$
35	31 34	mpbird	$$⊢\phi \to B\subseteq \mathbb{N}\setminus \left\{m\right\}$$
36		difssd	$$⊢\phi \to \mathbb{N}\setminus \left\{m\right\}\subseteq \mathbb{N}$$
37	1	rpnnen2lem7	$$⊢\left(B\subseteq \mathbb{N}\setminus \left\{m\right\}\wedge \mathbb{N}\setminus \left\{m\right\}\subseteq \mathbb{N}\wedge m\in \mathbb{N}\right)\to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)\le \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(\mathbb{N}\setminus \left\{m\right\}\right)\left(k\right)$$
38	35 36 10 37	syl3anc	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)\le \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(\mathbb{N}\setminus \left\{m\right\}\right)\left(k\right)$$
39	1	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)$$
40	10 39	syl	$$⊢\phi \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)$$
41	15	recni	$$⊢\frac{1}{3}\in ℂ$$
42		expp1	$$⊢\left(\frac{1}{3}\in ℂ\wedge m\in {\mathbb{N}}_0\right)\to {\left(\frac{1}{3}\right)}^{m+1}={\left(\frac{1}{3}\right)}^m\left(\frac{1}{3}\right)$$
43	41 16 42	sylancr	$$⊢\phi \to {\left(\frac{1}{3}\right)}^{m+1}={\left(\frac{1}{3}\right)}^m\left(\frac{1}{3}\right)$$
44	27	recnd	$$⊢\phi \to {\left(\frac{1}{3}\right)}^m\in ℂ$$
45		3cn	$$⊢3\in ℂ$$
46		3ne0	$$⊢3\ne 0$$
47		divrec	$$⊢\left({\left(\frac{1}{3}\right)}^m\in ℂ\wedge 3\in ℂ\wedge 3\ne 0\right)\to \frac{{\left(\frac{1}{3}\right)}^m}{3}={\left(\frac{1}{3}\right)}^m\left(\frac{1}{3}\right)$$
48	45 46 47	mp3an23	$$⊢{\left(\frac{1}{3}\right)}^m\in ℂ\to \frac{{\left(\frac{1}{3}\right)}^m}{3}={\left(\frac{1}{3}\right)}^m\left(\frac{1}{3}\right)$$
49	44 48	syl	$$⊢\phi \to \frac{{\left(\frac{1}{3}\right)}^m}{3}={\left(\frac{1}{3}\right)}^m\left(\frac{1}{3}\right)$$
50	43 49	eqtr4d	$$⊢\phi \to {\left(\frac{1}{3}\right)}^{m+1}=\frac{{\left(\frac{1}{3}\right)}^m}{3}$$
51	50	oveq1d	$$⊢\phi \to \frac{{\left(\frac{1}{3}\right)}^{m+1}}{1-\left(\frac{1}{3}\right)}=\frac{\frac{{\left(\frac{1}{3}\right)}^m}{3}}{1-\left(\frac{1}{3}\right)}$$
52		ax-1cn	$$⊢1\in ℂ$$
53	45 46	pm3.2i	$$⊢\left(3\in ℂ\wedge 3\ne 0\right)$$
54		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)$$
55	45 52 53 54	mp3an	$$⊢\frac{3-1}{3}=\left(\frac{3}{3}\right)-\left(\frac{1}{3}\right)$$
56		3m1e2	$$⊢3-1=2$$
57	56	oveq1i	$$⊢\frac{3-1}{3}=\frac{2}{3}$$
58	45 46	dividi	$$⊢\frac{3}{3}=1$$
59	58	oveq1i	$$⊢\left(\frac{3}{3}\right)-\left(\frac{1}{3}\right)=1-\left(\frac{1}{3}\right)$$
60	55 57 59	3eqtr3ri	$$⊢1-\left(\frac{1}{3}\right)=\frac{2}{3}$$
61	60	oveq2i	$$⊢\frac{\frac{{\left(\frac{1}{3}\right)}^m}{3}}{1-\left(\frac{1}{3}\right)}=\frac{\frac{{\left(\frac{1}{3}\right)}^m}{3}}{\frac{2}{3}}$$
62		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
63		divcan7	$$⊢\left({\left(\frac{1}{3}\right)}^m\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\to \frac{\frac{{\left(\frac{1}{3}\right)}^m}{3}}{\frac{2}{3}}=\frac{{\left(\frac{1}{3}\right)}^m}{2}$$
64	62 53 63	mp3an23	$$⊢{\left(\frac{1}{3}\right)}^m\in ℂ\to \frac{\frac{{\left(\frac{1}{3}\right)}^m}{3}}{\frac{2}{3}}=\frac{{\left(\frac{1}{3}\right)}^m}{2}$$
65	44 64	syl	$$⊢\phi \to \frac{\frac{{\left(\frac{1}{3}\right)}^m}{3}}{\frac{2}{3}}=\frac{{\left(\frac{1}{3}\right)}^m}{2}$$
66	61 65	syl5eq	$$⊢\phi \to \frac{\frac{{\left(\frac{1}{3}\right)}^m}{3}}{1-\left(\frac{1}{3}\right)}=\frac{{\left(\frac{1}{3}\right)}^m}{2}$$
67	51 66	eqtrd	$$⊢\phi \to \frac{{\left(\frac{1}{3}\right)}^{m+1}}{1-\left(\frac{1}{3}\right)}=\frac{{\left(\frac{1}{3}\right)}^m}{2}$$
68	67	oveq2d	$$⊢\phi \to 0+\left(\frac{{\left(\frac{1}{3}\right)}^{m+1}}{1-\left(\frac{1}{3}\right)}\right)=0+\left(\frac{{\left(\frac{1}{3}\right)}^m}{2}\right)$$
69	28	recnd	$$⊢\phi \to \frac{{\left(\frac{1}{3}\right)}^m}{2}\in ℂ$$
70	69	addid2d	$$⊢\phi \to 0+\left(\frac{{\left(\frac{1}{3}\right)}^m}{2}\right)=\frac{{\left(\frac{1}{3}\right)}^m}{2}$$
71	40 68 70	3eqtrd	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(\mathbb{N}\setminus \left\{m\right\}\right)\left(k\right)=\frac{{\left(\frac{1}{3}\right)}^m}{2}$$
72	38 71	breqtrd	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)\le \frac{{\left(\frac{1}{3}\right)}^m}{2}$$
73		rphalflt	$$⊢{\left(\frac{1}{3}\right)}^m\in {ℝ}^{+}\to \frac{{\left(\frac{1}{3}\right)}^m}{2}<{\left(\frac{1}{3}\right)}^m$$
74	26 73	syl	$$⊢\phi \to \frac{{\left(\frac{1}{3}\right)}^m}{2}<{\left(\frac{1}{3}\right)}^m$$
75	12 28 27 72 74	lelttrd	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)<{\left(\frac{1}{3}\right)}^m$$
76		eluznn	$$⊢\left(m\in \mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge m}\right)\to k\in \mathbb{N}$$
77	10 76	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge m}\right)\to k\in \mathbb{N}$$
78	1	rpnnen2lem1	$$⊢\left(\left\{m\right\}\subseteq \mathbb{N}\wedge k\in \mathbb{N}\right)\to F\left(\left\{m\right\}\right)\left(k\right)=if\left(k\in \left\{m\right\},{\left(\frac{1}{3}\right)}^k,0\right)$$
79	32 77 78	syl2an2r	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge m}\right)\to F\left(\left\{m\right\}\right)\left(k\right)=if\left(k\in \left\{m\right\},{\left(\frac{1}{3}\right)}^k,0\right)$$
80	79	sumeq2dv	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(\left\{m\right\}\right)\left(k\right)=\sum _{k\in {\mathbb{Z}}_{\ge m}}if\left(k\in \left\{m\right\},{\left(\frac{1}{3}\right)}^k,0\right)$$
81		uzid	$$⊢m\in \mathbb{Z}\to m\in {\mathbb{Z}}_{\ge m}$$
82	24 81	syl	$$⊢\phi \to m\in {\mathbb{Z}}_{\ge m}$$
83	82	snssd	$$⊢\phi \to \left\{m\right\}\subseteq {\mathbb{Z}}_{\ge m}$$
84		vex	$$⊢m\in \mathrm{V}$$
85		oveq2	$$⊢k=m\to {\left(\frac{1}{3}\right)}^k={\left(\frac{1}{3}\right)}^m$$
86	85	eleq1d	$$⊢k=m\to \left({\left(\frac{1}{3}\right)}^k\in ℂ\leftrightarrow {\left(\frac{1}{3}\right)}^m\in ℂ\right)$$
87	84 86	ralsn	$$⊢\forall k\in \left\{m\right\}{\left(\frac{1}{3}\right)}^k\in ℂ\leftrightarrow {\left(\frac{1}{3}\right)}^m\in ℂ$$
88	44 87	sylibr	$$⊢\phi \to \forall k\in \left\{m\right\}{\left(\frac{1}{3}\right)}^k\in ℂ$$
89		ssidd	$$⊢\phi \to {\mathbb{Z}}_{\ge m}\subseteq {\mathbb{Z}}_{\ge m}$$
90	89	orcd	$$⊢\phi \to \left({\mathbb{Z}}_{\ge m}\subseteq {\mathbb{Z}}_{\ge m}\vee {\mathbb{Z}}_{\ge m}\in \mathrm{Fin}\right)$$
91		sumss2	$$⊢\left(\left(\left\{m\right\}\subseteq {\mathbb{Z}}_{\ge m}\wedge \forall k\in \left\{m\right\}{\left(\frac{1}{3}\right)}^k\in ℂ\right)\wedge \left({\mathbb{Z}}_{\ge m}\subseteq {\mathbb{Z}}_{\ge m}\vee {\mathbb{Z}}_{\ge m}\in \mathrm{Fin}\right)\right)\to \sum _{k\in \left\{m\right\}}{\left(\frac{1}{3}\right)}^k=\sum _{k\in {\mathbb{Z}}_{\ge m}}if\left(k\in \left\{m\right\},{\left(\frac{1}{3}\right)}^k,0\right)$$
92	83 88 90 91	syl21anc	$$⊢\phi \to \sum _{k\in \left\{m\right\}}{\left(\frac{1}{3}\right)}^k=\sum _{k\in {\mathbb{Z}}_{\ge m}}if\left(k\in \left\{m\right\},{\left(\frac{1}{3}\right)}^k,0\right)$$
93	85	sumsn	$$⊢\left(m\in \mathbb{N}\wedge {\left(\frac{1}{3}\right)}^m\in ℂ\right)\to \sum _{k\in \left\{m\right\}}{\left(\frac{1}{3}\right)}^k={\left(\frac{1}{3}\right)}^m$$
94	10 44 93	syl2anc	$$⊢\phi \to \sum _{k\in \left\{m\right\}}{\left(\frac{1}{3}\right)}^k={\left(\frac{1}{3}\right)}^m$$
95	80 92 94	3eqtr2d	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(\left\{m\right\}\right)\left(k\right)={\left(\frac{1}{3}\right)}^m$$
96	4 7	syl	$$⊢\phi \to m\in A$$
97	96	snssd	$$⊢\phi \to \left\{m\right\}\subseteq A$$
98	1	rpnnen2lem7	$$⊢\left(\left\{m\right\}\subseteq A\wedge A\subseteq \mathbb{N}\wedge m\in \mathbb{N}\right)\to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(\left\{m\right\}\right)\left(k\right)\le \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)$$
99	97 2 10 98	syl3anc	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(\left\{m\right\}\right)\left(k\right)\le \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)$$
100	95 99	eqbrtrrd	$$⊢\phi \to {\left(\frac{1}{3}\right)}^m\le \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)$$
101	12 18 20 75 100	ltletrd	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)<\sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)$$
102	12 101	gtned	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)\ne \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)$$
103	1 2 3 4 5 6	rpnnen2lem10	$$⊢\left(\phi \wedge \psi \right)\to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)=\sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)$$
104	103	ex	$$⊢\phi \to \left(\psi \to \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)=\sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)\right)$$
105	104	necon3ad	$$⊢\phi \to \left(\sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(A\right)\left(k\right)\ne \sum _{k\in {\mathbb{Z}}_{\ge m}}F\left(B\right)\left(k\right)\to \neg \psi \right)$$
106	102 105	mpd	$$⊢\phi \to \neg \psi$$