rpnnen1lem5 - Metamath Proof Explorer

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

Theorem rpnnen1lem5 11259

Description: Lemma for rpnnen1 11260. (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 11257	. . 3
4	1, 2	rpnnen1lem1 11255	. . . . . 6
5		qex 11241	. . . . . . 7
6		nnex 10584	. . . . . . 7
7	5, 6	elmap 7487	. . . . . 6
8	4, 7	sylib 198	. . . . 5
9		frn 5722	. . . . . 6
10		qssre 11239	. . . . . 6
11	9, 10	syl6ss 3456	. . . . 5
12	8, 11	syl 17	. . . 4
13		1nn 10589	. . . . . . . 8
14	13	ne0ii 3747	. . . . . . 7
15		fdm 5720	. . . . . . . 8
16	15	neeq1d 2682	. . . . . . 7
17	14, 16	mpbiri 235	. . . . . 6
18		dm0rn0 5042	. . . . . . 7
19	18	necon3bii 2673	. . . . . 6
20	17, 19	sylib 198	. . . . 5
21	8, 20	syl 17	. . . 4
22		breq2 4401	. . . . . . 7
23	22	ralbidv 2845	. . . . . 6
24	23	rspcev 3162	. . . . 5 $/\$
25	3, 24	mpdan 668	. . . 4
26		id 23	. . . 4
27		suprleub 10549	. . . 4 $/\$ $/\$ $/\$
28	12, 21, 25, 26, 27	syl31anc 1235	. . 3
29	3, 28	mpbird 234	. 2
30	1, 2	rpnnen1lem4 11258	. . . . . . . . 9
31		resubcl 9921	. . . . . . . . 9 $/\$
32	30, 31	mpdan 668	. . . . . . . 8
33	32	adantr 465	. . . . . . 7 $/\$
34		posdif 10088	. . . . . . . . . 10 $/\$
35	30, 34	mpancom 669	. . . . . . . . 9
36	35	biimpa 484	. . . . . . . 8 $/\$
37	36	gt0ne0d 10159	. . . . . . 7 $/\$
38	33, 37	rereccld 10414	. . . . . 6 $/\$
39		arch 10835	. . . . . 6
40	38, 39	syl 17	. . . . 5 $/\$
41	40	ex 434	. . . 4
42	1, 2	rpnnen1lem2 11256	. . . . . . . . 9 $/\$
43	42	zred 11010	. . . . . . . 8 $/\$
44	43	3adant3 1019	. . . . . . 7 $/\$ $/\$
45	44	ltp1d 10518	. . . . . 6 $/\$ $/\$
46	33, 36	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$
47		nnre 10585	. . . . . . . . . . . . . 14
48		nngt0 10607	. . . . . . . . . . . . . 14
49	47, 48	jca 532	. . . . . . . . . . . . 13 $/\$
50		ltrec1 10474	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
51	46, 49, 50	syl2an 477	. . . . . . . . . . . 12 $/\$ $/\$
52	30	ad2antrr 726	. . . . . . . . . . . . . 14 $/\$ $/\$
53		nnrecre 10615	. . . . . . . . . . . . . . 15
54	53	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
55		simpll 754	. . . . . . . . . . . . . 14 $/\$ $/\$
56	52, 54, 55	ltaddsub2d 10195	. . . . . . . . . . . . 13 $/\$ $/\$
57	12	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
58		ffn 5716	. . . . . . . . . . . . . . . . . . 19
59	8, 58	syl 17	. . . . . . . . . . . . . . . . . 18
60		fnfvelrn 6008	. . . . . . . . . . . . . . . . . 18 $/\$
61	59, 60	sylan 471	. . . . . . . . . . . . . . . . 17 $/\$
62	57, 61	sseldd 3445	. . . . . . . . . . . . . . . 16 $/\$
63	30	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
64	53	adantl 466	. . . . . . . . . . . . . . . 16 $/\$
65	12, 21, 25	3jca 1179	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
66	65	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
67		suprub 10546	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
68	66, 61, 67	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$
69	62, 63, 64, 68	leadd1dd 10208	. . . . . . . . . . . . . . 15 $/\$
70	62, 64	readdcld 9655	. . . . . . . . . . . . . . . 16 $/\$
71		readdcl 9607	. . . . . . . . . . . . . . . . 17 $/\$
72	30, 53, 71	syl2an 477	. . . . . . . . . . . . . . . 16 $/\$
73		simpl 457	. . . . . . . . . . . . . . . 16 $/\$
74		lelttr 9708	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
75	74	expd 436	. . . . . . . . . . . . . . . 16 $/\$ $/\$
76	70, 72, 73, 75	syl3anc 1232	. . . . . . . . . . . . . . 15 $/\$
77	69, 76	mpd 15	. . . . . . . . . . . . . 14 $/\$
78	77	adantlr 715	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	sylbird 237	. . . . . . . . . . . 12 $/\$ $/\$
80	51, 79	sylbid 217	. . . . . . . . . . 11 $/\$ $/\$
81	42	peano2zd 11013	. . . . . . . . . . . . . . . 16 $/\$
82		oveq1 6287	. . . . . . . . . . . . . . . . . . 19
83	82	breq1d 4407	. . . . . . . . . . . . . . . . . 18
84	83, 1	elrab2 3211	. . . . . . . . . . . . . . . . 17 $/\$
85	84	biimpri 208	. . . . . . . . . . . . . . . 16 $/\$
86	81, 85	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		ssrab2 3526	. . . . . . . . . . . . . . . . . . . 20
88	1, 87	eqsstri 3474	. . . . . . . . . . . . . . . . . . 19
89		zssre 10914	. . . . . . . . . . . . . . . . . . 19
90	88, 89	sstri 3453	. . . . . . . . . . . . . . . . . 18
91	90	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
92		remulcl 9609	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	92	ancoms 453	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
94	47, 93	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
95		btwnz 11007	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
96	95	simpld 459	. . . . . . . . . . . . . . . . . . . . 21
97	94, 96	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
98		zre 10911	. . . . . . . . . . . . . . . . . . . . . . 23
99	98	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
100		simpll 754	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101	49	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
102		ltdivmul 10460	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
103	99, 100, 101, 102	syl3anc 1232	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	103	rexbidva 2917	. . . . . . . . . . . . . . . . . . . 20 $/\$
105	97, 104	mpbird 234	. . . . . . . . . . . . . . . . . . 19 $/\$
106		rabn0 3761	. . . . . . . . . . . . . . . . . . 19
107	105, 106	sylibr 214	. . . . . . . . . . . . . . . . . 18 $/\$
108	1	neeq1i 2690	. . . . . . . . . . . . . . . . . 18
109	107, 108	sylibr 214	. . . . . . . . . . . . . . . . 17 $/\$
110	1	rabeq2i 3058	. . . . . . . . . . . . . . . . . . . 20 $/\$
111	47	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
112	111, 100, 92	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ltle 9706	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
114	99, 112, 113	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
115	103, 114	sylbid 217	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
116	115	impr 619	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117	110, 116	sylan2b 475	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118	117	ralrimiva 2820	. . . . . . . . . . . . . . . . . 18 $/\$
119		breq2 4401	. . . . . . . . . . . . . . . . . . . 20
120	119	ralbidv 2845	. . . . . . . . . . . . . . . . . . 19
121	120	rspcev 3162	. . . . . . . . . . . . . . . . . 18 $/\$
122	94, 118, 121	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$
123	91, 109, 122	3jca 1179	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
124		suprub 10546	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125	123, 124	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	86, 125	syldan 470	. . . . . . . . . . . . . 14 $/\$ $/\$
127	126	ex 434	. . . . . . . . . . . . 13 $/\$
128	42	zcnd 11011	. . . . . . . . . . . . . . . 16 $/\$
129		1cnd 9644	. . . . . . . . . . . . . . . 16 $/\$
130		nncn 10586	. . . . . . . . . . . . . . . . . 18
131		nnne0 10611	. . . . . . . . . . . . . . . . . 18
132	130, 131	jca 532	. . . . . . . . . . . . . . . . 17 $/\$
133	132	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
134		divdir 10273	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
135	128, 129, 133, 134	syl3anc 1232	. . . . . . . . . . . . . . 15 $/\$
136	6	mptex 6126	. . . . . . . . . . . . . . . . . . 19
137	2	fvmpt2 5943	. . . . . . . . . . . . . . . . . . 19 $/\$
138	136, 137	mpan2 671	. . . . . . . . . . . . . . . . . 18
139	138	fveq1d 5853	. . . . . . . . . . . . . . . . 17
140		ovex 6308	. . . . . . . . . . . . . . . . . 18
141		eqid 2404	. . . . . . . . . . . . . . . . . . 19
142	141	fvmpt2 5943	. . . . . . . . . . . . . . . . . 18 $/\$
143	140, 142	mpan2 671	. . . . . . . . . . . . . . . . 17
144	139, 143	sylan9eq 2465	. . . . . . . . . . . . . . . 16 $/\$
145	144	oveq1d 6295	. . . . . . . . . . . . . . 15 $/\$
146	135, 145	eqtr4d 2448	. . . . . . . . . . . . . 14 $/\$
147	146	breq1d 4407	. . . . . . . . . . . . 13 $/\$
148	81	zred 11010	. . . . . . . . . . . . . 14 $/\$
149	148, 43	lenltd 9765	. . . . . . . . . . . . 13 $/\$
150	127, 147, 149	3imtr3d 269	. . . . . . . . . . . 12 $/\$
151	150	adantlr 715	. . . . . . . . . . 11 $/\$ $/\$
152	80, 151	syld 44	. . . . . . . . . 10 $/\$ $/\$
153	152	exp31 604	. . . . . . . . 9
154	153	com4l 86	. . . . . . . 8
155	154	com14 90	. . . . . . 7
156	155	3imp 1193	. . . . . 6 $/\$ $/\$
157	45, 156	mt2d 119	. . . . 5 $/\$ $/\$
158	157	rexlimdv3a 2900	. . . 4
159	41, 158	syld 44	. . 3
160	159	pm2.01d 171	. 2
161		eqlelt 9705	. . 3 $/\$ $/\$
162	30, 161	mpancom 669	. 2 $/\$
163	29, 160, 162	mpbir2and 925	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 186 $/\$ wa 369 $/\$ w3a 976

wceq 1407

wcel 1844

wne 2600

wral 2756

wrex 2757

crab 2760

cvv 3061

wss 3416

c0 3740 class class class wbr 4397

cmpt 4455

cdm 4825

crn 4826

wfn 5566

wf 5567

cfv 5571 (class class class)co 6280

cmap 7459

csup 7936

cc 9522

cr 9523

cc0 9524

c1 9525

caddc 9527

cmul 9529

clt 9660

cle 9661

cmin 9843

cdiv 10249

cn 10578

cz 10907

cq 11229

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1641 ax-4 1654 ax-5 1727 ax-6 1773 ax-7 1816 ax-8 1846 ax-9 1848 ax-10 1863 ax-11 1868 ax-12 1880 ax-13 2028 ax-ext 2382 ax-rep 4509 ax-sep 4519 ax-nul 4527 ax-pow 4574 ax-pr 4632 ax-un 6576 ax-cnex 9580 ax-resscn 9581 ax-1cn 9582 ax-icn 9583 ax-addcl 9584 ax-addrcl 9585 ax-mulcl 9586 ax-mulrcl 9587 ax-mulcom 9588 ax-addass 9589 ax-mulass 9590 ax-distr 9591 ax-i2m1 9592 ax-1ne0 9593 ax-1rid 9594 ax-rnegex 9595 ax-rrecex 9596 ax-cnre 9597 ax-pre-lttri 9598 ax-pre-lttrn 9599 ax-pre-ltadd 9600 ax-pre-mulgt0 9601 ax-pre-sup 9602

This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-nel 2603 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-tp 3979 df-op 3981 df-uni 4194 df-iun 4275 df-br 4398 df-opab 4456 df-mpt 4457 df-tr 4492 df-eprel 4736 df-id 4740 df-po 4746 df-so 4747 df-fr 4784 df-we 4786 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-pred 5369 df-ord 5415 df-on 5416 df-lim 5417 df-suc 5418 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-riota 6242 df-ov 6283 df-oprab 6284 df-mpt2 6285 df-om 6686 df-1st 6786 df-2nd 6787 df-wrecs 7015 df-recs 7077 df-rdg 7115 df-er 7350 df-map 7461 df-en 7557 df-dom 7558 df-sdom 7559 df-sup 7937 df-pnf 9662 df-mnf 9663 df-xr 9664 df-ltxr 9665 df-le 9666 df-sub 9845 df-neg 9846 df-div 10250 df-nn 10579 df-n0 10839 df-z 10908 df-q 11230

This theorem is referenced by: rpnnen1 11260

W3C validator