opnmbllem - Metamath Proof Explorer

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

Theorem opnmbllem 22559

Description: Lemma for opnmbl 22560. (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 5865	. . . . . . . . 9
2	1	sseq1d 3459	. . . . . . . 8
3	2	elrab 3196	. . . . . . 7 $/\$
4		simprr 766	. . . . . . . 8 $/\$ $/\$
5		fvex 5875	. . . . . . . . 9
6	5	elpw 3957	. . . . . . . 8
7	4, 6	sylibr 216	. . . . . . 7 $/\$ $/\$
8	3, 7	sylan2b 478	. . . . . 6 $/\$
9	8	ralrimiva 2802	. . . . 5
10		iccf 11733	. . . . . . 7
11		ffun 5731	. . . . . . 7
12	10, 11	ax-mp 5	. . . . . 6
13		ssrab2 3514	. . . . . . . 8
14		dyadmbl.1	. . . . . . . . . . 11
15	14	dyadf 22549	. . . . . . . . . 10
16		frn 5735	. . . . . . . . . 10
17	15, 16	ax-mp 5	. . . . . . . . 9
18		inss2 3653	. . . . . . . . . 10
19		rexpssxrxp 9685	. . . . . . . . . 10
20	18, 19	sstri 3441	. . . . . . . . 9
21	17, 20	sstri 3441	. . . . . . . 8
22	13, 21	sstri 3441	. . . . . . 7
23	10	fdmi 5734	. . . . . . 7
24	22, 23	sseqtr4i 3465	. . . . . 6
25		funimass4 5916	. . . . . 6 $/\$
26	12, 24, 25	mp2an 678	. . . . 5
27	9, 26	sylibr 216	. . . 4
28		sspwuni 4367	. . . 4
29	27, 28	sylib 200	. . 3
30		eqid 2451	. . . . . . . 8
31	30	rexmet 21809	. . . . . . 7
32		eqid 2451	. . . . . . . . 9
33	30, 32	tgioo 21814	. . . . . . . 8
34	33	mopni2 21508	. . . . . . 7 $/\$ $/\$
35	31, 34	mp3an1 1351	. . . . . 6 $/\$
36		elssuni 4227	. . . . . . . . . . . 12
37		uniretop 21783	. . . . . . . . . . . 12
38	36, 37	syl6sseqr 3479	. . . . . . . . . . 11
39	38	sselda 3432	. . . . . . . . . 10 $/\$
40		rpre 11308	. . . . . . . . . 10
41	30	bl2ioo 21810	. . . . . . . . . 10 $/\$
42	39, 40, 41	syl2an 480	. . . . . . . . 9 $/\$ $/\$
43	42	sseq1d 3459	. . . . . . . 8 $/\$ $/\$
44		2re 10679	. . . . . . . . . . . 12
45		1lt2 10776	. . . . . . . . . . . 12
46		expnlbnd 12402	. . . . . . . . . . . 12 $/\$ $/\$
47	44, 45, 46	mp3an23 1356	. . . . . . . . . . 11
48	47	ad2antrl 734	. . . . . . . . . 10 $/\$ $/\$ $/\$
49	39	ad2antrr 732	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
50		2nn 10767	. . . . . . . . . . . . . . . . . . 19
51		nnnn0 10876	. . . . . . . . . . . . . . . . . . . 20
52	51	ad2antrl 734	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
53		nnexpcl 12285	. . . . . . . . . . . . . . . . . . 19 $/\$
54	50, 52, 53	sylancr 669	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	nnred 10624	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
56	49, 55	remulcld 9671	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
57		fllelt 12033	. . . . . . . . . . . . . . . 16 $/\$
58	56, 57	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	simpld 461	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
60		reflcl 12032	. . . . . . . . . . . . . . . 16
61	56, 60	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
62	54	nngt0d 10653	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
63		ledivmul2 10484	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64	61, 49, 55, 62, 63	syl112anc 1272	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
65	59, 64	mpbird 236	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
66		peano2re 9806	. . . . . . . . . . . . . . . 16
67	61, 66	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
68	67, 54	nndivred 10658	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
69	58	simprd 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
70		ltmuldiv 10478	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
71	49, 67, 55, 62, 70	syl112anc 1272	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
72	69, 71	mpbid 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
73	49, 68, 72	ltled 9783	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
74	61, 54	nndivred 10658	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
75		elicc2 11699	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	74, 68, 75	syl2anc 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	49, 65, 73, 76	mpbir3and 1191	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
78	56	flcld 12034	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
79	14	dyadval 22550	. . . . . . . . . . . . . . 15 $/\$
80	78, 52, 79	syl2anc 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	fveq2d 5869	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
82		df-ov 6293	. . . . . . . . . . . . 13
83	81, 82	syl6eqr 2503	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	77, 83	eleqtrrd 2532	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
85		ffn 5728	. . . . . . . . . . . . . . . 16
86	15, 85	ax-mp 5	. . . . . . . . . . . . . . 15
87		fnovrn 6444	. . . . . . . . . . . . . . 15 $/\$ $/\$
88	86, 87	mp3an1 1351	. . . . . . . . . . . . . 14 $/\$
89	78, 52, 88	syl2anc 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
90		simplrl 770	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
91	90	rpred 11341	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
92	49, 91	resubcld 10047	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
93	92	rexrd 9690	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
94	49, 91	readdcld 9670	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	rexrd 9690	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
96	74, 91	readdcld 9670	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
97	61	recnd 9669	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
98		1cnd 9659	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
99	55	recnd 9669	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
100	54	nnne0d 10654	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 99, 100	divdird 10421	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
102	54	nnrecred 10655	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
103		simprr 766	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
104	102, 91, 74, 103	ltadd2dd 9794	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
105	101, 104	eqbrtrd 4423	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
106	49, 68, 96, 72, 105	lttrd 9796	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
107	49, 91, 74	ltsubaddd 10209	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
108	106, 107	mpbird 236	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
109	49, 102	readdcld 9670	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
110	74, 49, 102, 65	leadd1dd 10227	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	101, 110	eqbrtrd 4423	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 91, 49, 103	ltadd2dd 9794	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
113	68, 109, 94, 111, 112	lelttrd 9793	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
114		iccssioo 11703	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	93, 95, 108, 113, 114	syl22anc 1269	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	83, 115	eqsstrd 3466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
117		simplrr 771	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
118	116, 117	sstrd 3442	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
119		fveq2 5865	. . . . . . . . . . . . . . 15
120	119	sseq1d 3459	. . . . . . . . . . . . . 14
121	120	elrab 3196	. . . . . . . . . . . . 13 $/\$
122	89, 118, 121	sylanbrc 670	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
123		funfvima2 6141	. . . . . . . . . . . . 13 $/\$
124	12, 24, 123	mp2an 678	. . . . . . . . . . . 12
125	122, 124	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
126		elunii 4203	. . . . . . . . . . 11 $/\$
127	84, 125, 126	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
128	48, 127	rexlimddv 2883	. . . . . . . . 9 $/\$ $/\$ $/\$
129	128	expr 620	. . . . . . . 8 $/\$ $/\$
130	43, 129	sylbid 219	. . . . . . 7 $/\$ $/\$
131	130	rexlimdva 2879	. . . . . 6 $/\$
132	35, 131	mpd 15	. . . . 5 $/\$
133	132	ex 436	. . . 4
134	133	ssrdv 3438	. . 3
135	29, 134	eqssd 3449	. 2
136		fveq2 5865	. . . . . . 7
137	136	sseq1d 3459	. . . . . 6
138		equequ1 1867	. . . . . 6
139	137, 138	imbi12d 322	. . . . 5
140	139	ralbidv 2827	. . . 4
141	140	cbvrabv 3044	. . 3
142	13	a1i 11	. . 3
143	14, 141, 142	dyadmbl 22558	. 2
144	135, 143	eqeltrrd 2530	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1444

wcel 1887

wral 2737

wrex 2738

crab 2741

cin 3403

wss 3404

cpw 3951

cop 3974

cuni 4198 class class class wbr 4402

cxp 4832

cdm 4834

crn 4835

cres 4836

cima 4837

ccom 4838

wfun 5576

wfn 5577

wf 5578

cfv 5582 (class class class)co 6290

cmpt2 6292

cr 9538

cc0 9539

c1 9540

caddc 9542

cmul 9544

cxr 9674

clt 9675

cle 9676

cmin 9860

cdiv 10269

cn 10609

c2 10659

cn0 10869

cz 10937

crp 11302

cioo 11635

cicc 11638

cfl 12026

cexp 12272

cabs 13297

ctg 15336

cxmt 18955

cbl 18957

cmopn 18960

cvol 22415

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-inf2 8146 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-fal 1450 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-int 4235 df-iun 4280 df-disj 4374 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-se 4794 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-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-omul 7187 df-er 7363 df-map 7474 df-pm 7475 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-acn 8376 df-cda 8598 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-2 10668 df-3 10669 df-4 10670 df-n0 10870 df-z 10938 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13552 df-rlim 13553 df-sum 13753 df-rest 15321 df-topgen 15342 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-top 19921 df-bases 19922 df-topon 19923 df-cmp 20402 df-ovol 22416 df-vol 22418

This theorem is referenced by: opnmbl 22560

W3C validator