# Metamath Proof Explorer

## Theorem rpnnen2lem12

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

Ref Expression
Hypothesis rpnnen2.1 ${⊢}{F}=\left({x}\in 𝒫ℕ⟼\left({n}\in ℕ⟼if\left({n}\in {x},{\left(\frac{1}{3}\right)}^{{n}},0\right)\right)\right)$
Assertion rpnnen2lem12 ${⊢}𝒫ℕ\preccurlyeq \left[0,1\right]$

### Proof

Step Hyp Ref Expression
1 rpnnen2.1 ${⊢}{F}=\left({x}\in 𝒫ℕ⟼\left({n}\in ℕ⟼if\left({n}\in {x},{\left(\frac{1}{3}\right)}^{{n}},0\right)\right)\right)$
2 ovex ${⊢}\left[0,1\right]\in \mathrm{V}$
3 elpwi ${⊢}{y}\in 𝒫ℕ\to {y}\subseteq ℕ$
4 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
5 4 sumeq1i ${⊢}\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in {ℤ}_{\ge 1}}{F}\left({y}\right)\left({k}\right)$
6 1nn ${⊢}1\in ℕ$
7 1 rpnnen2lem6 ${⊢}\left({y}\subseteq ℕ\wedge 1\in ℕ\right)\to \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left({y}\right)\left({k}\right)\in ℝ$
8 6 7 mpan2 ${⊢}{y}\subseteq ℕ\to \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left({y}\right)\left({k}\right)\in ℝ$
9 5 8 eqeltrid ${⊢}{y}\subseteq ℕ\to \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\in ℝ$
10 3 9 syl ${⊢}{y}\in 𝒫ℕ\to \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\in ℝ$
11 1zzd ${⊢}{y}\in 𝒫ℕ\to 1\in ℤ$
12 eqidd ${⊢}\left({y}\in 𝒫ℕ\wedge {k}\in ℕ\right)\to {F}\left({y}\right)\left({k}\right)={F}\left({y}\right)\left({k}\right)$
13 1 rpnnen2lem2 ${⊢}{y}\subseteq ℕ\to {F}\left({y}\right):ℕ⟶ℝ$
14 3 13 syl ${⊢}{y}\in 𝒫ℕ\to {F}\left({y}\right):ℕ⟶ℝ$
15 14 ffvelrnda ${⊢}\left({y}\in 𝒫ℕ\wedge {k}\in ℕ\right)\to {F}\left({y}\right)\left({k}\right)\in ℝ$
16 1 rpnnen2lem5 ${⊢}\left({y}\subseteq ℕ\wedge 1\in ℕ\right)\to seq1\left(+,{F}\left({y}\right)\right)\in \mathrm{dom}⇝$
17 3 6 16 sylancl ${⊢}{y}\in 𝒫ℕ\to seq1\left(+,{F}\left({y}\right)\right)\in \mathrm{dom}⇝$
18 ssid ${⊢}ℕ\subseteq ℕ$
19 1 rpnnen2lem4 ${⊢}\left({y}\subseteq ℕ\wedge ℕ\subseteq ℕ\wedge {k}\in ℕ\right)\to \left(0\le {F}\left({y}\right)\left({k}\right)\wedge {F}\left({y}\right)\left({k}\right)\le {F}\left(ℕ\right)\left({k}\right)\right)$
20 18 19 mp3an2 ${⊢}\left({y}\subseteq ℕ\wedge {k}\in ℕ\right)\to \left(0\le {F}\left({y}\right)\left({k}\right)\wedge {F}\left({y}\right)\left({k}\right)\le {F}\left(ℕ\right)\left({k}\right)\right)$
21 20 simpld ${⊢}\left({y}\subseteq ℕ\wedge {k}\in ℕ\right)\to 0\le {F}\left({y}\right)\left({k}\right)$
22 3 21 sylan ${⊢}\left({y}\in 𝒫ℕ\wedge {k}\in ℕ\right)\to 0\le {F}\left({y}\right)\left({k}\right)$
23 4 11 12 15 17 22 isumge0 ${⊢}{y}\in 𝒫ℕ\to 0\le \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)$
24 halfre ${⊢}\frac{1}{2}\in ℝ$
25 24 a1i ${⊢}{y}\in 𝒫ℕ\to \frac{1}{2}\in ℝ$
26 1re ${⊢}1\in ℝ$
27 26 a1i ${⊢}{y}\in 𝒫ℕ\to 1\in ℝ$
28 1 rpnnen2lem7 ${⊢}\left({y}\subseteq ℕ\wedge ℕ\subseteq ℕ\wedge 1\in ℕ\right)\to \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left({y}\right)\left({k}\right)\le \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left(ℕ\right)\left({k}\right)$
29 18 6 28 mp3an23 ${⊢}{y}\subseteq ℕ\to \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left({y}\right)\left({k}\right)\le \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left(ℕ\right)\left({k}\right)$
30 3 29 syl ${⊢}{y}\in 𝒫ℕ\to \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left({y}\right)\left({k}\right)\le \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left(ℕ\right)\left({k}\right)$
31 eqid ${⊢}{ℤ}_{\ge 1}={ℤ}_{\ge 1}$
32 eqidd ${⊢}\left({y}\in 𝒫ℕ\wedge {k}\in {ℤ}_{\ge 1}\right)\to {F}\left(ℕ\right)\left({k}\right)={F}\left(ℕ\right)\left({k}\right)$
33 elnnuz ${⊢}{k}\in ℕ↔{k}\in {ℤ}_{\ge 1}$
34 1 rpnnen2lem2 ${⊢}ℕ\subseteq ℕ\to {F}\left(ℕ\right):ℕ⟶ℝ$
35 18 34 ax-mp ${⊢}{F}\left(ℕ\right):ℕ⟶ℝ$
36 35 ffvelrni ${⊢}{k}\in ℕ\to {F}\left(ℕ\right)\left({k}\right)\in ℝ$
37 36 recnd ${⊢}{k}\in ℕ\to {F}\left(ℕ\right)\left({k}\right)\in ℂ$
38 33 37 sylbir ${⊢}{k}\in {ℤ}_{\ge 1}\to {F}\left(ℕ\right)\left({k}\right)\in ℂ$
39 38 adantl ${⊢}\left({y}\in 𝒫ℕ\wedge {k}\in {ℤ}_{\ge 1}\right)\to {F}\left(ℕ\right)\left({k}\right)\in ℂ$
40 1 rpnnen2lem3 ${⊢}seq1\left(+,{F}\left(ℕ\right)\right)⇝\left(\frac{1}{2}\right)$
41 40 a1i ${⊢}{y}\in 𝒫ℕ\to seq1\left(+,{F}\left(ℕ\right)\right)⇝\left(\frac{1}{2}\right)$
42 31 11 32 39 41 isumclim ${⊢}{y}\in 𝒫ℕ\to \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left(ℕ\right)\left({k}\right)=\frac{1}{2}$
43 30 42 breqtrd ${⊢}{y}\in 𝒫ℕ\to \sum _{{k}\in {ℤ}_{\ge 1}}{F}\left({y}\right)\left({k}\right)\le \frac{1}{2}$
44 5 43 eqbrtrid ${⊢}{y}\in 𝒫ℕ\to \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\le \frac{1}{2}$
45 halflt1 ${⊢}\frac{1}{2}<1$
46 24 26 45 ltleii ${⊢}\frac{1}{2}\le 1$
47 46 a1i ${⊢}{y}\in 𝒫ℕ\to \frac{1}{2}\le 1$
48 10 25 27 44 47 letrd ${⊢}{y}\in 𝒫ℕ\to \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\le 1$
49 elicc01 ${⊢}\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\in \left[0,1\right]↔\left(\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\in ℝ\wedge 0\le \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\wedge \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\le 1\right)$
50 10 23 48 49 syl3anbrc ${⊢}{y}\in 𝒫ℕ\to \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)\in \left[0,1\right]$
51 elpwi ${⊢}{z}\in 𝒫ℕ\to {z}\subseteq ℕ$
52 ssdifss ${⊢}{y}\subseteq ℕ\to {y}\setminus {z}\subseteq ℕ$
53 ssdifss ${⊢}{z}\subseteq ℕ\to {z}\setminus {y}\subseteq ℕ$
54 unss ${⊢}\left({y}\setminus {z}\subseteq ℕ\wedge {z}\setminus {y}\subseteq ℕ\right)↔\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\subseteq ℕ$
55 54 biimpi ${⊢}\left({y}\setminus {z}\subseteq ℕ\wedge {z}\setminus {y}\subseteq ℕ\right)\to \left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\subseteq ℕ$
56 52 53 55 syl2an ${⊢}\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\to \left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\subseteq ℕ$
57 3 51 56 syl2an ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\subseteq ℕ$
58 eqss ${⊢}{y}={z}↔\left({y}\subseteq {z}\wedge {z}\subseteq {y}\right)$
59 ssdif0 ${⊢}{y}\subseteq {z}↔{y}\setminus {z}=\varnothing$
60 ssdif0 ${⊢}{z}\subseteq {y}↔{z}\setminus {y}=\varnothing$
61 59 60 anbi12i ${⊢}\left({y}\subseteq {z}\wedge {z}\subseteq {y}\right)↔\left({y}\setminus {z}=\varnothing \wedge {z}\setminus {y}=\varnothing \right)$
62 un00 ${⊢}\left({y}\setminus {z}=\varnothing \wedge {z}\setminus {y}=\varnothing \right)↔\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)=\varnothing$
63 58 61 62 3bitri ${⊢}{y}={z}↔\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)=\varnothing$
64 63 necon3bii ${⊢}{y}\ne {z}↔\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\ne \varnothing$
65 64 biimpi ${⊢}{y}\ne {z}\to \left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\ne \varnothing$
66 nnwo ${⊢}\left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\subseteq ℕ\wedge \left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\ne \varnothing \right)\to \exists {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}{m}\le {n}$
67 57 65 66 syl2an ${⊢}\left(\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\wedge {y}\ne {z}\right)\to \exists {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}{m}\le {n}$
68 67 ex ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left({y}\ne {z}\to \exists {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)$
69 57 sselda ${⊢}\left(\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\wedge {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\right)\to {m}\in ℕ$
70 df-ral ${⊢}\forall {n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}{m}\le {n}↔\forall {n}\phantom{\rule{.4em}{0ex}}\left({n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\to {m}\le {n}\right)$
71 con34b ${⊢}\left({n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\to {m}\le {n}\right)↔\left(¬{m}\le {n}\to ¬{n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\right)$
72 eldif ${⊢}{n}\in \left({y}\setminus {z}\right)↔\left({n}\in {y}\wedge ¬{n}\in {z}\right)$
73 eldif ${⊢}{n}\in \left({z}\setminus {y}\right)↔\left({n}\in {z}\wedge ¬{n}\in {y}\right)$
74 72 73 orbi12i ${⊢}\left({n}\in \left({y}\setminus {z}\right)\vee {n}\in \left({z}\setminus {y}\right)\right)↔\left(\left({n}\in {y}\wedge ¬{n}\in {z}\right)\vee \left({n}\in {z}\wedge ¬{n}\in {y}\right)\right)$
75 elun ${⊢}{n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)↔\left({n}\in \left({y}\setminus {z}\right)\vee {n}\in \left({z}\setminus {y}\right)\right)$
76 xor ${⊢}¬\left({n}\in {y}↔{n}\in {z}\right)↔\left(\left({n}\in {y}\wedge ¬{n}\in {z}\right)\vee \left({n}\in {z}\wedge ¬{n}\in {y}\right)\right)$
77 74 75 76 3bitr4ri ${⊢}¬\left({n}\in {y}↔{n}\in {z}\right)↔{n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)$
78 77 con1bii ${⊢}¬{n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)↔\left({n}\in {y}↔{n}\in {z}\right)$
79 78 imbi2i ${⊢}\left(¬{m}\le {n}\to ¬{n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\right)↔\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
80 71 79 bitri ${⊢}\left({n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\to {m}\le {n}\right)↔\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
81 80 albii ${⊢}\forall {n}\phantom{\rule{.4em}{0ex}}\left({n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\to {m}\le {n}\right)↔\forall {n}\phantom{\rule{.4em}{0ex}}\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
82 70 81 bitri ${⊢}\forall {n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}{m}\le {n}↔\forall {n}\phantom{\rule{.4em}{0ex}}\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
83 alral ${⊢}\forall {n}\phantom{\rule{.4em}{0ex}}\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
84 nnre ${⊢}{n}\in ℕ\to {n}\in ℝ$
85 nnre ${⊢}{m}\in ℕ\to {m}\in ℝ$
86 ltnle ${⊢}\left({n}\in ℝ\wedge {m}\in ℝ\right)\to \left({n}<{m}↔¬{m}\le {n}\right)$
87 84 85 86 syl2anr ${⊢}\left({m}\in ℕ\wedge {n}\in ℕ\right)\to \left({n}<{m}↔¬{m}\le {n}\right)$
88 87 imbi1d ${⊢}\left({m}\in ℕ\wedge {n}\in ℕ\right)\to \left(\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)↔\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)$
89 88 ralbidva ${⊢}{m}\in ℕ\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)$
90 83 89 syl5ibr ${⊢}{m}\in ℕ\to \left(\forall {n}\phantom{\rule{.4em}{0ex}}\left(¬{m}\le {n}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)$
91 82 90 syl5bi ${⊢}{m}\in ℕ\to \left(\forall {n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}{m}\le {n}\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)$
92 69 91 syl ${⊢}\left(\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\wedge {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\right)\to \left(\forall {n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}{m}\le {n}\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)$
93 92 reximdva ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left(\exists {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}{m}\le {n}\to \exists {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)$
94 68 93 syld ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left({y}\ne {z}\to \exists {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)$
95 rexun ${⊢}\exists {m}\in \left(\left({y}\setminus {z}\right)\cup \left({z}\setminus {y}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)↔\left(\exists {m}\in \left({y}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\vee \exists {m}\in \left({z}\setminus {y}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)$
96 94 95 syl6ib ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left({y}\ne {z}\to \left(\exists {m}\in \left({y}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\vee \exists {m}\in \left({z}\setminus {y}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)$
97 simpll ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({y}\setminus {z}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to {y}\subseteq ℕ$
98 simplr ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({y}\setminus {z}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to {z}\subseteq ℕ$
99 simprl ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({y}\setminus {z}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to {m}\in \left({y}\setminus {z}\right)$
100 simprr ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({y}\setminus {z}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
101 biid ${⊢}\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)↔\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)$
102 1 97 98 99 100 101 rpnnen2lem11 ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({y}\setminus {z}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to ¬\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)$
103 102 rexlimdvaa ${⊢}\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\to \left(\exists {m}\in \left({y}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\to ¬\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)\right)$
104 simplr ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({z}\setminus {y}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to {z}\subseteq ℕ$
105 simpll ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({z}\setminus {y}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to {y}\subseteq ℕ$
106 simprl ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({z}\setminus {y}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to {m}\in \left({z}\setminus {y}\right)$
107 simprr ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({z}\setminus {y}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
108 bicom ${⊢}\left({n}\in {z}↔{n}\in {y}\right)↔\left({n}\in {y}↔{n}\in {z}\right)$
109 108 imbi2i ${⊢}\left({n}<{m}\to \left({n}\in {z}↔{n}\in {y}\right)\right)↔\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
110 109 ralbii ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {z}↔{n}\in {y}\right)\right)↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)$
111 107 110 sylibr ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({z}\setminus {y}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {z}↔{n}\in {y}\right)\right)$
112 eqcom ${⊢}\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)↔\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)$
113 1 104 105 106 111 112 rpnnen2lem11 ${⊢}\left(\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\wedge \left({m}\in \left({z}\setminus {y}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\right)\to ¬\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)$
114 113 rexlimdvaa ${⊢}\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\to \left(\exists {m}\in \left({z}\setminus {y}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\to ¬\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)\right)$
115 103 114 jaod ${⊢}\left({y}\subseteq ℕ\wedge {z}\subseteq ℕ\right)\to \left(\left(\exists {m}\in \left({y}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\vee \exists {m}\in \left({z}\setminus {y}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\to ¬\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)\right)$
116 3 51 115 syl2an ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left(\left(\exists {m}\in \left({y}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\vee \exists {m}\in \left({z}\setminus {y}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}<{m}\to \left({n}\in {y}↔{n}\in {z}\right)\right)\right)\to ¬\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)\right)$
117 96 116 syld ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left({y}\ne {z}\to ¬\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)\right)$
118 117 necon4ad ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left(\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)\to {y}={z}\right)$
119 fveq2 ${⊢}{y}={z}\to {F}\left({y}\right)={F}\left({z}\right)$
120 119 fveq1d ${⊢}{y}={z}\to {F}\left({y}\right)\left({k}\right)={F}\left({z}\right)\left({k}\right)$
121 120 sumeq2sdv ${⊢}{y}={z}\to \sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)$
122 118 121 impbid1 ${⊢}\left({y}\in 𝒫ℕ\wedge {z}\in 𝒫ℕ\right)\to \left(\sum _{{k}\in ℕ}{F}\left({y}\right)\left({k}\right)=\sum _{{k}\in ℕ}{F}\left({z}\right)\left({k}\right)↔{y}={z}\right)$
123 50 122 dom2 ${⊢}\left[0,1\right]\in \mathrm{V}\to 𝒫ℕ\preccurlyeq \left[0,1\right]$
124 2 123 ax-mp ${⊢}𝒫ℕ\preccurlyeq \left[0,1\right]$