mblfinlem3 - Mathbox for Brendan Leahy

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

Theorem mblfinlem3 33448

Description: The difference between two sets measurable by the criterion in ismblfin 33450 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)

**Assertion**
Ref	Expression
mblfinlem3	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$

Distinct variable groups:

Proof of Theorem mblfinlem3 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltso 10118	. . 3
2	1	a1i 11	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
3		difss 3737	. . . 4 $\$
4		ovolsscl 23254	. . . 4 $\$ $/\$ $/\$ $\$
5	3, 4	mp3an1 1411	. . 3 $/\$ $\$
6	5	3ad2ant1 1082	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
7		vex 3203	. . . . . 6
8		eqeq1 2626	. . . . . . . 8
9	8	anbi2d 740	. . . . . . 7 $\$ $/\$ $\$ $/\$
10	9	rexbidv 3052	. . . . . 6 $\$ $/\$ $\$ $/\$
11	7, 10	elab 3350	. . . . 5 $\$ $/\$ $\$ $/\$
12		simprl 794	. . . . . . . . 9 $/\$ $\$ $/\$ $\$
13		ssdifss 3741	. . . . . . . . 9 $\$
14		ovolss 23253	. . . . . . . . 9 $\$ $/\$ $\$ $\$
15	12, 13, 14	syl2anr 495	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $\$
16		uniretop 22566	. . . . . . . . . . . . 13
17	16	cldss 20833	. . . . . . . . . . . 12
18		ovolcl 23246	. . . . . . . . . . . 12
19	17, 18	syl 17	. . . . . . . . . . 11
20		ovolcl 23246	. . . . . . . . . . . 12 $\$ $\$
21	13, 20	syl 17	. . . . . . . . . . 11 $\$
22		xrlenlt 10103	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$
23	19, 21, 22	syl2anr 495	. . . . . . . . . 10 $/\$ $\$ $\$
24	23	adantrr 753	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $\$ $\$
25		id 22	. . . . . . . . . . . . . 14
26		dfss4 3858	. . . . . . . . . . . . . . . . 17 $\$ $\$
27	17, 26	sylib 208	. . . . . . . . . . . . . . . 16 $\$ $\$
28		rembl 23308	. . . . . . . . . . . . . . . . 17
29	16	cldopn 20835	. . . . . . . . . . . . . . . . . 18 $\$
30		opnmbl 23370	. . . . . . . . . . . . . . . . . 18 $\$ $\$
31	29, 30	syl 17	. . . . . . . . . . . . . . . . 17 $\$
32		difmbl 23311	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
33	28, 31, 32	sylancr 695	. . . . . . . . . . . . . . . 16 $\$ $\$
34	27, 33	eqeltrrd 2702	. . . . . . . . . . . . . . 15
35		mblvol 23298	. . . . . . . . . . . . . . 15
36	34, 35	syl 17	. . . . . . . . . . . . . 14
37	25, 36	sylan9eqr 2678	. . . . . . . . . . . . 13 $/\$
38	37	breq2d 4665	. . . . . . . . . . . 12 $/\$ $\$ $\$
39	38	notbid 308	. . . . . . . . . . 11 $/\$ $\$ $\$
40	39	adantrl 752	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$
41	40	adantl 482	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $\$ $\$
42	24, 41	bitr4d 271	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $\$ $\$
43	15, 42	mpbid 222	. . . . . . 7 $/\$ $/\$ $\$ $/\$ $\$
44	43	rexlimdvaa 3032	. . . . . 6 $\$ $/\$ $\$
45	44	imp 445	. . . . 5 $/\$ $\$ $/\$ $\$
46	11, 45	sylan2b 492	. . . 4 $/\$ $\$ $/\$ $\$
47	46	adantlr 751	. . 3 $/\$ $/\$ $\$ $/\$ $\$
48	47	3ad2antl1 1223	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
49		simplr 792	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
50		resubcl 10345	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$
51	50	adantrr 753	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$
52		posdif 10521	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$ $\$
53	52	ancoms 469	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $\$ $\$
54	53	biimpd 219	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$ $\$
55	54	impr 649	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$
56	51, 55	elrpd 11869	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$
57		3nn 11186	. . . . . . . . . . . . . . . . . 18
58		nnrp 11842	. . . . . . . . . . . . . . . . . 18
59	57, 58	ax-mp 5	. . . . . . . . . . . . . . . . 17
60		rpdivcl 11856	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$
61	56, 59, 60	sylancl 694	. . . . . . . . . . . . . . . 16 $\$ $/\$ $/\$ $\$ $\$
62	5, 61	sylan 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $\$
63	49, 62	ltsubrpd 11904	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
64	63	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
65		simpr 477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
66	64, 65	breqtrd 4679	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
67		reex 10027	. . . . . . . . . . . . . . . . . 18
68	67	ssex 4802	. . . . . . . . . . . . . . . . 17
69	68	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
70		sseq1 3626	. . . . . . . . . . . . . . . . . . 19
71		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
72	71	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19
73	70, 72	anbi12d 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74		sseq2 3627	. . . . . . . . . . . . . . . . . . . . . . 23
75	74	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76	75	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
77	76	abbidv 2741	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
78	77	sseq1d 3632	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
79	77	neeq1d 2853	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
80	77	raleqdv 3144	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
81	80	rexbidv 3052	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
82	78, 79, 81	3anbi123d 1399	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	73, 82	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84		simpr 477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
85	84, 36	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
86	85	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
87		simprl 794	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
88		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
89	88	3expb 1266	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
90	89	ancoms 469	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
91	87, 90	sylan2 491	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
92	86, 91	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
93	92	rexlimdvaa 3032	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
94	93	abssdv 3676	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
95		retop 22565	. . . . . . . . . . . . . . . . . . . . . 22
96		0cld 20842	. . . . . . . . . . . . . . . . . . . . . 22
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
98		0ss 3972	. . . . . . . . . . . . . . . . . . . . . 22
99		0mbl 23307	. . . . . . . . . . . . . . . . . . . . . . . 24
100		mblvol 23298	. . . . . . . . . . . . . . . . . . . . . . . 24
101	99, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
102		ovol0 23261	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . . 22
104	98, 103	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . 21 $/\$
105		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . 23
106		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
107	106	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . 23
108	105, 107	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
109	108	rspcev 3309	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
110	97, 104, 109	mp2an 708	. . . . . . . . . . . . . . . . . . . 20 $/\$
111		c0ex 10034	. . . . . . . . . . . . . . . . . . . . 21
112		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
114	113	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
115	111, 114	spcev 3300	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
116	110, 115	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $/\$
117		abn0 3954	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118	117	biimpri 218	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119	116, 118	mp1i 13	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
120		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121	120, 36	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
122	121	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
123		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
124		ovolss 23253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
125	124	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
126	123, 125	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
127	122, 126	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
128	127	rexlimdvaa 3032	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
129	128	alrimiv 1855	. . . . . . . . . . . . . . . . . . . . 21 $/\$
130		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . 24
131	130	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
132	131	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
133	132	ralab 3367	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
134	129, 133	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 $/\$
135		breq2 4657	. . . . . . . . . . . . . . . . . . . . . 22
136	135	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
137	136	rspcev 3309	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
138	134, 137	sylan2 491	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
139	138	ancoms 469	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
140	94, 119, 139	3jca 1242	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141	83, 140	vtoclg 3266	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
142	69, 141	mpcom 38	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
143	142	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
144	62	rpred 11872	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $\$
145	49, 144	resubcld 10458	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
146		suprlub 10987	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $/\$ $\$
147	143, 145, 146	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $/\$ $\$
148	147	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
149	66, 148	mpbid 222	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
150		eqeq1 2626	. . . . . . . . . . . . . . 15
151	150	anbi2d 740	. . . . . . . . . . . . . 14 $/\$ $/\$
152	151	rexbidv 3052	. . . . . . . . . . . . 13 $/\$ $/\$
153	152	rexab 3369	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $\$
154		breq2 4657	. . . . . . . . . . . . . . . . 17 $\$ $\$
155	154	ad2antll 765	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
156		sseq1 3626	. . . . . . . . . . . . . . . . . . . 20
157		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
158	157	breq2d 4665	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
159	156, 158	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
160	159	rspcev 3309	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$ $\$
161	160	expr 643	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$
162	161	adantrr 753	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $\$
163	155, 162	sylbid 230	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $\$
164	163	rexlimiva 3028	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$
165	164	imp 445	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
166	165	exlimiv 1858	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
167	153, 166	sylbi 207	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
168	149, 167	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
169	168	ex 450	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
170	169	adantlr 751	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
171		simplrr 801	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
172	62	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
173	171, 172	ltsubrpd 11904	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
174	173	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
175		simpr 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
176	174, 175	breqtrd 4679	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
177	67	ssex 4802	. . . . . . . . . . . . . . . 16
178	177	adantr 481	. . . . . . . . . . . . . . 15 $/\$
179		sseq1 3626	. . . . . . . . . . . . . . . . . 18
180		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
181	180	eleq1d 2686	. . . . . . . . . . . . . . . . . 18
182	179, 181	anbi12d 747	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
183		sseq2 3627	. . . . . . . . . . . . . . . . . . . . . 22
184	183	anbi1d 741	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
185	184	rexbidv 3052	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
186	185	abbidv 2741	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
187	186	sseq1d 3632	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
188	186	neeq1d 2853	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
189	186	raleqdv 3144	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
190	189	rexbidv 3052	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
191	187, 188, 190	3anbi123d 1399	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
192	182, 191	imbi12d 334	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
193	192, 140	vtoclg 3266	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
194	178, 193	mpcom 38	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
195	194	ad2antlr 763	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
196	144	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
197	171, 196	resubcld 10458	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
198		suprlub 10987	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $/\$ $\$
199	195, 197, 198	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $/\$ $\$
200	199	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
201	176, 200	mpbid 222	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
202	150	anbi2d 740	. . . . . . . . . . . . 13 $/\$ $/\$
203	202	rexbidv 3052	. . . . . . . . . . . 12 $/\$ $/\$
204	203	rexab 3369	. . . . . . . . . . 11 $/\$ $\$ $/\$ $/\$ $\$
205		breq2 4657	. . . . . . . . . . . . . . . 16 $\$ $\$
206	205	ad2antll 765	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
207		sseq1 3626	. . . . . . . . . . . . . . . . . . 19
208		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
209	208	breq2d 4665	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
210	207, 209	anbi12d 747	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$
211	210	rspcev 3309	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $\$
212	211	expr 643	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$
213	212	adantrr 753	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $\$
214	206, 213	sylbid 230	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$
215	214	rexlimiva 3028	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$
216	215	imp 445	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
217	216	exlimiv 1858	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
218	204, 217	sylbi 207	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
219	201, 218	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
220	219	ex 450	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
221	170, 220	anim12d 586	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
222		reeanv 3107	. . . . . . 7 $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
223	221, 222	syl6ibr 242	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
224		eqid 2622	. . . . . . . . . . . . . 14
225	224	ovolgelb 23248	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
226	225	3expa 1265	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
227	62, 226	sylan2 491	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
228	227	ancoms 469	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
229	228	an32s 846	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
230		elmapi 7879	. . . . . . . . . . . 12
231		ssid 3624	. . . . . . . . . . . . . . 15
232	224	ovollb 23247	. . . . . . . . . . . . . . 15 $/\$
233	231, 232	mpan2 707	. . . . . . . . . . . . . 14
234	233	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
235		eqid 2622	. . . . . . . . . . . . . . . 16
236	235, 224	ovolsf 23241	. . . . . . . . . . . . . . 15
237		frn 6053	. . . . . . . . . . . . . . . 16
238		icossxr 12258	. . . . . . . . . . . . . . . 16
239	237, 238	syl6ss 3615	. . . . . . . . . . . . . . 15
240		supxrcl 12145	. . . . . . . . . . . . . . 15
241	236, 239, 240	3syl 18	. . . . . . . . . . . . . 14
242		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$
243		readdcl 10019	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$
244	242, 144, 243	syl2anr 495	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
245	244	rexrd 10089	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
246	245	an32s 846	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
247		rncoss 5386	. . . . . . . . . . . . . . . . . 18
248	247	unissi 4461	. . . . . . . . . . . . . . . . 17
249		unirnioo 12273	. . . . . . . . . . . . . . . . 17
250	248, 249	sseqtr4i 3638	. . . . . . . . . . . . . . . 16
251		ovolcl 23246	. . . . . . . . . . . . . . . 16
252	250, 251	ax-mp 5	. . . . . . . . . . . . . . 15
253		xrletr 11989	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $\$ $\$
254	252, 253	mp3an1 1411	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
255	241, 246, 254	syl2anr 495	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
256	234, 255	mpand 711	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
257	230, 256	sylan2 491	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
258	257	anim2d 589	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$
259	258	reximdva 3017	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
260	229, 259	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
261		rexex 3002	. . . . . . . 8 $/\$ $\$ $/\$ $\$
262	260, 261	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
263	16	cldss 20833	. . . . . . . . . . . . . . . . 17
264		indif2 3870	. . . . . . . . . . . . . . . . . 18 $\$ $\$
265		df-ss 3588	. . . . . . . . . . . . . . . . . . . 20
266	265	biimpi 206	. . . . . . . . . . . . . . . . . . 19
267	266	difeq1d 3727	. . . . . . . . . . . . . . . . . 18 $\$ $\$
268	264, 267	syl5eq 2668	. . . . . . . . . . . . . . . . 17 $\$ $\$
269	263, 268	syl 17	. . . . . . . . . . . . . . . 16 $\$ $\$
270		retopbas 22564	. . . . . . . . . . . . . . . . . . . . 21
271		bastg 20770	. . . . . . . . . . . . . . . . . . . . 21
272	270, 271	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
273	247, 272	sstri 3612	. . . . . . . . . . . . . . . . . . 19
274		uniopn 20702	. . . . . . . . . . . . . . . . . . 19 $/\$
275	95, 273, 274	mp2an 708	. . . . . . . . . . . . . . . . . 18
276	16	opncld 20837	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
277	95, 275, 276	mp2an 708	. . . . . . . . . . . . . . . . 17 $\$
278		incld 20847	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$
279	277, 278	mpan2 707	. . . . . . . . . . . . . . . 16 $\$
280	269, 279	eqeltrrd 2702	. . . . . . . . . . . . . . 15 $\$
281	280	adantr 481	. . . . . . . . . . . . . 14 $/\$ $\$
282	281	ad2antlr 763	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
283		simprll 802	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
284		simplll 798	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
285	283, 284	ssdif2d 3749	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
286		fveq2 6191	. . . . . . . . . . . . . . . . 17 $\$ $\$
287	286	eqcoms 2630	. . . . . . . . . . . . . . . 16 $\$ $\$
288	287	biantrud 528	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $/\$ $\$
289		sseq1 3626	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
290	288, 289	bitr3d 270	. . . . . . . . . . . . . 14 $\$ $\$ $/\$ $\$ $\$ $\$
291	290	rspcev 3309	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$
292	282, 285, 291	syl2anc 693	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
293	292	adantlll 754	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
294		difss 3737	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
295	294, 3	sstri 3612	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
296		ovolsscl 23254	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $/\$ $/\$ $\$ $\$ $\$
297	295, 296	mp3an1 1411	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
298	297	ad5antr 770	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
299	5	ad5antr 770	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
300		simpl 473	. . . . . . . . . . . . . 14 $/\$ $\$
301	300	ad4antlr 769	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
302		difdif2 3884	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$ $\$
303	302	fveq2i 6194	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ $\$ $\$
304		difss 3737	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
305	304, 3	sstri 3612	. . . . . . . . . . . . . . . . . 18 $\$ $\$
306		inss1 3833	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
307	306, 3	sstri 3612	. . . . . . . . . . . . . . . . . 18 $\$
308	305, 307	unssi 3788	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
309		ovolsscl 23254	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $/\$ $/\$ $\$ $\$ $\$
310	308, 309	mp3an1 1411	. . . . . . . . . . . . . . . 16 $/\$ $\$ $\$ $\$
311	310	ad5antr 770	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
312		difss 3737	. . . . . . . . . . . . . . . . . 18 $\$
313		ovolsscl 23254	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$
314	312, 313	mp3an1 1411	. . . . . . . . . . . . . . . . 17 $/\$ $\$
315	314	ad5antr 770	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
316	171, 196	readdcld 10069	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
317	316, 252	jctil 560	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
318		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$
319		ovolge0 23249	. . . . . . . . . . . . . . . . . . . . 21
320	250, 319	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
321	318, 320	jctil 560	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
322		xrrege0 12005	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $/\$ $\$
323	317, 321, 322	syl2an 494	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
324		difss 3737	. . . . . . . . . . . . . . . . . . 19 $\$
325		ovolsscl 23254	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $/\$ $\$
326	324, 250, 325	mp3an12 1414	. . . . . . . . . . . . . . . . . 18 $\$
327	323, 326	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
328	327	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
329	315, 328	readdcld 10069	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
330	5, 50	sylan 488	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
331	330	adantrr 753	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $\$
332	331	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
333	332	ad3antrrr 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
334		ssdifss 3741	. . . . . . . . . . . . . . . . . . . . 21 $\$
335	324, 250	sstri 3612	. . . . . . . . . . . . . . . . . . . . 21 $\$
336		unss 3787	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$ $\$ $\$ $\$
337	334, 335, 336	sylanblc 696	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
338		ovolcl 23246	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
339	337, 338	syl 17	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
340	339	ad4antr 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
341	314	ad3antrrr 766	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
342	341, 327	readdcld 10069	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
343		ovolge0 23249	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
344	337, 343	syl 17	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
345	344	ad4antr 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
346	334	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
347	346, 314	jca 554	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $\$
348	347	ad3antrrr 766	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
349	327, 335	jctil 560	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
350		ovolun 23267	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
351	348, 349, 350	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
352		xrrege0 12005	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
353	340, 342, 345, 351, 352	syl22anc 1327	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
354	353	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
355		ssdif 3745	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$
356	3, 355	ax-mp 5	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
357		incom 3805	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
358		indif2 3870	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
359	357, 358	eqtri 2644	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
360		inss1 3833	. . . . . . . . . . . . . . . . . . . . 21
361	360	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
362		simprrl 804	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
363	361, 362	ssdif2d 3749	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
364	359, 363	syl5eqss 3649	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
365		unss12 3785	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
366	356, 364, 365	sylancr 695	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
367	337	ad6antr 772	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
368		ovolss 23253	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
369	366, 367, 368	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
370	334	ad6antr 772	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
371	328, 335	jctil 560	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
372	370, 315, 371, 350	syl21anc 1325	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
373	311, 354, 329, 369, 372	letrd 10194	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
374	196	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
375	196, 196	readdcld 10069	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
376	375	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
377		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25
378	377, 34	vtoclga 3272	. . . . . . . . . . . . . . . . . . . . . . . 24
379		mblvol 23298	. . . . . . . . . . . . . . . . . . . . . . . 24
380	378, 379	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
381	380	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
382		sseqin2 3817	. . . . . . . . . . . . . . . . . . . . . . . . . 26
383	382	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . 25
384	383	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24
385	384	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23
386	385	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$ $\$
387	381, 386	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
388	387	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
389	388	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
390	378	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
391		simplll 798	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
392		mblsplit 23300	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
393	392	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
394	393	3expb 1266	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
395	390, 391, 394	syl2anr 495	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
396	395	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
397		simp-6r 811	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
398	397	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
399		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . 24
400		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
401	399, 400	mp3an1 1411	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
402	401	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
403	402	ad5antr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
404	314	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$
405	404	ad5antr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
406	398, 403, 405	subaddd 10410	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
407	396, 406	mpbird 247	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
408	389, 407	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
409	381	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
410		simpll 790	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$ $\$
411		simp-4l 806	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
412		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
413	412	3expb 1266	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
414	410, 411, 413	syl2anr 495	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
415	409, 414	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
416		simprlr 803	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
417	397, 374, 415, 416	ltsub23d 10632	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
418	408, 417	eqbrtrrd 4677	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
419	323	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
420	419	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
421	242	ad5antlr 771	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
422	421	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
423		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
424	423, 34	vtoclga 3272	. . . . . . . . . . . . . . . . . . . . . . . . 25
425		mblvol 23298	. . . . . . . . . . . . . . . . . . . . . . . . 25
426	424, 425	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
427	426	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
428	427	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
429		simprl 794	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$ $\$
430		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
431		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
432	431	3expb 1266	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
433	429, 430, 432	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
434	428, 433	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
435	434	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
436	420, 422, 435	npncand 10416	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
437		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$
438	429, 437	sylan9ssr 3617	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
439		sseqin2 3817	. . . . . . . . . . . . . . . . . . . . . . 23
440	438, 439	sylib 208	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
441	440	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
442	428, 441	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
443	442	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
444	424	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
445	323, 250	jctil 560	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
446		mblsplit 23300	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
447	446	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
448	447	3expb 1266	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
449	444, 445, 448	syl2anr 495	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
450	449	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
451		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . . 25
452		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
453	451, 250, 452	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . 24
454	323, 453	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
455	454	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
456	327	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
457	419, 455, 456	subaddd 10410	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
458	457	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
459	450, 458	mpbird 247	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
460	436, 443, 459	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
461	242	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
462	323, 461	resubcld 10458	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
463	462	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
464	421, 434	resubcld 10458	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
465		simprr 796	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
466	196	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
467	323, 461, 466	lesubadd2d 10626	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
468	465, 467	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
469	468	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
470		simprrr 805	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
471	421, 374, 434, 470	ltsub23d 10632	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
472	463, 464, 374, 374, 469, 471	leltaddd 10649	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
473	460, 472	eqbrtrrd 4677	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
474	315, 328, 374, 376, 418, 473	lt2addd 10650	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
475		df-3 11080	. . . . . . . . . . . . . . . . . . . . . 22
476		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . 23
477		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . 23
478	476, 477	addcomi 10227	. . . . . . . . . . . . . . . . . . . . . 22
479	475, 478	eqtri 2644	. . . . . . . . . . . . . . . . . . . . 21
480	479	oveq1i 6660	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
481	62	rpcnd 11874	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
482		adddir 10031	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$ $\$ $\$
483	477, 476, 482	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$ $\$
484	481, 483	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
485	481	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$ $\$
486	481	2timesd 11275	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
487	485, 486	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
488	484, 487	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
489	480, 488	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
490	331	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$ $\$
491		3cn 11095	. . . . . . . . . . . . . . . . . . . . 21
492		3ne0 11115	. . . . . . . . . . . . . . . . . . . . 21
493		divcan2 10693	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$ $/\$ $\$ $\$
494	491, 492, 493	mp3an23 1416	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
495	490, 494	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$ $\$ $\$
496	489, 495	eqtr3d 2658	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
497	496	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
498	497	ad3antrrr 766	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
499	474, 498	breqtrd 4679	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
500	311, 329, 333, 373, 499	lelttrd 10195	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
501	303, 500	syl5eqbr 4688	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
502	298, 299, 301, 501	ltsub13d 10633	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
503	285	adantlll 754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
504		sseqin2 3817	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$
505	503, 504	sylib 208	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
506	505	fveq2d 6195	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
507		opnmbl 23370	. . . . . . . . . . . . . . . . . . 19
508	275, 507	ax-mp 5	. . . . . . . . . . . . . . . . . 18
509		difmbl 23311	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
510	378, 508, 509	sylancl 694	. . . . . . . . . . . . . . . . 17 $\$
511	510	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $\$
512	511	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
513	13	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $\$
514	513, 5	jca 554	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$
515	514	ad5antr 770	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
516		mblsplit 23300	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
517	516	3expb 1266	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
518	517	eqcomd 2628	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
519	512, 515, 518	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
520	299	recnd 10068	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
521	298	recnd 10068	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
522		inss1 3833	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
523	522, 3	sstri 3612	. . . . . . . . . . . . . . . . . 18 $\$ $\$
524		ovolsscl 23254	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $/\$ $/\$ $\$ $\$
525	523, 524	mp3an1 1411	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$
526	525	ad5antr 770	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
527	526	recnd 10068	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
528	520, 521, 527	subadd2d 10411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
529	519, 528	mpbird 247	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
530		mblvol 23298	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
531	509, 530	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $\$ $\$
532	378, 508, 531	sylancl 694	. . . . . . . . . . . . . . 15 $\$ $\$
533	532	adantr 481	. . . . . . . . . . . . . 14 $/\$ $\$ $\$
534	533	ad2antlr 763	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
535	506, 529, 534	3eqtr4rd 2667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
536	502, 535	breqtrrd 4681	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
537		fvex 6201	. . . . . . . . . . . 12 $\$
538		eqeq1 2626	. . . . . . . . . . . . . . 15 $\$ $\$
539	538	anbi2d 740	. . . . . . . . . . . . . 14 $\$ $\$ $/\$ $\$ $/\$ $\$
540	539	rexbidv 3052	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $/\$ $\$
541		breq2 4657	. . . . . . . . . . . . 13 $\$ $\$
542	540, 541	anbi12d 747	. . . . . . . . . . . 12 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
543	537, 542	spcev 3300	. . . . . . . . . . 11 $\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $/\$
544	293, 536, 543	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$ $/\$
545	150	anbi2d 740	. . . . . . . . . . . 12 $\$ $/\$ $\$ $/\$
546	545	rexbidv 3052	. . . . . . . . . . 11 $\$ $/\$ $\$ $/\$
547	546	rexab 3369	. . . . . . . . . 10 $\$ $/\$ $\$ $/\$ $/\$
548	544, 547	sylibr 224	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$
549	548	ex 450	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$
550	549	rexlimdvva 3038	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$
551	262, 550	exlimddv 1863	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $/\$
552	223, 551	syld 47	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
553	552	exp31 630	. . . 4 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
554	553	com34 91	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$
555	554	3imp1 1280	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$
556	2, 6, 48, 555	eqsupd 8363	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wal 1481

wceq 1483

wex 1704

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cuni 4436 class class class wbr 4653

wor 5034

cxp 5112

cdm 5114

crn 5115

ccom 5118

wf 5884

cfv 5888 (class class class)co 6650

cmap 7857

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

cxr 10073

clt 10074

cle 10075

cmin 10266

cdiv 10684

cn 11020

c2 11070

c3 11071

crp 11832

cioo 12175

cico 12177

cseq 12801

cabs 13974

ctg 16098

ctop 20698

ctb 20749

ccld 20820

covol 23231

cvol 23232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cld 20823 df-cmp 21190 df-ovol 23233 df-vol 23234

This theorem is referenced by: ismblfin 33450

W3C validator