rpnnen1lem5 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rpnnen1lem5		Structured version Unicode version

Theorem rpnnen1lem5 10979

Description: Lemma for rpnnen1 10980. (Contributed by Mario Carneiro, 12-May-2013.)

**Hypotheses**
Ref	Expression
rpnnen1.1
rpnnen1.2

**Assertion**
Ref	Expression
rpnnen1lem5

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem rpnnen1lem5 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpnnen1.1	. . . 4
2		rpnnen1.2	. . . 4
3	1, 2	rpnnen1lem3 10977	. . 3
4	1, 2	rpnnen1lem1 10975	. . . . . 6
5		qexALT 10964	. . . . . . 7
6		nnexALT 10320	. . . . . . 7
7	5, 6	elmap 7237	. . . . . 6
8	4, 7	sylib 196	. . . . 5
9		frn 5562	. . . . . 6
10		qssre 10959	. . . . . 6
11	9, 10	syl6ss 3365	. . . . 5
12	8, 11	syl 16	. . . 4
13		1nn 10329	. . . . . . . 8
14		ne0i 3640	. . . . . . . 8
15	13, 14	ax-mp 5	. . . . . . 7
16		fdm 5560	. . . . . . . 8
17	16	neeq1d 2619	. . . . . . 7
18	15, 17	mpbiri 233	. . . . . 6
19		dm0rn0 5052	. . . . . . 7
20	19	necon3bii 2638	. . . . . 6
21	18, 20	sylib 196	. . . . 5
22	8, 21	syl 16	. . . 4
23		breq2 4293	. . . . . . 7
24	23	ralbidv 2733	. . . . . 6
25	24	rspcev 3070	. . . . 5 $/\$
26	3, 25	mpdan 663	. . . 4
27		id 22	. . . 4
28		suprleub 10290	. . . 4 $/\$ $/\$ $/\$
29	12, 22, 26, 27, 28	syl31anc 1216	. . 3
30	3, 29	mpbird 232	. 2
31	1, 2	rpnnen1lem4 10978	. . . . . . . . 9
32		resubcl 9669	. . . . . . . . 9 $/\$
33	31, 32	mpdan 663	. . . . . . . 8
34	33	adantr 462	. . . . . . 7 $/\$
35		posdif 9828	. . . . . . . . . 10 $/\$
36	31, 35	mpancom 664	. . . . . . . . 9
37	36	biimpa 481	. . . . . . . 8 $/\$
38	37	gt0ne0d 9900	. . . . . . 7 $/\$
39	34, 38	rereccld 10154	. . . . . 6 $/\$
40		arch 10572	. . . . . 6
41	39, 40	syl 16	. . . . 5 $/\$
42	41	ex 434	. . . 4
43	1, 2	rpnnen1lem2 10976	. . . . . . . . 9 $/\$
44	43	zred 10743	. . . . . . . 8 $/\$
45	44	3adant3 1003	. . . . . . 7 $/\$ $/\$
46	45	ltp1d 10259	. . . . . 6 $/\$ $/\$
47	34, 37	jca 529	. . . . . . . . . . . . 13 $/\$ $/\$
48		nnre 10325	. . . . . . . . . . . . . 14
49		nngt0 10347	. . . . . . . . . . . . . 14
50	48, 49	jca 529	. . . . . . . . . . . . 13 $/\$
51		ltrec1 10215	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
52	47, 50, 51	syl2an 474	. . . . . . . . . . . 12 $/\$ $/\$
53	31	ad2antrr 720	. . . . . . . . . . . . . 14 $/\$ $/\$
54		nnrecre 10354	. . . . . . . . . . . . . . 15
55	54	adantl 463	. . . . . . . . . . . . . 14 $/\$ $/\$
56		simpll 748	. . . . . . . . . . . . . 14 $/\$ $/\$
57	53, 55, 56	ltaddsub2d 9936	. . . . . . . . . . . . 13 $/\$ $/\$
58	12	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$
59		ffn 5556	. . . . . . . . . . . . . . . . . . 19
60	8, 59	syl 16	. . . . . . . . . . . . . . . . . 18
61		fnfvelrn 5837	. . . . . . . . . . . . . . . . . 18 $/\$
62	60, 61	sylan 468	. . . . . . . . . . . . . . . . 17 $/\$
63	58, 62	sseldd 3354	. . . . . . . . . . . . . . . 16 $/\$
64	31	adantr 462	. . . . . . . . . . . . . . . 16 $/\$
65	54	adantl 463	. . . . . . . . . . . . . . . 16 $/\$
66	12, 22, 26	3jca 1163	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
67	66	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
68		suprub 10287	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
69	67, 62, 68	syl2anc 656	. . . . . . . . . . . . . . . 16 $/\$
70	63, 64, 65, 69	leadd1dd 9949	. . . . . . . . . . . . . . 15 $/\$
71	63, 65	readdcld 9409	. . . . . . . . . . . . . . . 16 $/\$
72		readdcl 9361	. . . . . . . . . . . . . . . . 17 $/\$
73	31, 54, 72	syl2an 474	. . . . . . . . . . . . . . . 16 $/\$
74		simpl 454	. . . . . . . . . . . . . . . 16 $/\$
75		lelttr 9461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
76	75	exp3a 436	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	71, 73, 74, 76	syl3anc 1213	. . . . . . . . . . . . . . 15 $/\$
78	70, 77	mpd 15	. . . . . . . . . . . . . 14 $/\$
79	78	adantlr 709	. . . . . . . . . . . . 13 $/\$ $/\$
80	57, 79	sylbird 235	. . . . . . . . . . . 12 $/\$ $/\$
81	52, 80	sylbid 215	. . . . . . . . . . 11 $/\$ $/\$
82	43	peano2zd 10746	. . . . . . . . . . . . . . . 16 $/\$
83		oveq1 6097	. . . . . . . . . . . . . . . . . . 19
84	83	breq1d 4299	. . . . . . . . . . . . . . . . . 18
85	84, 1	elrab2 3116	. . . . . . . . . . . . . . . . 17 $/\$
86	85	biimpri 206	. . . . . . . . . . . . . . . 16 $/\$
87	82, 86	sylan 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
88		ssrab2 3434	. . . . . . . . . . . . . . . . . . . 20
89	1, 88	eqsstri 3383	. . . . . . . . . . . . . . . . . . 19
90		zssre 10649	. . . . . . . . . . . . . . . . . . 19
91	89, 90	sstri 3362	. . . . . . . . . . . . . . . . . 18
92	91	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
93		remulcl 9363	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
94	93	ancoms 450	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
95	48, 94	sylan2 471	. . . . . . . . . . . . . . . . . . . . 21 $/\$
96		btwnz 10740	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
97	96	simpld 456	. . . . . . . . . . . . . . . . . . . . 21
98	95, 97	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
99		zre 10646	. . . . . . . . . . . . . . . . . . . . . . 23
100	99	adantl 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101		simpll 748	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
102	50	ad2antlr 721	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
103		ltdivmul 10200	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
104	100, 101, 102, 103	syl3anc 1213	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
105	104	rexbidva 2730	. . . . . . . . . . . . . . . . . . . 20 $/\$
106	98, 105	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$
107		rabn0 3654	. . . . . . . . . . . . . . . . . . 19
108	106, 107	sylibr 212	. . . . . . . . . . . . . . . . . 18 $/\$
109	1	neeq1i 2616	. . . . . . . . . . . . . . . . . 18
110	108, 109	sylibr 212	. . . . . . . . . . . . . . . . 17 $/\$
111	1	rabeq2i 2967	. . . . . . . . . . . . . . . . . . . 20 $/\$
112	48	ad2antlr 721	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
113	112, 101, 93	syl2anc 656	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114		ltle 9459	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
115	100, 113, 114	syl2anc 656	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
116	104, 115	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
117	116	impr 616	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
118	111, 117	sylan2b 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119	118	ralrimiva 2797	. . . . . . . . . . . . . . . . . 18 $/\$
120		breq2 4293	. . . . . . . . . . . . . . . . . . . 20
121	120	ralbidv 2733	. . . . . . . . . . . . . . . . . . 19
122	121	rspcev 3070	. . . . . . . . . . . . . . . . . 18 $/\$
123	95, 119, 122	syl2anc 656	. . . . . . . . . . . . . . . . 17 $/\$
124	92, 110, 123	3jca 1163	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125		suprub 10287	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	124, 125	sylan 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
127	87, 126	syldan 467	. . . . . . . . . . . . . 14 $/\$ $/\$
128	127	ex 434	. . . . . . . . . . . . 13 $/\$
129	43	zcnd 10744	. . . . . . . . . . . . . . . 16 $/\$
130		1cnd 9398	. . . . . . . . . . . . . . . 16 $/\$
131		nncn 10326	. . . . . . . . . . . . . . . . . 18
132		nnne0 10350	. . . . . . . . . . . . . . . . . 18
133	131, 132	jca 529	. . . . . . . . . . . . . . . . 17 $/\$
134	133	adantl 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$
135		divdir 10013	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136	129, 130, 134, 135	syl3anc 1213	. . . . . . . . . . . . . . 15 $/\$
137	6	mptex 5945	. . . . . . . . . . . . . . . . . . 19
138	2	fvmpt2 5778	. . . . . . . . . . . . . . . . . . 19 $/\$
139	137, 138	mpan2 666	. . . . . . . . . . . . . . . . . 18
140	139	fveq1d 5690	. . . . . . . . . . . . . . . . 17
141		ovex 6115	. . . . . . . . . . . . . . . . . 18
142		eqid 2441	. . . . . . . . . . . . . . . . . . 19
143	142	fvmpt2 5778	. . . . . . . . . . . . . . . . . 18 $/\$
144	141, 143	mpan2 666	. . . . . . . . . . . . . . . . 17
145	140, 144	sylan9eq 2493	. . . . . . . . . . . . . . . 16 $/\$
146	145	oveq1d 6105	. . . . . . . . . . . . . . 15 $/\$
147	136, 146	eqtr4d 2476	. . . . . . . . . . . . . 14 $/\$
148	147	breq1d 4299	. . . . . . . . . . . . 13 $/\$
149	82	zred 10743	. . . . . . . . . . . . . 14 $/\$
150	149, 44	lenltd 9516	. . . . . . . . . . . . 13 $/\$
151	128, 148, 150	3imtr3d 267	. . . . . . . . . . . 12 $/\$
152	151	adantlr 709	. . . . . . . . . . 11 $/\$ $/\$
153	81, 152	syld 44	. . . . . . . . . 10 $/\$ $/\$
154	153	exp31 601	. . . . . . . . 9
155	154	com4l 84	. . . . . . . 8
156	155	com14 88	. . . . . . 7
157	156	3imp 1176	. . . . . 6 $/\$ $/\$
158	46, 157	mt2d 117	. . . . 5 $/\$ $/\$
159	158	rexlimdv3a 2841	. . . 4
160	42, 159	syld 44	. . 3
161	160	pm2.01d 169	. 2
162		eqlelt 9458	. . 3 $/\$ $/\$
163	31, 162	mpancom 664	. 2 $/\$
164	30, 161, 163	mpbir2and 908	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 960

wceq 1364

wcel 1761

wne 2604

wral 2713

wrex 2714

crab 2717

cvv 2970

wss 3325

c0 3634 class class class wbr 4289

cmpt 4347

cdm 4836

crn 4837

wfn 5410

wf 5411

cfv 5415 (class class class)co 6090

cmap 7210

csup 7686

cc 9276

cr 9277

cc0 9278

c1 9279

caddc 9281

cmul 9283

clt 9414

cle 9415

cmin 9591

cdiv 9989

cn 10318

cz 10642

cq 10949

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-er 7097 df-map 7212 df-en 7307 df-dom 7308 df-sdom 7309 df-sup 7687 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-n0 10576 df-z 10643 df-q 10950

This theorem is referenced by: rpnnen1 10980

W3C validator