rpnnen1lem5 - Metamath Proof Explorer

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

Theorem rpnnen1lem5 11317

Description: Lemma for rpnnen1 11318. (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 11315	. . 3
4	1, 2	rpnnen1lem1 11313	. . . . . 6
5		qex 11299	. . . . . . 7
6		nnex 10637	. . . . . . 7
7	5, 6	elmap 7518	. . . . . 6
8	4, 7	sylib 201	. . . . 5
9		frn 5747	. . . . . 6
10		qssre 11297	. . . . . 6
11	9, 10	syl6ss 3430	. . . . 5
12	8, 11	syl 17	. . . 4
13		1nn 10642	. . . . . . . 8
14	13	ne0ii 3729	. . . . . . 7
15		fdm 5745	. . . . . . . 8
16	15	neeq1d 2702	. . . . . . 7
17	14, 16	mpbiri 241	. . . . . 6
18		dm0rn0 5057	. . . . . . 7
19	18	necon3bii 2695	. . . . . 6
20	17, 19	sylib 201	. . . . 5
21	8, 20	syl 17	. . . 4
22		breq2 4399	. . . . . . 7
23	22	ralbidv 2829	. . . . . 6
24	23	rspcev 3136	. . . . 5 $/\$
25	3, 24	mpdan 681	. . . 4
26		id 22	. . . 4
27		suprleub 10595	. . . 4 $/\$ $/\$ $/\$
28	12, 21, 25, 26, 27	syl31anc 1295	. . 3
29	3, 28	mpbird 240	. 2
30	1, 2	rpnnen1lem4 11316	. . . . . . . . 9
31		resubcl 9958	. . . . . . . . 9 $/\$
32	30, 31	mpdan 681	. . . . . . . 8
33	32	adantr 472	. . . . . . 7 $/\$
34		posdif 10128	. . . . . . . . . 10 $/\$
35	30, 34	mpancom 682	. . . . . . . . 9
36	35	biimpa 492	. . . . . . . 8 $/\$
37	36	gt0ne0d 10199	. . . . . . 7 $/\$
38	33, 37	rereccld 10456	. . . . . 6 $/\$
39		arch 10890	. . . . . 6
40	38, 39	syl 17	. . . . 5 $/\$
41	40	ex 441	. . . 4
42	1, 2	rpnnen1lem2 11314	. . . . . . . . 9 $/\$
43	42	zred 11063	. . . . . . . 8 $/\$
44	43	3adant3 1050	. . . . . . 7 $/\$ $/\$
45	44	ltp1d 10559	. . . . . 6 $/\$ $/\$
46	33, 36	jca 541	. . . . . . . . . . . . 13 $/\$ $/\$
47		nnre 10638	. . . . . . . . . . . . . 14
48		nngt0 10660	. . . . . . . . . . . . . 14
49	47, 48	jca 541	. . . . . . . . . . . . 13 $/\$
50		ltrec1 10515	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
51	46, 49, 50	syl2an 485	. . . . . . . . . . . 12 $/\$ $/\$
52	30	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$
53		nnrecre 10668	. . . . . . . . . . . . . . 15
54	53	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$
55		simpll 768	. . . . . . . . . . . . . 14 $/\$ $/\$
56	52, 54, 55	ltaddsub2d 10235	. . . . . . . . . . . . 13 $/\$ $/\$
57	12	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
58		ffn 5739	. . . . . . . . . . . . . . . . . . 19
59	8, 58	syl 17	. . . . . . . . . . . . . . . . . 18
60		fnfvelrn 6034	. . . . . . . . . . . . . . . . . 18 $/\$
61	59, 60	sylan 479	. . . . . . . . . . . . . . . . 17 $/\$
62	57, 61	sseldd 3419	. . . . . . . . . . . . . . . 16 $/\$
63	30	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
64	53	adantl 473	. . . . . . . . . . . . . . . 16 $/\$
65	12, 21, 25	3jca 1210	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
66	65	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
67		suprub 10592	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
68	66, 61, 67	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$
69	62, 63, 64, 68	leadd1dd 10248	. . . . . . . . . . . . . . 15 $/\$
70	62, 64	readdcld 9688	. . . . . . . . . . . . . . . 16 $/\$
71		readdcl 9640	. . . . . . . . . . . . . . . . 17 $/\$
72	30, 53, 71	syl2an 485	. . . . . . . . . . . . . . . 16 $/\$
73		simpl 464	. . . . . . . . . . . . . . . 16 $/\$
74		lelttr 9742	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
75	74	expd 443	. . . . . . . . . . . . . . . 16 $/\$ $/\$
76	70, 72, 73, 75	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$
77	69, 76	mpd 15	. . . . . . . . . . . . . 14 $/\$
78	77	adantlr 729	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	sylbird 243	. . . . . . . . . . . 12 $/\$ $/\$
80	51, 79	sylbid 223	. . . . . . . . . . 11 $/\$ $/\$
81	42	peano2zd 11066	. . . . . . . . . . . . . . . 16 $/\$
82		oveq1 6315	. . . . . . . . . . . . . . . . . . 19
83	82	breq1d 4405	. . . . . . . . . . . . . . . . . 18
84	83, 1	elrab2 3186	. . . . . . . . . . . . . . . . 17 $/\$
85	84	biimpri 211	. . . . . . . . . . . . . . . 16 $/\$
86	81, 85	sylan 479	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		ssrab2 3500	. . . . . . . . . . . . . . . . . . . 20
88	1, 87	eqsstri 3448	. . . . . . . . . . . . . . . . . . 19
89		zssre 10968	. . . . . . . . . . . . . . . . . . 19
90	88, 89	sstri 3427	. . . . . . . . . . . . . . . . . 18
91	90	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
92		remulcl 9642	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	92	ancoms 460	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
94	47, 93	sylan2 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
95		btwnz 11060	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
96	95	simpld 466	. . . . . . . . . . . . . . . . . . . . 21
97	94, 96	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
98		zre 10965	. . . . . . . . . . . . . . . . . . . . . . 23
99	98	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
100		simpll 768	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101	49	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
102		ltdivmul 10502	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
103	99, 100, 101, 102	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	103	rexbidva 2889	. . . . . . . . . . . . . . . . . . . 20 $/\$
105	97, 104	mpbird 240	. . . . . . . . . . . . . . . . . . 19 $/\$
106		rabn0 3755	. . . . . . . . . . . . . . . . . . 19
107	105, 106	sylibr 217	. . . . . . . . . . . . . . . . . 18 $/\$
108	1	neeq1i 2707	. . . . . . . . . . . . . . . . . 18
109	107, 108	sylibr 217	. . . . . . . . . . . . . . . . 17 $/\$
110	1	rabeq2i 3028	. . . . . . . . . . . . . . . . . . . 20 $/\$
111	47	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
112	111, 100, 92	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ltle 9740	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
114	99, 112, 113	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
115	103, 114	sylbid 223	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
116	115	impr 631	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117	110, 116	sylan2b 483	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118	117	ralrimiva 2809	. . . . . . . . . . . . . . . . . 18 $/\$
119		breq2 4399	. . . . . . . . . . . . . . . . . . . 20
120	119	ralbidv 2829	. . . . . . . . . . . . . . . . . . 19
121	120	rspcev 3136	. . . . . . . . . . . . . . . . . 18 $/\$
122	94, 118, 121	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$
123	91, 109, 122	3jca 1210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
124		suprub 10592	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125	123, 124	sylan 479	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	86, 125	syldan 478	. . . . . . . . . . . . . 14 $/\$ $/\$
127	126	ex 441	. . . . . . . . . . . . 13 $/\$
128	42	zcnd 11064	. . . . . . . . . . . . . . . 16 $/\$
129		1cnd 9677	. . . . . . . . . . . . . . . 16 $/\$
130		nncn 10639	. . . . . . . . . . . . . . . . . 18
131		nnne0 10664	. . . . . . . . . . . . . . . . . 18
132	130, 131	jca 541	. . . . . . . . . . . . . . . . 17 $/\$
133	132	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$
134		divdir 10315	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
135	128, 129, 133, 134	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$
136	6	mptex 6152	. . . . . . . . . . . . . . . . . . 19
137	2	fvmpt2 5972	. . . . . . . . . . . . . . . . . . 19 $/\$
138	136, 137	mpan2 685	. . . . . . . . . . . . . . . . . 18
139	138	fveq1d 5881	. . . . . . . . . . . . . . . . 17
140		ovex 6336	. . . . . . . . . . . . . . . . . 18
141		eqid 2471	. . . . . . . . . . . . . . . . . . 19
142	141	fvmpt2 5972	. . . . . . . . . . . . . . . . . 18 $/\$
143	140, 142	mpan2 685	. . . . . . . . . . . . . . . . 17
144	139, 143	sylan9eq 2525	. . . . . . . . . . . . . . . 16 $/\$
145	144	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$
146	135, 145	eqtr4d 2508	. . . . . . . . . . . . . 14 $/\$
147	146	breq1d 4405	. . . . . . . . . . . . 13 $/\$
148	81	zred 11063	. . . . . . . . . . . . . 14 $/\$
149	148, 43	lenltd 9798	. . . . . . . . . . . . 13 $/\$
150	127, 147, 149	3imtr3d 275	. . . . . . . . . . . 12 $/\$
151	150	adantlr 729	. . . . . . . . . . 11 $/\$ $/\$
152	80, 151	syld 44	. . . . . . . . . 10 $/\$ $/\$
153	152	exp31 615	. . . . . . . . 9
154	153	com4l 86	. . . . . . . 8
155	154	com14 90	. . . . . . 7
156	155	3imp 1224	. . . . . 6 $/\$ $/\$
157	45, 156	mt2d 121	. . . . 5 $/\$ $/\$
158	157	rexlimdv3a 2873	. . . 4
159	41, 158	syld 44	. . 3
160	159	pm2.01d 174	. 2
161		eqlelt 9739	. . 3 $/\$ $/\$
162	30, 161	mpancom 682	. 2 $/\$
163	29, 160, 162	mpbir2and 936	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

crab 2760

cvv 3031

wss 3390

c0 3722 class class class wbr 4395

cmpt 4454

cdm 4839

crn 4840

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cmap 7490

csup 7972

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

cz 10961

cq 11287

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-sup 7974 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-n0 10894 df-z 10962 df-q 11288

This theorem is referenced by: rpnnen1 11318

W3C validator