rpnnen1lem5 - Metamath Proof Explorer

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

Theorem rpnnen1lem5 10983

Description: Lemma for rpnnen1 10984. (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 10981	. . 3
4	1, 2	rpnnen1lem1 10979	. . . . . 6
5		qexALT 10968	. . . . . . 7
6		nnexALT 10324	. . . . . . 7
7	5, 6	elmap 7241	. . . . . 6
8	4, 7	sylib 196	. . . . 5
9		frn 5565	. . . . . 6
10		qssre 10963	. . . . . 6
11	9, 10	syl6ss 3368	. . . . 5
12	8, 11	syl 16	. . . 4
13		1nn 10333	. . . . . . . 8
14		ne0i 3643	. . . . . . . 8
15	13, 14	ax-mp 5	. . . . . . 7
16		fdm 5563	. . . . . . . 8
17	16	neeq1d 2621	. . . . . . 7
18	15, 17	mpbiri 233	. . . . . 6
19		dm0rn0 5056	. . . . . . 7
20	19	necon3bii 2640	. . . . . 6
21	18, 20	sylib 196	. . . . 5
22	8, 21	syl 16	. . . 4
23		breq2 4296	. . . . . . 7
24	23	ralbidv 2735	. . . . . 6
25	24	rspcev 3073	. . . . 5 $/\$
26	3, 25	mpdan 668	. . . 4
27		id 22	. . . 4
28		suprleub 10294	. . . 4 $/\$ $/\$ $/\$
29	12, 22, 26, 27, 28	syl31anc 1221	. . 3
30	3, 29	mpbird 232	. 2
31	1, 2	rpnnen1lem4 10982	. . . . . . . . 9
32		resubcl 9673	. . . . . . . . 9 $/\$
33	31, 32	mpdan 668	. . . . . . . 8
34	33	adantr 465	. . . . . . 7 $/\$
35		posdif 9832	. . . . . . . . . 10 $/\$
36	31, 35	mpancom 669	. . . . . . . . 9
37	36	biimpa 484	. . . . . . . 8 $/\$
38	37	gt0ne0d 9904	. . . . . . 7 $/\$
39	34, 38	rereccld 10158	. . . . . 6 $/\$
40		arch 10576	. . . . . 6
41	39, 40	syl 16	. . . . 5 $/\$
42	41	ex 434	. . . 4
43	1, 2	rpnnen1lem2 10980	. . . . . . . . 9 $/\$
44	43	zred 10747	. . . . . . . 8 $/\$
45	44	3adant3 1008	. . . . . . 7 $/\$ $/\$
46	45	ltp1d 10263	. . . . . 6 $/\$ $/\$
47	34, 37	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$
48		nnre 10329	. . . . . . . . . . . . . 14
49		nngt0 10351	. . . . . . . . . . . . . 14
50	48, 49	jca 532	. . . . . . . . . . . . 13 $/\$
51		ltrec1 10219	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
52	47, 50, 51	syl2an 477	. . . . . . . . . . . 12 $/\$ $/\$
53	31	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$
54		nnrecre 10358	. . . . . . . . . . . . . . 15
55	54	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
56		simpll 753	. . . . . . . . . . . . . 14 $/\$ $/\$
57	53, 55, 56	ltaddsub2d 9940	. . . . . . . . . . . . 13 $/\$ $/\$
58	12	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
59		ffn 5559	. . . . . . . . . . . . . . . . . . 19
60	8, 59	syl 16	. . . . . . . . . . . . . . . . . 18
61		fnfvelrn 5840	. . . . . . . . . . . . . . . . . 18 $/\$
62	60, 61	sylan 471	. . . . . . . . . . . . . . . . 17 $/\$
63	58, 62	sseldd 3357	. . . . . . . . . . . . . . . 16 $/\$
64	31	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
65	54	adantl 466	. . . . . . . . . . . . . . . 16 $/\$
66	12, 22, 26	3jca 1168	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
67	66	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
68		suprub 10291	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
69	67, 62, 68	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$
70	63, 64, 65, 69	leadd1dd 9953	. . . . . . . . . . . . . . 15 $/\$
71	63, 65	readdcld 9413	. . . . . . . . . . . . . . . 16 $/\$
72		readdcl 9365	. . . . . . . . . . . . . . . . 17 $/\$
73	31, 54, 72	syl2an 477	. . . . . . . . . . . . . . . 16 $/\$
74		simpl 457	. . . . . . . . . . . . . . . 16 $/\$
75		lelttr 9465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
76	75	expd 436	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	71, 73, 74, 76	syl3anc 1218	. . . . . . . . . . . . . . 15 $/\$
78	70, 77	mpd 15	. . . . . . . . . . . . . 14 $/\$
79	78	adantlr 714	. . . . . . . . . . . . 13 $/\$ $/\$
80	57, 79	sylbird 235	. . . . . . . . . . . 12 $/\$ $/\$
81	52, 80	sylbid 215	. . . . . . . . . . 11 $/\$ $/\$
82	43	peano2zd 10750	. . . . . . . . . . . . . . . 16 $/\$
83		oveq1 6098	. . . . . . . . . . . . . . . . . . 19
84	83	breq1d 4302	. . . . . . . . . . . . . . . . . 18
85	84, 1	elrab2 3119	. . . . . . . . . . . . . . . . 17 $/\$
86	85	biimpri 206	. . . . . . . . . . . . . . . 16 $/\$
87	82, 86	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$
88		ssrab2 3437	. . . . . . . . . . . . . . . . . . . 20
89	1, 88	eqsstri 3386	. . . . . . . . . . . . . . . . . . 19
90		zssre 10653	. . . . . . . . . . . . . . . . . . 19
91	89, 90	sstri 3365	. . . . . . . . . . . . . . . . . 18
92	91	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
93		remulcl 9367	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
94	93	ancoms 453	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
95	48, 94	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
96		btwnz 10744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
97	96	simpld 459	. . . . . . . . . . . . . . . . . . . . 21
98	95, 97	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
99		zre 10650	. . . . . . . . . . . . . . . . . . . . . . 23
100	99	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101		simpll 753	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
102	50	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
103		ltdivmul 10204	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
104	100, 101, 102, 103	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
105	104	rexbidva 2732	. . . . . . . . . . . . . . . . . . . 20 $/\$
106	98, 105	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$
107		rabn0 3657	. . . . . . . . . . . . . . . . . . 19
108	106, 107	sylibr 212	. . . . . . . . . . . . . . . . . 18 $/\$
109	1	neeq1i 2618	. . . . . . . . . . . . . . . . . 18
110	108, 109	sylibr 212	. . . . . . . . . . . . . . . . 17 $/\$
111	1	rabeq2i 2969	. . . . . . . . . . . . . . . . . . . 20 $/\$
112	48	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
113	112, 101, 93	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114		ltle 9463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
115	100, 113, 114	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
116	104, 115	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
117	116	impr 619	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
118	111, 117	sylan2b 475	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119	118	ralrimiva 2799	. . . . . . . . . . . . . . . . . 18 $/\$
120		breq2 4296	. . . . . . . . . . . . . . . . . . . 20
121	120	ralbidv 2735	. . . . . . . . . . . . . . . . . . 19
122	121	rspcev 3073	. . . . . . . . . . . . . . . . . 18 $/\$
123	95, 119, 122	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$
124	92, 110, 123	3jca 1168	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125		suprub 10291	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	124, 125	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$
127	87, 126	syldan 470	. . . . . . . . . . . . . 14 $/\$ $/\$
128	127	ex 434	. . . . . . . . . . . . 13 $/\$
129	43	zcnd 10748	. . . . . . . . . . . . . . . 16 $/\$
130		1cnd 9402	. . . . . . . . . . . . . . . 16 $/\$
131		nncn 10330	. . . . . . . . . . . . . . . . . 18
132		nnne0 10354	. . . . . . . . . . . . . . . . . 18
133	131, 132	jca 532	. . . . . . . . . . . . . . . . 17 $/\$
134	133	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
135		divdir 10017	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136	129, 130, 134, 135	syl3anc 1218	. . . . . . . . . . . . . . 15 $/\$
137	6	mptex 5948	. . . . . . . . . . . . . . . . . . 19
138	2	fvmpt2 5781	. . . . . . . . . . . . . . . . . . 19 $/\$
139	137, 138	mpan2 671	. . . . . . . . . . . . . . . . . 18
140	139	fveq1d 5693	. . . . . . . . . . . . . . . . 17
141		ovex 6116	. . . . . . . . . . . . . . . . . 18
142		eqid 2443	. . . . . . . . . . . . . . . . . . 19
143	142	fvmpt2 5781	. . . . . . . . . . . . . . . . . 18 $/\$
144	141, 143	mpan2 671	. . . . . . . . . . . . . . . . 17
145	140, 144	sylan9eq 2495	. . . . . . . . . . . . . . . 16 $/\$
146	145	oveq1d 6106	. . . . . . . . . . . . . . 15 $/\$
147	136, 146	eqtr4d 2478	. . . . . . . . . . . . . 14 $/\$
148	147	breq1d 4302	. . . . . . . . . . . . 13 $/\$
149	82	zred 10747	. . . . . . . . . . . . . 14 $/\$
150	149, 44	lenltd 9520	. . . . . . . . . . . . 13 $/\$
151	128, 148, 150	3imtr3d 267	. . . . . . . . . . . 12 $/\$
152	151	adantlr 714	. . . . . . . . . . 11 $/\$ $/\$
153	81, 152	syld 44	. . . . . . . . . 10 $/\$ $/\$
154	153	exp31 604	. . . . . . . . 9
155	154	com4l 84	. . . . . . . 8
156	155	com14 88	. . . . . . 7
157	156	3imp 1181	. . . . . 6 $/\$ $/\$
158	46, 157	mt2d 117	. . . . 5 $/\$ $/\$
159	158	rexlimdv3a 2843	. . . 4
160	42, 159	syld 44	. . 3
161	160	pm2.01d 169	. 2
162		eqlelt 9462	. . 3 $/\$ $/\$
163	31, 162	mpancom 669	. 2 $/\$
164	30, 161, 163	mpbir2and 913	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wne 2606

wral 2715

wrex 2716

crab 2719

cvv 2972

wss 3328

c0 3637 class class class wbr 4292

cmpt 4350

cdm 4840

crn 4841

wfn 5413

wf 5414

cfv 5418 (class class class)co 6091

cmap 7214

csup 7690

cc 9280

cr 9281

cc0 9282

c1 9283

caddc 9285

cmul 9287

clt 9418

cle 9419

cmin 9595

cdiv 9993

cn 10322

cz 10646

cq 10953

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-inf2 7847 ax-resscn 9339 ax-1cn 9340 ax-icn 9341 ax-addcl 9342 ax-addrcl 9343 ax-mulcl 9344 ax-mulrcl 9345 ax-mulcom 9346 ax-addass 9347 ax-mulass 9348 ax-distr 9349 ax-i2m1 9350 ax-1ne0 9351 ax-1rid 9352 ax-rnegex 9353 ax-rrecex 9354 ax-cnre 9355 ax-pre-lttri 9356 ax-pre-lttrn 9357 ax-pre-ltadd 9358 ax-pre-mulgt0 9359 ax-pre-sup 9360

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-nel 2609 df-ral 2720 df-rex 2721 df-reu 2722 df-rmo 2723 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-om 6477 df-1st 6577 df-2nd 6578 df-recs 6832 df-rdg 6866 df-er 7101 df-map 7216 df-en 7311 df-dom 7312 df-sdom 7313 df-sup 7691 df-pnf 9420 df-mnf 9421 df-xr 9422 df-ltxr 9423 df-le 9424 df-sub 9597 df-neg 9598 df-div 9994 df-nn 10323 df-n0 10580 df-z 10647 df-q 10954

This theorem is referenced by: rpnnen1 10984

W3C validator