rpnnen1lem5 - Metamath Proof Explorer

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

Theorem rpnnen1lem5 11237

Description: Lemma for rpnnen1 11238. (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 11235	. . 3
4	1, 2	rpnnen1lem1 11233	. . . . . 6
5		qexALT 11222	. . . . . . 7
6		nnexALT 10558	. . . . . . 7
7	5, 6	elmap 7466	. . . . . 6
8	4, 7	sylib 196	. . . . 5
9		frn 5743	. . . . . 6
10		qssre 11217	. . . . . 6
11	9, 10	syl6ss 3511	. . . . 5
12	8, 11	syl 16	. . . 4
13		1nn 10567	. . . . . . . 8
14	13	ne0ii 3800	. . . . . . 7
15		fdm 5741	. . . . . . . 8
16	15	neeq1d 2734	. . . . . . 7
17	14, 16	mpbiri 233	. . . . . 6
18		dm0rn0 5229	. . . . . . 7
19	18	necon3bii 2725	. . . . . 6
20	17, 19	sylib 196	. . . . 5
21	8, 20	syl 16	. . . 4
22		breq2 4460	. . . . . . 7
23	22	ralbidv 2896	. . . . . 6
24	23	rspcev 3210	. . . . 5 $/\$
25	3, 24	mpdan 668	. . . 4
26		id 22	. . . 4
27		suprleub 10527	. . . 4 $/\$ $/\$ $/\$
28	12, 21, 25, 26, 27	syl31anc 1231	. . 3
29	3, 28	mpbird 232	. 2
30	1, 2	rpnnen1lem4 11236	. . . . . . . . 9
31		resubcl 9902	. . . . . . . . 9 $/\$
32	30, 31	mpdan 668	. . . . . . . 8
33	32	adantr 465	. . . . . . 7 $/\$
34		posdif 10066	. . . . . . . . . 10 $/\$
35	30, 34	mpancom 669	. . . . . . . . 9
36	35	biimpa 484	. . . . . . . 8 $/\$
37	36	gt0ne0d 10138	. . . . . . 7 $/\$
38	33, 37	rereccld 10392	. . . . . 6 $/\$
39		arch 10813	. . . . . 6
40	38, 39	syl 16	. . . . 5 $/\$
41	40	ex 434	. . . 4
42	1, 2	rpnnen1lem2 11234	. . . . . . . . 9 $/\$
43	42	zred 10990	. . . . . . . 8 $/\$
44	43	3adant3 1016	. . . . . . 7 $/\$ $/\$
45	44	ltp1d 10496	. . . . . 6 $/\$ $/\$
46	33, 36	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$
47		nnre 10563	. . . . . . . . . . . . . 14
48		nngt0 10585	. . . . . . . . . . . . . 14
49	47, 48	jca 532	. . . . . . . . . . . . 13 $/\$
50		ltrec1 10452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
51	46, 49, 50	syl2an 477	. . . . . . . . . . . 12 $/\$ $/\$
52	30	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$
53		nnrecre 10593	. . . . . . . . . . . . . . 15
54	53	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
55		simpll 753	. . . . . . . . . . . . . 14 $/\$ $/\$
56	52, 54, 55	ltaddsub2d 10174	. . . . . . . . . . . . 13 $/\$ $/\$
57	12	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
58		ffn 5737	. . . . . . . . . . . . . . . . . . 19
59	8, 58	syl 16	. . . . . . . . . . . . . . . . . 18
60		fnfvelrn 6029	. . . . . . . . . . . . . . . . . 18 $/\$
61	59, 60	sylan 471	. . . . . . . . . . . . . . . . 17 $/\$
62	57, 61	sseldd 3500	. . . . . . . . . . . . . . . 16 $/\$
63	30	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
64	53	adantl 466	. . . . . . . . . . . . . . . 16 $/\$
65	12, 21, 25	3jca 1176	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
66	65	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
67		suprub 10524	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
68	66, 61, 67	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$
69	62, 63, 64, 68	leadd1dd 10187	. . . . . . . . . . . . . . 15 $/\$
70	62, 64	readdcld 9640	. . . . . . . . . . . . . . . 16 $/\$
71		readdcl 9592	. . . . . . . . . . . . . . . . 17 $/\$
72	30, 53, 71	syl2an 477	. . . . . . . . . . . . . . . 16 $/\$
73		simpl 457	. . . . . . . . . . . . . . . 16 $/\$
74		lelttr 9692	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
75	74	expd 436	. . . . . . . . . . . . . . . 16 $/\$ $/\$
76	70, 72, 73, 75	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$
77	69, 76	mpd 15	. . . . . . . . . . . . . 14 $/\$
78	77	adantlr 714	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	sylbird 235	. . . . . . . . . . . 12 $/\$ $/\$
80	51, 79	sylbid 215	. . . . . . . . . . 11 $/\$ $/\$
81	42	peano2zd 10993	. . . . . . . . . . . . . . . 16 $/\$
82		oveq1 6303	. . . . . . . . . . . . . . . . . . 19
83	82	breq1d 4466	. . . . . . . . . . . . . . . . . 18
84	83, 1	elrab2 3259	. . . . . . . . . . . . . . . . 17 $/\$
85	84	biimpri 206	. . . . . . . . . . . . . . . 16 $/\$
86	81, 85	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		ssrab2 3581	. . . . . . . . . . . . . . . . . . . 20
88	1, 87	eqsstri 3529	. . . . . . . . . . . . . . . . . . 19
89		zssre 10892	. . . . . . . . . . . . . . . . . . 19
90	88, 89	sstri 3508	. . . . . . . . . . . . . . . . . 18
91	90	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
92		remulcl 9594	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	92	ancoms 453	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
94	47, 93	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
95		btwnz 10987	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
96	95	simpld 459	. . . . . . . . . . . . . . . . . . . . 21
97	94, 96	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
98		zre 10889	. . . . . . . . . . . . . . . . . . . . . . 23
99	98	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
100		simpll 753	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101	49	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
102		ltdivmul 10438	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
103	99, 100, 101, 102	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	103	rexbidva 2965	. . . . . . . . . . . . . . . . . . . 20 $/\$
105	97, 104	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$
106		rabn0 3814	. . . . . . . . . . . . . . . . . . 19
107	105, 106	sylibr 212	. . . . . . . . . . . . . . . . . 18 $/\$
108	1	neeq1i 2742	. . . . . . . . . . . . . . . . . 18
109	107, 108	sylibr 212	. . . . . . . . . . . . . . . . 17 $/\$
110	1	rabeq2i 3106	. . . . . . . . . . . . . . . . . . . 20 $/\$
111	47	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
112	111, 100, 92	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ltle 9690	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
114	99, 112, 113	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
115	103, 114	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
116	115	impr 619	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117	110, 116	sylan2b 475	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118	117	ralrimiva 2871	. . . . . . . . . . . . . . . . . 18 $/\$
119		breq2 4460	. . . . . . . . . . . . . . . . . . . 20
120	119	ralbidv 2896	. . . . . . . . . . . . . . . . . . 19
121	120	rspcev 3210	. . . . . . . . . . . . . . . . . 18 $/\$
122	94, 118, 121	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$
123	91, 109, 122	3jca 1176	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
124		suprub 10524	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125	123, 124	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	86, 125	syldan 470	. . . . . . . . . . . . . 14 $/\$ $/\$
127	126	ex 434	. . . . . . . . . . . . 13 $/\$
128	42	zcnd 10991	. . . . . . . . . . . . . . . 16 $/\$
129		1cnd 9629	. . . . . . . . . . . . . . . 16 $/\$
130		nncn 10564	. . . . . . . . . . . . . . . . . 18
131		nnne0 10589	. . . . . . . . . . . . . . . . . 18
132	130, 131	jca 532	. . . . . . . . . . . . . . . . 17 $/\$
133	132	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
134		divdir 10251	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
135	128, 129, 133, 134	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$
136	6	mptex 6144	. . . . . . . . . . . . . . . . . . 19
137	2	fvmpt2 5964	. . . . . . . . . . . . . . . . . . 19 $/\$
138	136, 137	mpan2 671	. . . . . . . . . . . . . . . . . 18
139	138	fveq1d 5874	. . . . . . . . . . . . . . . . 17
140		ovex 6324	. . . . . . . . . . . . . . . . . 18
141		eqid 2457	. . . . . . . . . . . . . . . . . . 19
142	141	fvmpt2 5964	. . . . . . . . . . . . . . . . . 18 $/\$
143	140, 142	mpan2 671	. . . . . . . . . . . . . . . . 17
144	139, 143	sylan9eq 2518	. . . . . . . . . . . . . . . 16 $/\$
145	144	oveq1d 6311	. . . . . . . . . . . . . . 15 $/\$
146	135, 145	eqtr4d 2501	. . . . . . . . . . . . . 14 $/\$
147	146	breq1d 4466	. . . . . . . . . . . . 13 $/\$
148	81	zred 10990	. . . . . . . . . . . . . 14 $/\$
149	148, 43	lenltd 9748	. . . . . . . . . . . . 13 $/\$
150	127, 147, 149	3imtr3d 267	. . . . . . . . . . . 12 $/\$
151	150	adantlr 714	. . . . . . . . . . 11 $/\$ $/\$
152	80, 151	syld 44	. . . . . . . . . 10 $/\$ $/\$
153	152	exp31 604	. . . . . . . . 9
154	153	com4l 84	. . . . . . . 8
155	154	com14 88	. . . . . . 7
156	155	3imp 1190	. . . . . 6 $/\$ $/\$
157	45, 156	mt2d 117	. . . . 5 $/\$ $/\$
158	157	rexlimdv3a 2951	. . . 4
159	41, 158	syld 44	. . 3
160	159	pm2.01d 169	. 2
161		eqlelt 9689	. . 3 $/\$ $/\$
162	30, 161	mpancom 669	. 2 $/\$
163	29, 160, 162	mpbir2and 922	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1395

wcel 1819

wne 2652

wral 2807

wrex 2808

crab 2811

cvv 3109

wss 3471

c0 3793 class class class wbr 4456

cmpt 4515

cdm 5008

crn 5009

wfn 5589

wf 5590

cfv 5594 (class class class)co 6296

cmap 7438

csup 7918

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cmul 9514

clt 9645

cle 9646

cmin 9824

cdiv 10227

cn 10556

cz 10885

cq 11207

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-sup 7919 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-n0 10817 df-z 10886 df-q 11208

This theorem is referenced by: rpnnen1 11238

W3C validator