opnmbllem - Metamath Proof Explorer

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

Theorem opnmbllem 22176

Description: Lemma for opnmbl 22177. (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 5848	. . . . . . . . 9
2	1	sseq1d 3516	. . . . . . . 8
3	2	elrab 3254	. . . . . . 7 $/\$
4		simprr 755	. . . . . . . 8 $/\$ $/\$
5		fvex 5858	. . . . . . . . 9
6	5	elpw 4005	. . . . . . . 8
7	4, 6	sylibr 212	. . . . . . 7 $/\$ $/\$
8	3, 7	sylan2b 473	. . . . . 6 $/\$
9	8	ralrimiva 2868	. . . . 5
10		iccf 11626	. . . . . . 7
11		ffun 5715	. . . . . . 7
12	10, 11	ax-mp 5	. . . . . 6
13		ssrab2 3571	. . . . . . . 8
14		dyadmbl.1	. . . . . . . . . . 11
15	14	dyadf 22166	. . . . . . . . . 10
16		frn 5719	. . . . . . . . . 10
17	15, 16	ax-mp 5	. . . . . . . . 9
18		inss2 3705	. . . . . . . . . 10
19		rexpssxrxp 9627	. . . . . . . . . 10
20	18, 19	sstri 3498	. . . . . . . . 9
21	17, 20	sstri 3498	. . . . . . . 8
22	13, 21	sstri 3498	. . . . . . 7
23	10	fdmi 5718	. . . . . . 7
24	22, 23	sseqtr4i 3522	. . . . . 6
25		funimass4 5899	. . . . . 6 $/\$
26	12, 24, 25	mp2an 670	. . . . 5
27	9, 26	sylibr 212	. . . 4
28		sspwuni 4404	. . . 4
29	27, 28	sylib 196	. . 3
30		eqid 2454	. . . . . . . 8
31	30	rexmet 21462	. . . . . . 7
32		eqid 2454	. . . . . . . . 9
33	30, 32	tgioo 21467	. . . . . . . 8
34	33	mopni2 21162	. . . . . . 7 $/\$ $/\$
35	31, 34	mp3an1 1309	. . . . . 6 $/\$
36		elssuni 4264	. . . . . . . . . . . 12
37		uniretop 21435	. . . . . . . . . . . 12
38	36, 37	syl6sseqr 3536	. . . . . . . . . . 11
39	38	sselda 3489	. . . . . . . . . 10 $/\$
40		rpre 11227	. . . . . . . . . 10
41	30	bl2ioo 21463	. . . . . . . . . 10 $/\$
42	39, 40, 41	syl2an 475	. . . . . . . . 9 $/\$ $/\$
43	42	sseq1d 3516	. . . . . . . 8 $/\$ $/\$
44		2re 10601	. . . . . . . . . . . 12
45		1lt2 10698	. . . . . . . . . . . 12
46		expnlbnd 12278	. . . . . . . . . . . 12 $/\$ $/\$
47	44, 45, 46	mp3an23 1314	. . . . . . . . . . 11
48	47	ad2antrl 725	. . . . . . . . . 10 $/\$ $/\$ $/\$
49	39	ad2antrr 723	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
50		2nn 10689	. . . . . . . . . . . . . . . . . . 19
51		nnnn0 10798	. . . . . . . . . . . . . . . . . . . 20
52	51	ad2antrl 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
53		nnexpcl 12161	. . . . . . . . . . . . . . . . . . 19 $/\$
54	50, 52, 53	sylancr 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	nnred 10546	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
56	49, 55	remulcld 9613	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
57		fllelt 11915	. . . . . . . . . . . . . . . 16 $/\$
58	56, 57	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	simpld 457	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
60		reflcl 11914	. . . . . . . . . . . . . . . 16
61	56, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
62	54	nngt0d 10575	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
63		ledivmul2 10417	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64	61, 49, 55, 62, 63	syl112anc 1230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
65	59, 64	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
66		peano2re 9742	. . . . . . . . . . . . . . . 16
67	61, 66	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
68	67, 54	nndivred 10580	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
69	58	simprd 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
70		ltmuldiv 10411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
71	49, 67, 55, 62, 70	syl112anc 1230	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
72	69, 71	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
73	49, 68, 72	ltled 9722	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
74	61, 54	nndivred 10580	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
75		elicc2 11592	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	74, 68, 75	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	49, 65, 73, 76	mpbir3and 1177	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
78	56	flcld 11916	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	14	dyadval 22167	. . . . . . . . . . . . . . 15 $/\$
80	78, 52, 79	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	fveq2d 5852	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
82		df-ov 6273	. . . . . . . . . . . . 13
83	81, 82	syl6eqr 2513	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	77, 83	eleqtrrd 2545	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
85		ffn 5713	. . . . . . . . . . . . . . . 16
86	15, 85	ax-mp 5	. . . . . . . . . . . . . . 15
87		fnovrn 6423	. . . . . . . . . . . . . . 15 $/\$ $/\$
88	86, 87	mp3an1 1309	. . . . . . . . . . . . . 14 $/\$
89	78, 52, 88	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
90		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
91	90	rpred 11259	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
92	49, 91	resubcld 9983	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
93	92	rexrd 9632	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	49, 91	readdcld 9612	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	rexrd 9632	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
96	74, 91	readdcld 9612	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
97	61	recnd 9611	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
98		1cnd 9601	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
99	55	recnd 9611	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
100	54	nnne0d 10576	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 99, 100	divdird 10354	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
102	54	nnrecred 10577	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
103		simprr 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
104	102, 91, 74, 103	ltadd2dd 9730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
105	101, 104	eqbrtrd 4459	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
106	49, 68, 96, 72, 105	lttrd 9732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
107	49, 91, 74	ltsubaddd 10144	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
108	106, 107	mpbird 232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
109	49, 102	readdcld 9612	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
110	74, 49, 102, 65	leadd1dd 10162	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	101, 110	eqbrtrd 4459	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 91, 49, 103	ltadd2dd 9730	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
113	68, 109, 94, 111, 112	lelttrd 9729	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
114		iccssioo 11596	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	93, 95, 108, 113, 114	syl22anc 1227	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	83, 115	eqsstrd 3523	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
117		simplrr 760	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
118	116, 117	sstrd 3499	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
119		fveq2 5848	. . . . . . . . . . . . . . 15
120	119	sseq1d 3516	. . . . . . . . . . . . . 14
121	120	elrab 3254	. . . . . . . . . . . . 13 $/\$
122	89, 118, 121	sylanbrc 662	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
123		funfvima2 6123	. . . . . . . . . . . . 13 $/\$
124	12, 24, 123	mp2an 670	. . . . . . . . . . . 12
125	122, 124	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
126		elunii 4240	. . . . . . . . . . 11 $/\$
127	84, 125, 126	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
128	48, 127	rexlimddv 2950	. . . . . . . . 9 $/\$ $/\$ $/\$
129	128	expr 613	. . . . . . . 8 $/\$ $/\$
130	43, 129	sylbid 215	. . . . . . 7 $/\$ $/\$
131	130	rexlimdva 2946	. . . . . 6 $/\$
132	35, 131	mpd 15	. . . . 5 $/\$
133	132	ex 432	. . . 4
134	133	ssrdv 3495	. . 3
135	29, 134	eqssd 3506	. 2
136		fveq2 5848	. . . . . . 7
137	136	sseq1d 3516	. . . . . 6
138		equequ1 1803	. . . . . 6
139	137, 138	imbi12d 318	. . . . 5
140	139	ralbidv 2893	. . . 4
141	140	cbvrabv 3105	. . 3
142	13	a1i 11	. . 3
143	14, 141, 142	dyadmbl 22175	. 2
144	135, 143	eqeltrrd 2543	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

wral 2804

wrex 2805

crab 2808

cin 3460

wss 3461

cpw 3999

cop 4022

cuni 4235 class class class wbr 4439

cxp 4986

cdm 4988

crn 4989

cres 4990

cima 4991

ccom 4992

wfun 5564

wfn 5565

wf 5566

cfv 5570 (class class class)co 6270

cmpt2 6272

cr 9480

cc0 9481

c1 9482

caddc 9484

cmul 9486

cxr 9616

clt 9617

cle 9618

cmin 9796

cdiv 10202

cn 10531

c2 10581

cn0 10791

cz 10860

crp 11221

cioo 11532

cicc 11535

cfl 11908

cexp 12148

cabs 13149

ctg 14927

cxmt 18598

cbl 18600

cmopn 18603

cvol 22041

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-inf2 8049 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-fal 1404 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-disj 4411 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-se 4828 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-isom 5579 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-of 6513 df-om 6674 df-1st 6773 df-2nd 6774 df-recs 7034 df-rdg 7068 df-1o 7122 df-2o 7123 df-oadd 7126 df-omul 7127 df-er 7303 df-map 7414 df-pm 7415 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-fi 7863 df-sup 7893 df-oi 7927 df-card 8311 df-acn 8314 df-cda 8539 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-div 10203 df-nn 10532 df-2 10590 df-3 10591 df-4 10592 df-n0 10792 df-z 10861 df-uz 11083 df-q 11184 df-rp 11222 df-xneg 11321 df-xadd 11322 df-xmul 11323 df-ioo 11536 df-ico 11538 df-icc 11539 df-fz 11676 df-fzo 11800 df-fl 11910 df-seq 12090 df-exp 12149 df-hash 12388 df-cj 13014 df-re 13015 df-im 13016 df-sqrt 13150 df-abs 13151 df-clim 13393 df-rlim 13394 df-sum 13591 df-rest 14912 df-topgen 14933 df-psmet 18606 df-xmet 18607 df-met 18608 df-bl 18609 df-mopn 18610 df-top 19566 df-bases 19568 df-topon 19569 df-cmp 20054 df-ovol 22042 df-vol 22043

This theorem is referenced by: opnmbl 22177

W3C validator