rpnnen1lem5 - Metamath Proof Explorer

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

Theorem rpnnen1lem5 11212

Description: Lemma for rpnnen1 11213. (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 11210	. . 3
4	1, 2	rpnnen1lem1 11208	. . . . . 6
5		qexALT 11197	. . . . . . 7
6		nnexALT 10538	. . . . . . 7
7	5, 6	elmap 7447	. . . . . 6
8	4, 7	sylib 196	. . . . 5
9		frn 5737	. . . . . 6
10		qssre 11192	. . . . . 6
11	9, 10	syl6ss 3516	. . . . 5
12	8, 11	syl 16	. . . 4
13		1nn 10547	. . . . . . . 8
14		ne0i 3791	. . . . . . . 8
15	13, 14	ax-mp 5	. . . . . . 7
16		fdm 5735	. . . . . . . 8
17	16	neeq1d 2744	. . . . . . 7
18	15, 17	mpbiri 233	. . . . . 6
19		dm0rn0 5219	. . . . . . 7
20	19	necon3bii 2735	. . . . . 6
21	18, 20	sylib 196	. . . . 5
22	8, 21	syl 16	. . . 4
23		breq2 4451	. . . . . . 7
24	23	ralbidv 2903	. . . . . 6
25	24	rspcev 3214	. . . . 5 $/\$
26	3, 25	mpdan 668	. . . 4
27		id 22	. . . 4
28		suprleub 10507	. . . 4 $/\$ $/\$ $/\$
29	12, 22, 26, 27, 28	syl31anc 1231	. . 3
30	3, 29	mpbird 232	. 2
31	1, 2	rpnnen1lem4 11211	. . . . . . . . 9
32		resubcl 9883	. . . . . . . . 9 $/\$
33	31, 32	mpdan 668	. . . . . . . 8
34	33	adantr 465	. . . . . . 7 $/\$
35		posdif 10045	. . . . . . . . . 10 $/\$
36	31, 35	mpancom 669	. . . . . . . . 9
37	36	biimpa 484	. . . . . . . 8 $/\$
38	37	gt0ne0d 10117	. . . . . . 7 $/\$
39	34, 38	rereccld 10371	. . . . . 6 $/\$
40		arch 10792	. . . . . 6
41	39, 40	syl 16	. . . . 5 $/\$
42	41	ex 434	. . . 4
43	1, 2	rpnnen1lem2 11209	. . . . . . . . 9 $/\$
44	43	zred 10966	. . . . . . . 8 $/\$
45	44	3adant3 1016	. . . . . . 7 $/\$ $/\$
46	45	ltp1d 10476	. . . . . 6 $/\$ $/\$
47	34, 37	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$
48		nnre 10543	. . . . . . . . . . . . . 14
49		nngt0 10565	. . . . . . . . . . . . . 14
50	48, 49	jca 532	. . . . . . . . . . . . 13 $/\$
51		ltrec1 10432	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
52	47, 50, 51	syl2an 477	. . . . . . . . . . . 12 $/\$ $/\$
53	31	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$
54		nnrecre 10572	. . . . . . . . . . . . . . 15
55	54	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
56		simpll 753	. . . . . . . . . . . . . 14 $/\$ $/\$
57	53, 55, 56	ltaddsub2d 10153	. . . . . . . . . . . . 13 $/\$ $/\$
58	12	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
59		ffn 5731	. . . . . . . . . . . . . . . . . . 19
60	8, 59	syl 16	. . . . . . . . . . . . . . . . . 18
61		fnfvelrn 6018	. . . . . . . . . . . . . . . . . 18 $/\$
62	60, 61	sylan 471	. . . . . . . . . . . . . . . . 17 $/\$
63	58, 62	sseldd 3505	. . . . . . . . . . . . . . . 16 $/\$
64	31	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
65	54	adantl 466	. . . . . . . . . . . . . . . 16 $/\$
66	12, 22, 26	3jca 1176	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
67	66	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
68		suprub 10504	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
69	67, 62, 68	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$
70	63, 64, 65, 69	leadd1dd 10166	. . . . . . . . . . . . . . 15 $/\$
71	63, 65	readdcld 9623	. . . . . . . . . . . . . . . 16 $/\$
72		readdcl 9575	. . . . . . . . . . . . . . . . 17 $/\$
73	31, 54, 72	syl2an 477	. . . . . . . . . . . . . . . 16 $/\$
74		simpl 457	. . . . . . . . . . . . . . . 16 $/\$
75		lelttr 9675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
76	75	expd 436	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	71, 73, 74, 76	syl3anc 1228	. . . . . . . . . . . . . . 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 10969	. . . . . . . . . . . . . . . 16 $/\$
83		oveq1 6291	. . . . . . . . . . . . . . . . . . 19
84	83	breq1d 4457	. . . . . . . . . . . . . . . . . 18
85	84, 1	elrab2 3263	. . . . . . . . . . . . . . . . 17 $/\$
86	85	biimpri 206	. . . . . . . . . . . . . . . 16 $/\$
87	82, 86	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$
88		ssrab2 3585	. . . . . . . . . . . . . . . . . . . 20
89	1, 88	eqsstri 3534	. . . . . . . . . . . . . . . . . . 19
90		zssre 10871	. . . . . . . . . . . . . . . . . . 19
91	89, 90	sstri 3513	. . . . . . . . . . . . . . . . . 18
92	91	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
93		remulcl 9577	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
94	93	ancoms 453	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
95	48, 94	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
96		btwnz 10963	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
97	96	simpld 459	. . . . . . . . . . . . . . . . . . . . 21
98	95, 97	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
99		zre 10868	. . . . . . . . . . . . . . . . . . . . . . 23
100	99	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101		simpll 753	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
102	50	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
103		ltdivmul 10417	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
104	100, 101, 102, 103	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
105	104	rexbidva 2970	. . . . . . . . . . . . . . . . . . . 20 $/\$
106	98, 105	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$
107		rabn0 3805	. . . . . . . . . . . . . . . . . . 19
108	106, 107	sylibr 212	. . . . . . . . . . . . . . . . . 18 $/\$
109	1	neeq1i 2752	. . . . . . . . . . . . . . . . . 18
110	108, 109	sylibr 212	. . . . . . . . . . . . . . . . 17 $/\$
111	1	rabeq2i 3110	. . . . . . . . . . . . . . . . . . . 20 $/\$
112	48	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
113	112, 101, 93	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114		ltle 9673	. . . . . . . . . . . . . . . . . . . . . . 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 2878	. . . . . . . . . . . . . . . . . 18 $/\$
120		breq2 4451	. . . . . . . . . . . . . . . . . . . 20
121	120	ralbidv 2903	. . . . . . . . . . . . . . . . . . 19
122	121	rspcev 3214	. . . . . . . . . . . . . . . . . 18 $/\$
123	95, 119, 122	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$
124	92, 110, 123	3jca 1176	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125		suprub 10504	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	124, 125	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$
127	87, 126	syldan 470	. . . . . . . . . . . . . 14 $/\$ $/\$
128	127	ex 434	. . . . . . . . . . . . 13 $/\$
129	43	zcnd 10967	. . . . . . . . . . . . . . . 16 $/\$
130		1cnd 9612	. . . . . . . . . . . . . . . 16 $/\$
131		nncn 10544	. . . . . . . . . . . . . . . . . 18
132		nnne0 10568	. . . . . . . . . . . . . . . . . 18
133	131, 132	jca 532	. . . . . . . . . . . . . . . . 17 $/\$
134	133	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
135		divdir 10230	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136	129, 130, 134, 135	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$
137	6	mptex 6131	. . . . . . . . . . . . . . . . . . 19
138	2	fvmpt2 5957	. . . . . . . . . . . . . . . . . . 19 $/\$
139	137, 138	mpan2 671	. . . . . . . . . . . . . . . . . 18
140	139	fveq1d 5868	. . . . . . . . . . . . . . . . 17
141		ovex 6309	. . . . . . . . . . . . . . . . . 18
142		eqid 2467	. . . . . . . . . . . . . . . . . . 19
143	142	fvmpt2 5957	. . . . . . . . . . . . . . . . . 18 $/\$
144	141, 143	mpan2 671	. . . . . . . . . . . . . . . . 17
145	140, 144	sylan9eq 2528	. . . . . . . . . . . . . . . 16 $/\$
146	145	oveq1d 6299	. . . . . . . . . . . . . . 15 $/\$
147	136, 146	eqtr4d 2511	. . . . . . . . . . . . . 14 $/\$
148	147	breq1d 4457	. . . . . . . . . . . . 13 $/\$
149	82	zred 10966	. . . . . . . . . . . . . 14 $/\$
150	149, 44	lenltd 9730	. . . . . . . . . . . . 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 1190	. . . . . 6 $/\$ $/\$
158	46, 157	mt2d 117	. . . . 5 $/\$ $/\$
159	158	rexlimdv3a 2957	. . . 4
160	42, 159	syld 44	. . 3
161	160	pm2.01d 169	. 2
162		eqlelt 9672	. . 3 $/\$ $/\$
163	31, 162	mpancom 669	. 2 $/\$
164	30, 161, 163	mpbir2and 920	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wcel 1767

wne 2662

wral 2814

wrex 2815

crab 2818

cvv 3113

wss 3476

c0 3785 class class class wbr 4447

cmpt 4505

cdm 4999

crn 5000

wfn 5583

wf 5584

cfv 5588 (class class class)co 6284

cmap 7420

csup 7900

cc 9490

cr 9491

cc0 9492

c1 9493

caddc 9495

cmul 9497

clt 9628

cle 9629

cmin 9805

cdiv 10206

cn 10536

cz 10864

cq 11182

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-er 7311 df-map 7422 df-en 7517 df-dom 7518 df-sdom 7519 df-sup 7901 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-n0 10796 df-z 10865 df-q 11183

This theorem is referenced by: rpnnen1 11213

W3C validator