opnmbllem0 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > opnmbllem0		Structured version Unicode version

Theorem opnmbllem0 30290

Description: Lemma for ismblfin 30295; could also be used to shorten proof of opnmbllem 22176. (Contributed by Brendan Leahy, 13-Jul-2018.)

**Assertion**
Ref	Expression
opnmbllem0

Distinct variable group:

Proof of Theorem opnmbllem0 Dummy variables

are mutually distinct and distinct from all other variables.

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

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-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 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-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-iun 4317 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-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-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-1st 6773 df-2nd 6774 df-recs 7034 df-rdg 7068 df-er 7303 df-map 7414 df-en 7510 df-dom 7511 df-sdom 7512 df-sup 7893 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-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-icc 11539 df-fl 11910 df-seq 12090 df-exp 12149 df-cj 13014 df-re 13015 df-im 13016 df-sqrt 13150 df-abs 13151 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

This theorem is referenced by: mblfinlem1 30291 mblfinlem2 30292

W3C validator