opnmbllem - Metamath Proof Explorer

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

Theorem opnmbllem 21745

Description: Lemma for opnmbl 21746. (Contributed by Mario Carneiro, 26-Mar-2015.)

**Hypothesis**
Ref	Expression
dyadmbl.1

**Assertion**
Ref	Expression
opnmbllem

Distinct variable groups:

Proof of Theorem opnmbllem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5864	. . . . . . . . 9
2	1	sseq1d 3531	. . . . . . . 8
3	2	elrab 3261	. . . . . . 7 $/\$
4		simprr 756	. . . . . . . 8 $/\$ $/\$
5		fvex 5874	. . . . . . . . 9
6	5	elpw 4016	. . . . . . . 8
7	4, 6	sylibr 212	. . . . . . 7 $/\$ $/\$
8	3, 7	sylan2b 475	. . . . . 6 $/\$
9	8	ralrimiva 2878	. . . . 5
10		iccf 11619	. . . . . . 7
11		ffun 5731	. . . . . . 7
12	10, 11	ax-mp 5	. . . . . 6
13		ssrab2 3585	. . . . . . . 8
14		dyadmbl.1	. . . . . . . . . . 11
15	14	dyadf 21735	. . . . . . . . . 10
16		frn 5735	. . . . . . . . . 10
17	15, 16	ax-mp 5	. . . . . . . . 9
18		inss2 3719	. . . . . . . . . 10
19		rexpssxrxp 9634	. . . . . . . . . 10
20	18, 19	sstri 3513	. . . . . . . . 9
21	17, 20	sstri 3513	. . . . . . . 8
22	13, 21	sstri 3513	. . . . . . 7
23	10	fdmi 5734	. . . . . . 7
24	22, 23	sseqtr4i 3537	. . . . . 6
25		funimass4 5916	. . . . . 6 $/\$
26	12, 24, 25	mp2an 672	. . . . 5
27	9, 26	sylibr 212	. . . 4
28		sspwuni 4411	. . . 4
29	27, 28	sylib 196	. . 3
30		eqid 2467	. . . . . . . 8
31	30	rexmet 21031	. . . . . . 7
32		eqid 2467	. . . . . . . . 9
33	30, 32	tgioo 21036	. . . . . . . 8
34	33	mopni2 20731	. . . . . . 7 $/\$ $/\$
35	31, 34	mp3an1 1311	. . . . . 6 $/\$
36		elssuni 4275	. . . . . . . . . . . 12
37		uniretop 21004	. . . . . . . . . . . 12
38	36, 37	syl6sseqr 3551	. . . . . . . . . . 11
39	38	sselda 3504	. . . . . . . . . 10 $/\$
40		rpre 11222	. . . . . . . . . 10
41	30	bl2ioo 21032	. . . . . . . . . 10 $/\$
42	39, 40, 41	syl2an 477	. . . . . . . . 9 $/\$ $/\$
43	42	sseq1d 3531	. . . . . . . 8 $/\$ $/\$
44		2re 10601	. . . . . . . . . . . 12
45		1lt2 10698	. . . . . . . . . . . 12
46		expnlbnd 12260	. . . . . . . . . . . 12 $/\$ $/\$
47	44, 45, 46	mp3an23 1316	. . . . . . . . . . 11
48	47	ad2antrl 727	. . . . . . . . . 10 $/\$ $/\$ $/\$
49	39	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
50		2nn 10689	. . . . . . . . . . . . . . . . . . 19
51		nnnn0 10798	. . . . . . . . . . . . . . . . . . . 20
52	51	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
53		nnexpcl 12143	. . . . . . . . . . . . . . . . . . 19 $/\$
54	50, 52, 53	sylancr 663	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	nnred 10547	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
56	49, 55	remulcld 9620	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
57		fllelt 11898	. . . . . . . . . . . . . . . 16 $/\$
58	56, 57	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	simpld 459	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
60		reflcl 11897	. . . . . . . . . . . . . . . 16
61	56, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
62	54	nngt0d 10575	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
63		ledivmul2 10418	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64	61, 49, 55, 62, 63	syl112anc 1232	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
65	59, 64	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
66		peano2re 9748	. . . . . . . . . . . . . . . 16
67	61, 66	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
68	67, 54	nndivred 10580	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
69	58	simprd 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
70		ltmuldiv 10411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
71	49, 67, 55, 62, 70	syl112anc 1232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
72	69, 71	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
73	49, 68, 72	ltled 9728	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
74	61, 54	nndivred 10580	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
75		elicc2 11585	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	74, 68, 75	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	49, 65, 73, 76	mpbir3and 1179	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
78	56	flcld 11899	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	14	dyadval 21736	. . . . . . . . . . . . . . 15 $/\$
80	78, 52, 79	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	fveq2d 5868	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
82		df-ov 6285	. . . . . . . . . . . . 13
83	81, 82	syl6eqr 2526	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	77, 83	eleqtrrd 2558	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
85		ffn 5729	. . . . . . . . . . . . . . . 16
86	15, 85	ax-mp 5	. . . . . . . . . . . . . . 15
87		fnovrn 6432	. . . . . . . . . . . . . . 15 $/\$ $/\$
88	86, 87	mp3an1 1311	. . . . . . . . . . . . . 14 $/\$
89	78, 52, 88	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
90		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
91	90	rpred 11252	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
92	49, 91	resubcld 9983	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
93	92	rexrd 9639	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	49, 91	readdcld 9619	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	rexrd 9639	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
96	74, 91	readdcld 9619	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
97	61	recnd 9618	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
98		1cnd 9608	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
99	55	recnd 9618	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
100	54	nnne0d 10576	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 99, 100	divdird 10354	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
102	54	nnrecred 10577	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
103		simprr 756	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
104	102, 91, 74, 103	ltadd2dd 9736	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
105	101, 104	eqbrtrd 4467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
106	49, 68, 96, 72, 105	lttrd 9738	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
107	49, 91, 74	ltsubaddd 10144	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
108	106, 107	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
109	49, 102	readdcld 9619	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
110	74, 49, 102, 65	leadd1dd 10162	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	101, 110	eqbrtrd 4467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 91, 49, 103	ltadd2dd 9736	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
113	68, 109, 94, 111, 112	lelttrd 9735	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
114		iccssioo 11589	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	93, 95, 108, 113, 114	syl22anc 1229	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	83, 115	eqsstrd 3538	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
117		simplrr 760	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
118	116, 117	sstrd 3514	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
119		fveq2 5864	. . . . . . . . . . . . . . 15
120	119	sseq1d 3531	. . . . . . . . . . . . . 14
121	120	elrab 3261	. . . . . . . . . . . . 13 $/\$
122	89, 118, 121	sylanbrc 664	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
123		funfvima2 6134	. . . . . . . . . . . . 13 $/\$
124	12, 24, 123	mp2an 672	. . . . . . . . . . . 12
125	122, 124	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
126		elunii 4250	. . . . . . . . . . 11 $/\$
127	84, 125, 126	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
128	48, 127	rexlimddv 2959	. . . . . . . . 9 $/\$ $/\$ $/\$
129	128	expr 615	. . . . . . . 8 $/\$ $/\$
130	43, 129	sylbid 215	. . . . . . 7 $/\$ $/\$
131	130	rexlimdva 2955	. . . . . 6 $/\$
132	35, 131	mpd 15	. . . . 5 $/\$
133	132	ex 434	. . . 4
134	133	ssrdv 3510	. . 3
135	29, 134	eqssd 3521	. 2
136		fveq2 5864	. . . . . . 7
137	136	sseq1d 3531	. . . . . 6
138		equequ1 1747	. . . . . 6
139	137, 138	imbi12d 320	. . . . 5
140	139	ralbidv 2903	. . . 4
141	140	cbvrabv 3112	. . 3
142	13	a1i 11	. . 3
143	14, 141, 142	dyadmbl 21744	. 2
144	135, 143	eqeltrrd 2556	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

wral 2814

wrex 2815

crab 2818

cin 3475

wss 3476

cpw 4010

cop 4033

cuni 4245 class class class wbr 4447

cxp 4997

cdm 4999

crn 5000

cres 5001

cima 5002

ccom 5003

wfun 5580

wfn 5581

wf 5582

cfv 5586 (class class class)co 6282

cmpt2 6284

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

cxr 9623

clt 9624

cle 9625

cmin 9801

cdiv 10202

cn 10532

c2 10581

cn0 10791

cz 10860

crp 11216

cioo 11525

cicc 11528

cfl 11891

cexp 12130

cabs 13026

ctg 14689

cxmt 18174

cbl 18176

cmopn 18179

cvol 21610

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-omul 7132 df-er 7308 df-map 7419 df-pm 7420 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-acn 8319 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-n0 10792 df-z 10861 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-seq 12072 df-exp 12131 df-hash 12370 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-clim 13270 df-rlim 13271 df-sum 13468 df-rest 14674 df-topgen 14695 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-top 19166 df-bases 19168 df-topon 19169 df-cmp 19653 df-ovol 21611 df-vol 21612

This theorem is referenced by: opnmbl 21746

W3C validator