voliunlem1 - Metamath Proof Explorer

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

Theorem voliunlem1 21723

Description: Lemma for voliun 21727. (Contributed by Mario Carneiro, 20-Mar-2014.)

**Hypotheses**
Ref	Expression
voliunlem.3
voliunlem.5	Disj
voliunlem1.6
voliunlem1.7
voliunlem1.8

**Assertion**
Ref	Expression
voliunlem1	$/\$ $\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem voliunlem1 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		voliunlem1.7	. . . . 5
2	1	adantr 465	. . . 4 $/\$
3		voliunlem1.8	. . . . 5
4	3	adantr 465	. . . 4 $/\$
5		difss 3631	. . . . 5 $\$
6		ovolsscl 21660	. . . . 5 $\$ $/\$ $/\$ $\$
7	5, 6	mp3an1 1311	. . . 4 $/\$ $\$
8	2, 4, 7	syl2anc 661	. . 3 $/\$ $\$
9		difss 3631	. . . . 5 $\$
10		ovolsscl 21660	. . . . 5 $\$ $/\$ $/\$ $\$
11	9, 10	mp3an1 1311	. . . 4 $/\$ $\$
12	2, 4, 11	syl2anc 661	. . 3 $/\$ $\$
13		inss1 3718	. . . . 5
14		ovolsscl 21660	. . . . 5 $/\$ $/\$
15	13, 14	mp3an1 1311	. . . 4 $/\$
16	2, 4, 15	syl2anc 661	. . 3 $/\$
17		elfznn 11714	. . . . . . . . 9
18		voliunlem.3	. . . . . . . . . . . 12
19		ffn 5731	. . . . . . . . . . . 12
20	18, 19	syl 16	. . . . . . . . . . 11
21		fnfvelrn 6018	. . . . . . . . . . 11 $/\$
22	20, 21	sylan 471	. . . . . . . . . 10 $/\$
23		elssuni 4275	. . . . . . . . . 10
24	22, 23	syl 16	. . . . . . . . 9 $/\$
25	17, 24	sylan2 474	. . . . . . . 8 $/\$
26	25	ralrimiva 2878	. . . . . . 7
27	26	adantr 465	. . . . . 6 $/\$
28		iunss 4366	. . . . . 6
29	27, 28	sylibr 212	. . . . 5 $/\$
30	29	sscond 3641	. . . 4 $/\$ $\$ $\$
31	9, 2	syl5ss 3515	. . . 4 $/\$ $\$
32		ovolss 21659	. . . 4 $\$ $\$ $/\$ $\$ $\$ $\$
33	30, 31, 32	syl2anc 661	. . 3 $/\$ $\$ $\$
34	8, 12, 16, 33	leadd2dd 10167	. 2 $/\$ $\$ $\$
35		oveq2 6292	. . . . . . . . . . 11
36	35	iuneq1d 4350	. . . . . . . . . 10
37	36	eleq1d 2536	. . . . . . . . 9
38	36	ineq2d 3700	. . . . . . . . . . 11
39	38	fveq2d 5870	. . . . . . . . . 10
40		fveq2 5866	. . . . . . . . . 10
41	39, 40	eqeq12d 2489	. . . . . . . . 9
42	37, 41	anbi12d 710	. . . . . . . 8 $/\$ $/\$
43	42	imbi2d 316	. . . . . . 7 $/\$ $/\$
44		oveq2 6292	. . . . . . . . . . 11
45	44	iuneq1d 4350	. . . . . . . . . 10
46	45	eleq1d 2536	. . . . . . . . 9
47	45	ineq2d 3700	. . . . . . . . . . 11
48	47	fveq2d 5870	. . . . . . . . . 10
49		fveq2 5866	. . . . . . . . . 10
50	48, 49	eqeq12d 2489	. . . . . . . . 9
51	46, 50	anbi12d 710	. . . . . . . 8 $/\$ $/\$
52	51	imbi2d 316	. . . . . . 7 $/\$ $/\$
53		oveq2 6292	. . . . . . . . . . 11
54	53	iuneq1d 4350	. . . . . . . . . 10
55	54	eleq1d 2536	. . . . . . . . 9
56	54	ineq2d 3700	. . . . . . . . . . 11
57	56	fveq2d 5870	. . . . . . . . . 10
58		fveq2 5866	. . . . . . . . . 10
59	57, 58	eqeq12d 2489	. . . . . . . . 9
60	55, 59	anbi12d 710	. . . . . . . 8 $/\$ $/\$
61	60	imbi2d 316	. . . . . . 7 $/\$ $/\$
62		1z 10894	. . . . . . . . . . 11
63		fzsn 11725	. . . . . . . . . . 11
64		iuneq1 4339	. . . . . . . . . . 11
65	62, 63, 64	mp2b 10	. . . . . . . . . 10
66		1ex 9591	. . . . . . . . . . 11
67		fveq2 5866	. . . . . . . . . . 11
68	66, 67	iunxsn 4405	. . . . . . . . . 10
69	65, 68	eqtri 2496	. . . . . . . . 9
70		1nn 10547	. . . . . . . . . 10
71		ffvelrn 6019	. . . . . . . . . 10 $/\$
72	18, 70, 71	sylancl 662	. . . . . . . . 9
73	69, 72	syl5eqel 2559	. . . . . . . 8
74	67	ineq2d 3700	. . . . . . . . . . . 12
75	74	fveq2d 5870	. . . . . . . . . . 11
76		voliunlem1.6	. . . . . . . . . . 11
77		fvex 5876	. . . . . . . . . . 11
78	75, 76, 77	fvmpt 5950	. . . . . . . . . 10
79	70, 78	ax-mp 5	. . . . . . . . 9
80		seq1 12088	. . . . . . . . . 10
81	62, 80	ax-mp 5	. . . . . . . . 9
82	69	ineq2i 3697	. . . . . . . . . 10
83	82	fveq2i 5869	. . . . . . . . 9
84	79, 81, 83	3eqtr4ri 2507	. . . . . . . 8
85	73, 84	jctir 538	. . . . . . 7 $/\$
86		peano2nn 10548	. . . . . . . . . . . . 13
87		ffvelrn 6019	. . . . . . . . . . . . 13 $/\$
88	18, 86, 87	syl2an 477	. . . . . . . . . . . 12 $/\$
89		unmbl 21711	. . . . . . . . . . . . 13 $/\$
90	89	ex 434	. . . . . . . . . . . 12
91	88, 90	syl5com 30	. . . . . . . . . . 11 $/\$
92		simpr 461	. . . . . . . . . . . . . . 15 $/\$
93		nnuz 11117	. . . . . . . . . . . . . . 15
94	92, 93	syl6eleq 2565	. . . . . . . . . . . . . 14 $/\$
95		fzsuc 11727	. . . . . . . . . . . . . 14
96		iuneq1 4339	. . . . . . . . . . . . . 14
97	94, 95, 96	3syl 20	. . . . . . . . . . . . 13 $/\$
98		iunxun 4407	. . . . . . . . . . . . . 14
99		ovex 6309	. . . . . . . . . . . . . . . 16
100		fveq2 5866	. . . . . . . . . . . . . . . 16
101	99, 100	iunxsn 4405	. . . . . . . . . . . . . . 15
102	101	uneq2i 3655	. . . . . . . . . . . . . 14
103	98, 102	eqtri 2496	. . . . . . . . . . . . 13
104	97, 103	syl6eq 2524	. . . . . . . . . . . 12 $/\$
105	104	eleq1d 2536	. . . . . . . . . . 11 $/\$
106	91, 105	sylibrd 234	. . . . . . . . . 10 $/\$
107		oveq1 6291	. . . . . . . . . . 11
108		inss1 3718	. . . . . . . . . . . . . . 15
109	108, 2	syl5ss 3515	. . . . . . . . . . . . . 14 $/\$
110		ovolsscl 21660	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	108, 110	mp3an1 1311	. . . . . . . . . . . . . . 15 $/\$
112	2, 4, 111	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
113		mblsplit 21706	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
114	88, 109, 112, 113	syl3anc 1228	. . . . . . . . . . . . 13 $/\$ $\$
115		in32 3710	. . . . . . . . . . . . . . . 16
116		inss2 3719	. . . . . . . . . . . . . . . . . 18
117	86	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
118	117, 93	syl6eleq 2565	. . . . . . . . . . . . . . . . . . 19 $/\$
119		eluzfz2 11694	. . . . . . . . . . . . . . . . . . 19
120	100	ssiun2s 4369	. . . . . . . . . . . . . . . . . . 19
121	118, 119, 120	3syl 20	. . . . . . . . . . . . . . . . . 18 $/\$
122	116, 121	syl5ss 3515	. . . . . . . . . . . . . . . . 17 $/\$
123		df-ss 3490	. . . . . . . . . . . . . . . . 17
124	122, 123	sylib 196	. . . . . . . . . . . . . . . 16 $/\$
125	115, 124	syl5eq 2520	. . . . . . . . . . . . . . 15 $/\$
126	125	fveq2d 5870	. . . . . . . . . . . . . 14 $/\$
127		indif2 3741	. . . . . . . . . . . . . . . 16 $\$ $\$
128		uncom 3648	. . . . . . . . . . . . . . . . . . 19
129	104, 128	syl6req 2525	. . . . . . . . . . . . . . . . . 18 $/\$
130		voliunlem.5	. . . . . . . . . . . . . . . . . . . . . . 23 Disj
131	130	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Disj
132	117	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
133	17	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
134	133	nnred 10551	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
135		elfzle2 11690	. . . . . . . . . . . . . . . . . . . . . . . . 25
136	135	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
137	92	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
138		nnleltp1 10917	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
139	133, 137, 138	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
140	136, 139	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
141	134, 140	gtned 9719	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
142		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . 23
143		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . 23
144	142, 143	disji2 4434	. . . . . . . . . . . . . . . . . . . . . 22 Disj $/\$ $/\$ $/\$
145	131, 132, 133, 141, 144	syl121anc 1233	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
146	145	iuneq2dv 4347	. . . . . . . . . . . . . . . . . . . 20 $/\$
147		iunin2 4389	. . . . . . . . . . . . . . . . . . . 20
148		iun0 4381	. . . . . . . . . . . . . . . . . . . 20
149	146, 147, 148	3eqtr3g 2531	. . . . . . . . . . . . . . . . . . 19 $/\$
150		uneqdifeq 3915	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
151	121, 149, 150	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
152	129, 151	mpbid 210	. . . . . . . . . . . . . . . . 17 $/\$ $\$
153	152	ineq2d 3700	. . . . . . . . . . . . . . . 16 $/\$ $\$
154	127, 153	syl5eqr 2522	. . . . . . . . . . . . . . 15 $/\$ $\$
155	154	fveq2d 5870	. . . . . . . . . . . . . 14 $/\$ $\$
156	126, 155	oveq12d 6302	. . . . . . . . . . . . 13 $/\$ $\$
157		inss1 3718	. . . . . . . . . . . . . . . . 17
158		ovolsscl 21660	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159	157, 158	mp3an1 1311	. . . . . . . . . . . . . . . 16 $/\$
160	2, 4, 159	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$
161	160	recnd 9622	. . . . . . . . . . . . . 14 $/\$
162	16	recnd 9622	. . . . . . . . . . . . . 14 $/\$
163	161, 162	addcomd 9781	. . . . . . . . . . . . 13 $/\$
164	114, 156, 163	3eqtrd 2512	. . . . . . . . . . . 12 $/\$
165		seqp1 12090	. . . . . . . . . . . . . 14
166	94, 165	syl 16	. . . . . . . . . . . . 13 $/\$
167	100	ineq2d 3700	. . . . . . . . . . . . . . . . 17
168	167	fveq2d 5870	. . . . . . . . . . . . . . . 16
169		fvex 5876	. . . . . . . . . . . . . . . 16
170	168, 76, 169	fvmpt 5950	. . . . . . . . . . . . . . 15
171	117, 170	syl 16	. . . . . . . . . . . . . 14 $/\$
172	171	oveq2d 6300	. . . . . . . . . . . . 13 $/\$
173	166, 172	eqtrd 2508	. . . . . . . . . . . 12 $/\$
174	164, 173	eqeq12d 2489	. . . . . . . . . . 11 $/\$
175	107, 174	syl5ibr 221	. . . . . . . . . 10 $/\$
176	106, 175	anim12d 563	. . . . . . . . 9 $/\$ $/\$ $/\$
177	176	expcom 435	. . . . . . . 8 $/\$ $/\$
178	177	a2d 26	. . . . . . 7 $/\$ $/\$
179	43, 52, 61, 52, 85, 178	nnind 10554	. . . . . 6 $/\$
180	179	impcom 430	. . . . 5 $/\$ $/\$
181	180	simprd 463	. . . 4 $/\$
182	181	eqcomd 2475	. . 3 $/\$
183	182	oveq1d 6299	. 2 $/\$ $\$ $\$
184	180	simpld 459	. . 3 $/\$
185		mblsplit 21706	. . 3 $/\$ $/\$ $\$
186	184, 2, 4, 185	syl3anc 1228	. 2 $/\$ $\$
187	34, 183, 186	3brtr4d 4477	1 $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wne 2662

wral 2814 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

csn 4027

cuni 4245

ciun 4325 Disj wdisj 4417 class class class wbr 4447

cmpt 4505

cdm 4999

crn 5000

wfn 5583

wf 5584

cfv 5588 (class class class)co 6284

cr 9491

c1 9493

caddc 9495

clt 9628

cle 9629

cn 10536

cz 10864

cuz 11082

cfz 11672

cseq 12075

covol 21637

cvol 21638

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-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 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-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-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 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-er 7311 df-map 7422 df-en 7517 df-dom 7518 df-sdom 7519 df-sup 7901 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-n0 10796 df-z 10865 df-uz 11083 df-q 11183 df-rp 11221 df-ioo 11533 df-ico 11535 df-icc 11536 df-fz 11673 df-fl 11897 df-seq 12076 df-exp 12135 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-ovol 21639 df-vol 21640

This theorem is referenced by: voliunlem2 21724 voliunlem3 21725

W3C validator