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 11294

Description: Lemma for rpnnen1 11295. (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 11292	. . 3
4	1, 2	rpnnen1lem1 11290	. . . . . 6
5		qex 11276	. . . . . . 7
6		nnex 10615	. . . . . . 7
7	5, 6	elmap 7500	. . . . . 6
8	4, 7	sylib 200	. . . . 5
9		frn 5735	. . . . . 6
10		qssre 11274	. . . . . 6
11	9, 10	syl6ss 3444	. . . . 5
12	8, 11	syl 17	. . . 4
13		1nn 10620	. . . . . . . 8
14	13	ne0ii 3738	. . . . . . 7
15		fdm 5733	. . . . . . . 8
16	15	neeq1d 2683	. . . . . . 7
17	14, 16	mpbiri 237	. . . . . 6
18		dm0rn0 5051	. . . . . . 7
19	18	necon3bii 2676	. . . . . 6
20	17, 19	sylib 200	. . . . 5
21	8, 20	syl 17	. . . 4
22		breq2 4406	. . . . . . 7
23	22	ralbidv 2827	. . . . . 6
24	23	rspcev 3150	. . . . 5 $/\$
25	3, 24	mpdan 674	. . . 4
26		id 22	. . . 4
27		suprleub 10573	. . . 4 $/\$ $/\$ $/\$
28	12, 21, 25, 26, 27	syl31anc 1271	. . 3
29	3, 28	mpbird 236	. 2
30	1, 2	rpnnen1lem4 11293	. . . . . . . . 9
31		resubcl 9938	. . . . . . . . 9 $/\$
32	30, 31	mpdan 674	. . . . . . . 8
33	32	adantr 467	. . . . . . 7 $/\$
34		posdif 10107	. . . . . . . . . 10 $/\$
35	30, 34	mpancom 675	. . . . . . . . 9
36	35	biimpa 487	. . . . . . . 8 $/\$
37	36	gt0ne0d 10178	. . . . . . 7 $/\$
38	33, 37	rereccld 10434	. . . . . 6 $/\$
39		arch 10866	. . . . . 6
40	38, 39	syl 17	. . . . 5 $/\$
41	40	ex 436	. . . 4
42	1, 2	rpnnen1lem2 11291	. . . . . . . . 9 $/\$
43	42	zred 11040	. . . . . . . 8 $/\$
44	43	3adant3 1028	. . . . . . 7 $/\$ $/\$
45	44	ltp1d 10537	. . . . . 6 $/\$ $/\$
46	33, 36	jca 535	. . . . . . . . . . . . 13 $/\$ $/\$
47		nnre 10616	. . . . . . . . . . . . . 14
48		nngt0 10638	. . . . . . . . . . . . . 14
49	47, 48	jca 535	. . . . . . . . . . . . 13 $/\$
50		ltrec1 10493	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
51	46, 49, 50	syl2an 480	. . . . . . . . . . . 12 $/\$ $/\$
52	30	ad2antrr 732	. . . . . . . . . . . . . 14 $/\$ $/\$
53		nnrecre 10646	. . . . . . . . . . . . . . 15
54	53	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$
55		simpll 760	. . . . . . . . . . . . . 14 $/\$ $/\$
56	52, 54, 55	ltaddsub2d 10214	. . . . . . . . . . . . 13 $/\$ $/\$
57	12	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
58		ffn 5728	. . . . . . . . . . . . . . . . . . 19
59	8, 58	syl 17	. . . . . . . . . . . . . . . . . 18
60		fnfvelrn 6019	. . . . . . . . . . . . . . . . . 18 $/\$
61	59, 60	sylan 474	. . . . . . . . . . . . . . . . 17 $/\$
62	57, 61	sseldd 3433	. . . . . . . . . . . . . . . 16 $/\$
63	30	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
64	53	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
65	12, 21, 25	3jca 1188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
66	65	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
67		suprub 10570	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
68	66, 61, 67	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$
69	62, 63, 64, 68	leadd1dd 10227	. . . . . . . . . . . . . . 15 $/\$
70	62, 64	readdcld 9670	. . . . . . . . . . . . . . . 16 $/\$
71		readdcl 9622	. . . . . . . . . . . . . . . . 17 $/\$
72	30, 53, 71	syl2an 480	. . . . . . . . . . . . . . . 16 $/\$
73		simpl 459	. . . . . . . . . . . . . . . 16 $/\$
74		lelttr 9724	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
75	74	expd 438	. . . . . . . . . . . . . . . 16 $/\$ $/\$
76	70, 72, 73, 75	syl3anc 1268	. . . . . . . . . . . . . . 15 $/\$
77	69, 76	mpd 15	. . . . . . . . . . . . . 14 $/\$
78	77	adantlr 721	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	sylbird 239	. . . . . . . . . . . 12 $/\$ $/\$
80	51, 79	sylbid 219	. . . . . . . . . . 11 $/\$ $/\$
81	42	peano2zd 11043	. . . . . . . . . . . . . . . 16 $/\$
82		oveq1 6297	. . . . . . . . . . . . . . . . . . 19
83	82	breq1d 4412	. . . . . . . . . . . . . . . . . 18
84	83, 1	elrab2 3198	. . . . . . . . . . . . . . . . 17 $/\$
85	84	biimpri 210	. . . . . . . . . . . . . . . 16 $/\$
86	81, 85	sylan 474	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		ssrab2 3514	. . . . . . . . . . . . . . . . . . . 20
88	1, 87	eqsstri 3462	. . . . . . . . . . . . . . . . . . 19
89		zssre 10944	. . . . . . . . . . . . . . . . . . 19
90	88, 89	sstri 3441	. . . . . . . . . . . . . . . . . 18
91	90	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
92		remulcl 9624	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	92	ancoms 455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
94	47, 93	sylan2 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
95		btwnz 11037	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
96	95	simpld 461	. . . . . . . . . . . . . . . . . . . . 21
97	94, 96	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
98		zre 10941	. . . . . . . . . . . . . . . . . . . . . . 23
99	98	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
100		simpll 760	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101	49	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
102		ltdivmul 10480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
103	99, 100, 101, 102	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	103	rexbidva 2898	. . . . . . . . . . . . . . . . . . . 20 $/\$
105	97, 104	mpbird 236	. . . . . . . . . . . . . . . . . . 19 $/\$
106		rabn0 3752	. . . . . . . . . . . . . . . . . . 19
107	105, 106	sylibr 216	. . . . . . . . . . . . . . . . . 18 $/\$
108	1	neeq1i 2688	. . . . . . . . . . . . . . . . . 18
109	107, 108	sylibr 216	. . . . . . . . . . . . . . . . 17 $/\$
110	1	rabeq2i 3042	. . . . . . . . . . . . . . . . . . . 20 $/\$
111	47	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
112	111, 100, 92	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ltle 9722	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
114	99, 112, 113	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
115	103, 114	sylbid 219	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
116	115	impr 625	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117	110, 116	sylan2b 478	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118	117	ralrimiva 2802	. . . . . . . . . . . . . . . . . 18 $/\$
119		breq2 4406	. . . . . . . . . . . . . . . . . . . 20
120	119	ralbidv 2827	. . . . . . . . . . . . . . . . . . 19
121	120	rspcev 3150	. . . . . . . . . . . . . . . . . 18 $/\$
122	94, 118, 121	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$
123	91, 109, 122	3jca 1188	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
124		suprub 10570	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125	123, 124	sylan 474	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	86, 125	syldan 473	. . . . . . . . . . . . . 14 $/\$ $/\$
127	126	ex 436	. . . . . . . . . . . . 13 $/\$
128	42	zcnd 11041	. . . . . . . . . . . . . . . 16 $/\$
129		1cnd 9659	. . . . . . . . . . . . . . . 16 $/\$
130		nncn 10617	. . . . . . . . . . . . . . . . . 18
131		nnne0 10642	. . . . . . . . . . . . . . . . . 18
132	130, 131	jca 535	. . . . . . . . . . . . . . . . 17 $/\$
133	132	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$
134		divdir 10293	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
135	128, 129, 133, 134	syl3anc 1268	. . . . . . . . . . . . . . 15 $/\$
136	6	mptex 6136	. . . . . . . . . . . . . . . . . . 19
137	2	fvmpt2 5957	. . . . . . . . . . . . . . . . . . 19 $/\$
138	136, 137	mpan2 677	. . . . . . . . . . . . . . . . . 18
139	138	fveq1d 5867	. . . . . . . . . . . . . . . . 17
140		ovex 6318	. . . . . . . . . . . . . . . . . 18
141		eqid 2451	. . . . . . . . . . . . . . . . . . 19
142	141	fvmpt2 5957	. . . . . . . . . . . . . . . . . 18 $/\$
143	140, 142	mpan2 677	. . . . . . . . . . . . . . . . 17
144	139, 143	sylan9eq 2505	. . . . . . . . . . . . . . . 16 $/\$
145	144	oveq1d 6305	. . . . . . . . . . . . . . 15 $/\$
146	135, 145	eqtr4d 2488	. . . . . . . . . . . . . 14 $/\$
147	146	breq1d 4412	. . . . . . . . . . . . 13 $/\$
148	81	zred 11040	. . . . . . . . . . . . . 14 $/\$
149	148, 43	lenltd 9781	. . . . . . . . . . . . 13 $/\$
150	127, 147, 149	3imtr3d 271	. . . . . . . . . . . 12 $/\$
151	150	adantlr 721	. . . . . . . . . . 11 $/\$ $/\$
152	80, 151	syld 45	. . . . . . . . . 10 $/\$ $/\$
153	152	exp31 609	. . . . . . . . 9
154	153	com4l 87	. . . . . . . 8
155	154	com14 91	. . . . . . 7
156	155	3imp 1202	. . . . . 6 $/\$ $/\$
157	45, 156	mt2d 121	. . . . 5 $/\$ $/\$
158	157	rexlimdv3a 2881	. . . 4
159	41, 158	syld 45	. . 3
160	159	pm2.01d 173	. 2
161		eqlelt 9721	. . 3 $/\$ $/\$
162	30, 161	mpancom 675	. 2 $/\$
163	29, 160, 162	mpbir2and 933	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wne 2622

wral 2737

wrex 2738

crab 2741

cvv 3045

wss 3404

c0 3731 class class class wbr 4402

cmpt 4461

cdm 4834

crn 4835

wfn 5577

wf 5578

cfv 5582 (class class class)co 6290

cmap 7472

csup 7954

cc 9537

cr 9538

cc0 9539

c1 9540

caddc 9542

cmul 9544

clt 9675

cle 9676

cmin 9860

cdiv 10269

cn 10609

cz 10937

cq 11264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-er 7363 df-map 7474 df-en 7570 df-dom 7571 df-sdom 7572 df-sup 7956 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-n0 10870 df-z 10938 df-q 11265

This theorem is referenced by: rpnnen1 11295

W3C validator