rpnnen1lem5 - Metamath Proof Explorer

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

Theorem rpnnen1lem5 11296

Description: Lemma for rpnnen1 11297. (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 11294	. . 3
4	1, 2	rpnnen1lem1 11292	. . . . . 6
5		qex 11278	. . . . . . 7
6		nnex 10617	. . . . . . 7
7	5, 6	elmap 7506	. . . . . 6
8	4, 7	sylib 200	. . . . 5
9		frn 5750	. . . . . 6
10		qssre 11276	. . . . . 6
11	9, 10	syl6ss 3477	. . . . 5
12	8, 11	syl 17	. . . 4
13		1nn 10622	. . . . . . . 8
14	13	ne0ii 3769	. . . . . . 7
15		fdm 5748	. . . . . . . 8
16	15	neeq1d 2702	. . . . . . 7
17	14, 16	mpbiri 237	. . . . . 6
18		dm0rn0 5068	. . . . . . 7
19	18	necon3bii 2693	. . . . . 6
20	17, 19	sylib 200	. . . . 5
21	8, 20	syl 17	. . . 4
22		breq2 4425	. . . . . . 7
23	22	ralbidv 2865	. . . . . 6
24	23	rspcev 3183	. . . . 5 $/\$
25	3, 24	mpdan 673	. . . 4
26		id 23	. . . 4
27		suprleub 10575	. . . 4 $/\$ $/\$ $/\$
28	12, 21, 25, 26, 27	syl31anc 1268	. . 3
29	3, 28	mpbird 236	. 2
30	1, 2	rpnnen1lem4 11295	. . . . . . . . 9
31		resubcl 9940	. . . . . . . . 9 $/\$
32	30, 31	mpdan 673	. . . . . . . 8
33	32	adantr 467	. . . . . . 7 $/\$
34		posdif 10109	. . . . . . . . . 10 $/\$
35	30, 34	mpancom 674	. . . . . . . . 9
36	35	biimpa 487	. . . . . . . 8 $/\$
37	36	gt0ne0d 10180	. . . . . . 7 $/\$
38	33, 37	rereccld 10436	. . . . . 6 $/\$
39		arch 10868	. . . . . 6
40	38, 39	syl 17	. . . . 5 $/\$
41	40	ex 436	. . . 4
42	1, 2	rpnnen1lem2 11293	. . . . . . . . 9 $/\$
43	42	zred 11042	. . . . . . . 8 $/\$
44	43	3adant3 1026	. . . . . . 7 $/\$ $/\$
45	44	ltp1d 10539	. . . . . 6 $/\$ $/\$
46	33, 36	jca 535	. . . . . . . . . . . . 13 $/\$ $/\$
47		nnre 10618	. . . . . . . . . . . . . 14
48		nngt0 10640	. . . . . . . . . . . . . 14
49	47, 48	jca 535	. . . . . . . . . . . . 13 $/\$
50		ltrec1 10495	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
51	46, 49, 50	syl2an 480	. . . . . . . . . . . 12 $/\$ $/\$
52	30	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $/\$
53		nnrecre 10648	. . . . . . . . . . . . . . 15
54	53	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$
55		simpll 759	. . . . . . . . . . . . . 14 $/\$ $/\$
56	52, 54, 55	ltaddsub2d 10216	. . . . . . . . . . . . 13 $/\$ $/\$
57	12	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
58		ffn 5744	. . . . . . . . . . . . . . . . . . 19
59	8, 58	syl 17	. . . . . . . . . . . . . . . . . 18
60		fnfvelrn 6032	. . . . . . . . . . . . . . . . . 18 $/\$
61	59, 60	sylan 474	. . . . . . . . . . . . . . . . 17 $/\$
62	57, 61	sseldd 3466	. . . . . . . . . . . . . . . 16 $/\$
63	30	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
64	53	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
65	12, 21, 25	3jca 1186	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
66	65	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
67		suprub 10572	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
68	66, 61, 67	syl2anc 666	. . . . . . . . . . . . . . . 16 $/\$
69	62, 63, 64, 68	leadd1dd 10229	. . . . . . . . . . . . . . 15 $/\$
70	62, 64	readdcld 9672	. . . . . . . . . . . . . . . 16 $/\$
71		readdcl 9624	. . . . . . . . . . . . . . . . 17 $/\$
72	30, 53, 71	syl2an 480	. . . . . . . . . . . . . . . 16 $/\$
73		simpl 459	. . . . . . . . . . . . . . . 16 $/\$
74		lelttr 9726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
75	74	expd 438	. . . . . . . . . . . . . . . 16 $/\$ $/\$
76	70, 72, 73, 75	syl3anc 1265	. . . . . . . . . . . . . . 15 $/\$
77	69, 76	mpd 15	. . . . . . . . . . . . . 14 $/\$
78	77	adantlr 720	. . . . . . . . . . . . 13 $/\$ $/\$
79	56, 78	sylbird 239	. . . . . . . . . . . 12 $/\$ $/\$
80	51, 79	sylbid 219	. . . . . . . . . . 11 $/\$ $/\$
81	42	peano2zd 11045	. . . . . . . . . . . . . . . 16 $/\$
82		oveq1 6310	. . . . . . . . . . . . . . . . . . 19
83	82	breq1d 4431	. . . . . . . . . . . . . . . . . 18
84	83, 1	elrab2 3232	. . . . . . . . . . . . . . . . 17 $/\$
85	84	biimpri 210	. . . . . . . . . . . . . . . 16 $/\$
86	81, 85	sylan 474	. . . . . . . . . . . . . . 15 $/\$ $/\$
87		ssrab2 3547	. . . . . . . . . . . . . . . . . . . 20
88	1, 87	eqsstri 3495	. . . . . . . . . . . . . . . . . . 19
89		zssre 10946	. . . . . . . . . . . . . . . . . . 19
90	88, 89	sstri 3474	. . . . . . . . . . . . . . . . . 18
91	90	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
92		remulcl 9626	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	92	ancoms 455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
94	47, 93	sylan2 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
95		btwnz 11039	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
96	95	simpld 461	. . . . . . . . . . . . . . . . . . . . 21
97	94, 96	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
98		zre 10943	. . . . . . . . . . . . . . . . . . . . . . 23
99	98	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
100		simpll 759	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101	49	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
102		ltdivmul 10482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
103	99, 100, 101, 102	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	103	rexbidva 2937	. . . . . . . . . . . . . . . . . . . 20 $/\$
105	97, 104	mpbird 236	. . . . . . . . . . . . . . . . . . 19 $/\$
106		rabn0 3783	. . . . . . . . . . . . . . . . . . 19
107	105, 106	sylibr 216	. . . . . . . . . . . . . . . . . 18 $/\$
108	1	neeq1i 2710	. . . . . . . . . . . . . . . . . 18
109	107, 108	sylibr 216	. . . . . . . . . . . . . . . . 17 $/\$
110	1	rabeq2i 3079	. . . . . . . . . . . . . . . . . . . 20 $/\$
111	47	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
112	111, 100, 92	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ltle 9724	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
114	99, 112, 113	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
115	103, 114	sylbid 219	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
116	115	impr 624	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117	110, 116	sylan2b 478	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118	117	ralrimiva 2840	. . . . . . . . . . . . . . . . . 18 $/\$
119		breq2 4425	. . . . . . . . . . . . . . . . . . . 20
120	119	ralbidv 2865	. . . . . . . . . . . . . . . . . . 19
121	120	rspcev 3183	. . . . . . . . . . . . . . . . . 18 $/\$
122	94, 118, 121	syl2anc 666	. . . . . . . . . . . . . . . . 17 $/\$
123	91, 109, 122	3jca 1186	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
124		suprub 10572	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125	123, 124	sylan 474	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	86, 125	syldan 473	. . . . . . . . . . . . . 14 $/\$ $/\$
127	126	ex 436	. . . . . . . . . . . . 13 $/\$
128	42	zcnd 11043	. . . . . . . . . . . . . . . 16 $/\$
129		1cnd 9661	. . . . . . . . . . . . . . . 16 $/\$
130		nncn 10619	. . . . . . . . . . . . . . . . . 18
131		nnne0 10644	. . . . . . . . . . . . . . . . . 18
132	130, 131	jca 535	. . . . . . . . . . . . . . . . 17 $/\$
133	132	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$
134		divdir 10295	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
135	128, 129, 133, 134	syl3anc 1265	. . . . . . . . . . . . . . 15 $/\$
136	6	mptex 6149	. . . . . . . . . . . . . . . . . . 19
137	2	fvmpt2 5971	. . . . . . . . . . . . . . . . . . 19 $/\$
138	136, 137	mpan2 676	. . . . . . . . . . . . . . . . . 18
139	138	fveq1d 5881	. . . . . . . . . . . . . . . . 17
140		ovex 6331	. . . . . . . . . . . . . . . . . 18
141		eqid 2423	. . . . . . . . . . . . . . . . . . 19
142	141	fvmpt2 5971	. . . . . . . . . . . . . . . . . 18 $/\$
143	140, 142	mpan2 676	. . . . . . . . . . . . . . . . 17
144	139, 143	sylan9eq 2484	. . . . . . . . . . . . . . . 16 $/\$
145	144	oveq1d 6318	. . . . . . . . . . . . . . 15 $/\$
146	135, 145	eqtr4d 2467	. . . . . . . . . . . . . 14 $/\$
147	146	breq1d 4431	. . . . . . . . . . . . 13 $/\$
148	81	zred 11042	. . . . . . . . . . . . . 14 $/\$
149	148, 43	lenltd 9783	. . . . . . . . . . . . 13 $/\$
150	127, 147, 149	3imtr3d 271	. . . . . . . . . . . 12 $/\$
151	150	adantlr 720	. . . . . . . . . . 11 $/\$ $/\$
152	80, 151	syld 46	. . . . . . . . . 10 $/\$ $/\$
153	152	exp31 608	. . . . . . . . 9
154	153	com4l 88	. . . . . . . 8
155	154	com14 92	. . . . . . 7
156	155	3imp 1200	. . . . . 6 $/\$ $/\$
157	45, 156	mt2d 121	. . . . 5 $/\$ $/\$
158	157	rexlimdv3a 2920	. . . 4
159	41, 158	syld 46	. . 3
160	159	pm2.01d 173	. 2
161		eqlelt 9723	. . 3 $/\$ $/\$
162	30, 161	mpancom 674	. 2 $/\$
163	29, 160, 162	mpbir2and 931	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1438

wcel 1869

wne 2619

wral 2776

wrex 2777

crab 2780

cvv 3082

wss 3437

c0 3762 class class class wbr 4421

cmpt 4480

cdm 4851

crn 4852

wfn 5594

wf 5595

cfv 5599 (class class class)co 6303

cmap 7478

csup 7958

cc 9539

cr 9540

cc0 9541

c1 9542

caddc 9544

cmul 9546

clt 9677

cle 9678

cmin 9862

cdiv 10271

cn 10611

cz 10939

cq 11266

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-er 7369 df-map 7480 df-en 7576 df-dom 7577 df-sdom 7578 df-sup 7960 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-n0 10872 df-z 10940 df-q 11267

This theorem is referenced by: rpnnen1 11297

W3C validator