itg2addnclem - Mathbox for Brendan Leahy

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

Theorem itg2addnclem 33461

Description: An alternate expression for the

integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.)

**Hypothesis**
Ref	Expression
itg2addnclem.1	$/\$

**Assertion**
Ref	Expression
itg2addnclem

Distinct variable group:

Allowed substitution hints:

(

)

Proof of Theorem itg2addnclem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 $/\$ $/\$
2	1	itg2val 23495	. 2 $/\$
3		itg2addnclem.1	. . . 4 $/\$
4	3	supeq1i 8353	. . 3 $/\$
5		xrltso 11974	. . . . 5
6	5	a1i 11	. . . 4
7		simprr 796	. . . . . . . 8 $/\$ $/\$
8		itg1cl 23452	. . . . . . . . . 10
9	8	rexrd 10089	. . . . . . . . 9
10	9	adantr 481	. . . . . . . 8 $/\$ $/\$
11	7, 10	eqeltrd 2701	. . . . . . 7 $/\$ $/\$
12	11	rexlimiva 3028	. . . . . 6 $/\$
13	12	abssi 3677	. . . . 5 $/\$
14		supxrcl 12145	. . . . 5 $/\$ $/\$
15	13, 14	mp1i 13	. . . 4 $/\$
16		fveq1 6190	. . . . . . . . . . . . . . . 16
17	16	eqeq1d 2624	. . . . . . . . . . . . . . 15
18	16	oveq1d 6665	. . . . . . . . . . . . . . 15
19	17, 18	ifbieq2d 4111	. . . . . . . . . . . . . 14
20	19	mpteq2dv 4745	. . . . . . . . . . . . 13
21	20	breq1d 4663	. . . . . . . . . . . 12
22	21	rexbidv 3052	. . . . . . . . . . 11
23		fveq2 6191	. . . . . . . . . . . 12
24	23	eqeq2d 2632	. . . . . . . . . . 11
25	22, 24	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$
26	25	cbvrexv 3172	. . . . . . . . 9 $/\$ $/\$
27		breq2 4657	. . . . . . . . . . . . . . . . 17
28		breq2 4657	. . . . . . . . . . . . . . . . 17
29		id 22	. . . . . . . . . . . . . . . . . . 19
30		0le0 11110	. . . . . . . . . . . . . . . . . . 19
31	29, 30	syl6eqbr 4692	. . . . . . . . . . . . . . . . . 18
32	31	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
33		rpge0 11845	. . . . . . . . . . . . . . . . . . . 20
34	33	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
35		i1ff 23443	. . . . . . . . . . . . . . . . . . . . . 22
36	35	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . 21 $/\$
37	36	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
38		rpre 11839	. . . . . . . . . . . . . . . . . . . . 21
39	38	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
40	37, 39	addge01d 10615	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
41	34, 40	mpbid 222	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
42	41	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
43	27, 28, 32, 42	ifbothda 4123	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44	43	adantlll 754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
45	35	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46	45	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
47	46	rexrd 10089	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
48		0re 10040	. . . . . . . . . . . . . . . . . 18
49	38	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
50	46, 49	readdcld 10069	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
51		ifcl 4130	. . . . . . . . . . . . . . . . . 18 $/\$
52	48, 50, 51	sylancr 695	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
53	52	rexrd 10089	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
54		iccssxr 12256	. . . . . . . . . . . . . . . . . . 19
55		fss 6056	. . . . . . . . . . . . . . . . . . 19 $/\$
56	54, 55	mpan2 707	. . . . . . . . . . . . . . . . . 18
57	56	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
58	57	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
59		xrletr 11989	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
60	47, 53, 58, 59	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	44, 60	mpand 711	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
62	61	ralimdva 2962	. . . . . . . . . . . . 13 $/\$ $/\$
63		reex 10027	. . . . . . . . . . . . . . 15
64	63	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
65		eqidd 2623	. . . . . . . . . . . . . 14 $/\$ $/\$
66		id 22	. . . . . . . . . . . . . . . 16
67	66	feqmptd 6249	. . . . . . . . . . . . . . 15
68	67	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$
69	64, 52, 58, 65, 68	ofrfval2 6915	. . . . . . . . . . . . 13 $/\$ $/\$
70	35	feqmptd 6249	. . . . . . . . . . . . . . 15
71	70	ad2antlr 763	. . . . . . . . . . . . . 14 $/\$ $/\$
72	64, 46, 58, 71, 68	ofrfval2 6915	. . . . . . . . . . . . 13 $/\$ $/\$
73	62, 69, 72	3imtr4d 283	. . . . . . . . . . . 12 $/\$ $/\$
74	73	rexlimdva 3031	. . . . . . . . . . 11 $/\$
75	74	anim1d 588	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	75	reximdva 3017	. . . . . . . . 9 $/\$ $/\$
77	26, 76	syl5bi 232	. . . . . . . 8 $/\$ $/\$
78	77	ss2abdv 3675	. . . . . . 7 $/\$ $/\$
79	78	sseld 3602	. . . . . 6 $/\$ $/\$
80		simp3r 1090	. . . . . . . . . . 11 $/\$ $/\$ $/\$
81	9	3ad2ant2 1083	. . . . . . . . . . 11 $/\$ $/\$ $/\$
82	80, 81	eqeltrd 2701	. . . . . . . . . 10 $/\$ $/\$ $/\$
83	82	rexlimdv3a 3033	. . . . . . . . 9 $/\$
84	83	abssdv 3676	. . . . . . . 8 $/\$
85		xrsupss 12139	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
86	84, 85	syl 17	. . . . . . 7 $/\$ $/\$ $/\$
87	6, 86	supub 8365	. . . . . 6 $/\$ $/\$
88	79, 87	syld 47	. . . . 5 $/\$ $/\$
89	88	imp 445	. . . 4 $/\$ $/\$ $/\$
90		supxrlub 12155	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
91	13, 90	mpan 706	. . . . . . 7 $/\$ $/\$
92	91	adantl 482	. . . . . 6 $/\$ $/\$ $/\$
93		simprrr 805	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
94	93	breq2d 4665	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
95		simplll 798	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
96		i1f0 23454	. . . . . . . . . . . . . . . . . . 19
97		2rp 11837	. . . . . . . . . . . . . . . . . . . . 21
98	97	ne0ii 3923	. . . . . . . . . . . . . . . . . . . 20
99		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
100		elxrge0 12281	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
101	99, 100	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
102	101	simprd 479	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
103	102	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . 22
104	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
105		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . . . 24
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
107		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . 23
108	104, 106, 99, 107, 67	ofrfval2 6915	. . . . . . . . . . . . . . . . . . . . . 22
109	103, 108	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21
110	109	ralrimivw 2967	. . . . . . . . . . . . . . . . . . . 20
111		r19.2z 4060	. . . . . . . . . . . . . . . . . . . 20 $/\$
112	98, 110, 111	sylancr 695	. . . . . . . . . . . . . . . . . . 19
113		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
114		itg10 23455	. . . . . . . . . . . . . . . . . . . . . . 23
115	113, 114	syl6req 2673	. . . . . . . . . . . . . . . . . . . . . 22
116	115	biantrud 528	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . 26
118	105	fvconst2 6469	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	117, 118	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
120		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . 25
121	119, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
122	121	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . 23
123	122	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . 22
124	123	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . 21
125	116, 124	bitr3d 270	. . . . . . . . . . . . . . . . . . . 20 $/\$
126	125	rspcev 3309	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
127	96, 112, 126	sylancr 695	. . . . . . . . . . . . . . . . . 18 $/\$
128		id 22	. . . . . . . . . . . . . . . . . . 19
129		mnflt 11957	. . . . . . . . . . . . . . . . . . . 20
130	48, 129	mp1i 13	. . . . . . . . . . . . . . . . . . 19
131	128, 130	eqbrtrd 4675	. . . . . . . . . . . . . . . . . 18
132		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . 22
133	132	anbi2d 740	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
134	133	rexbidv 3052	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
135		breq2 4657	. . . . . . . . . . . . . . . . . . . 20
136	134, 135	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
137	105, 136	spcev 3300	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
138	127, 131, 137	syl2an 494	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
139	95, 138	sylan 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140		simp-4r 807	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141	8	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
142	141	ad3antlr 767	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
143		simpllr 799	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
144		ngtmnft 11997	. . . . . . . . . . . . . . . . . . . . . 22
145	144	biimprd 238	. . . . . . . . . . . . . . . . . . . . 21
146	145	necon1ad 2811	. . . . . . . . . . . . . . . . . . . 20
147	146	imp 445	. . . . . . . . . . . . . . . . . . 19 $/\$
148	143, 147	sylan 488	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
150	9	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
151	149, 150	anim12i 590	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
152		xrltle 11982	. . . . . . . . . . . . . . . . . . . . 21 $/\$
153	152	imp 445	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
154	151, 153	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
155	154	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156		xrre 12000	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
157	140, 142, 148, 155, 156	syl22anc 1327	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	127	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
159		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
160		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
161		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$
162		cnvimass 5485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
163		fdm 6051	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
164	35, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
165	162, 164	syl5sseq 3653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
166	165	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$
167		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$
168	163	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169		ffun 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170		difpreima 6343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
172		cnvimarndm 5486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173	172	difeq1i 3724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
174	171, 173	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
175	168, 174	difeq12d 3729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
176		cnvimass 5485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177		dfss4 3858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
178	176, 177	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
179	175, 178	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
180	179	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
181		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
182		fniniseg 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
183		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
184	182, 183	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
185	181, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
186	180, 185	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
187	35, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
188	187	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $\$
189	188	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $\$ $\$
190	161, 166, 167, 189	itg10a 23477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
191	160, 190	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
192	159, 191	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
193	158, 192, 137	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
194		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
195		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
196	194, 195	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
198		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
199	198	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$
200		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
201	200, 105	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
202	201	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $\$ $\$
203	35	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
204	203	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
205		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
206	197, 199, 202, 204, 205	offval2 6914	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
207		ovif2 6738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$ $\$ $\$
208	172, 163	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
209	208	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\$ $\$
210	171, 209	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $\$ $\$
211	210	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $\$ $\$
212	35, 211	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $\$ $\$
213	212	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $/\$ $\$ $\$
214		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $\$ $/\$
215	214	biantrurd 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $\$ $/\$ $/\$
216		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $\$ $/\$
217	215, 216	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $/\$ $\$
218	213, 217	bitr4d 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$ $\$
219	218	con2bid 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$ $\$
220		fniniseg 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
221	35, 181, 220	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
222	221	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$ $/\$
223	219, 222	bitr3d 270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $/\$ $\$ $/\$
224		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
225		0m0e0 11130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
226	224, 225	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
227	226	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
228	223, 227	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $/\$ $\$
229	228	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $/\$ $/\$ $\$
230	229	ifeq2da 4117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
231	207, 230	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
232	231	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
233	206, 232	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
234		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
235	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $/\$ $\$
236		1ex 10035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
237	236, 105	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
238	237	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $/\$ $\$
239		fconstmpt 5163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
240	239	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$ $\$
241		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$ $\$
242	197, 235, 238, 240, 241	offval2 6914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
243		ovif2 6738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$ $\$
244		resubcl 10345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
245	8, 244	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
246	245	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$
247		2re 11090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
248		i1fima 23445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\$
249		mblvol 23298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\$ $\$ $\$
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $\$ $\$
251		neldifsn 4321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\$
252		i1fima2 23446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $\$ $\$
253	251, 252	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $\$
254	250, 253	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $\$
255		remulcl 10021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $\$ $\$
256	247, 254, 255	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $\$
257	256	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $\$
258		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $\$
259	254	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $\$ $\$
260	259	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $\$ $\$
261		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
262	261	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $\$
263		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $\$ $\$
264	258, 260, 262, 263	mulne0d 10679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $\$
265	246, 257, 264	redivcld 10853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $\$
266	265	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $\$
267	266	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$ $\$
268	266	mul01d 10235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$
269	267, 268	ifeq12d 4106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
270	243, 269	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
271	270	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
272	242, 271	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
273		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
274	273	i1f1 23457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $/\$ $\$ $\$
275	248, 253, 274	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
276	275	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$
277	276, 265	i1fmulc 23470	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$ $\$
278	272, 277	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$ $\$
279		i1fsub 23475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$ $\$ $\$
280	234, 278, 279	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$ $\$
281	233, 280	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $\$ $\$
282		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
283		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
284	283	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
285	282, 284	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
286		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
287		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
288	287, 105	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
289	285, 286, 288	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $\$ $\$
290	289	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$ $\$ $\$
291	290, 289	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
292		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
293		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $\$ $\$
294	293	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $\$ $\$
295	294, 293	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$ $\$ $\$ $\$
296		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
297	295, 296	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
298	292, 297	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
299		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
300		ianor 509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $/\$ $\$ $\$ $\/$ $\$
301	294	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
302		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$
303	301, 302	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
304	303	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $\$ $\$ $\$ $\$
305		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$ $\$
306		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
307		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
308		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
309	307, 308	ifboth 4124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$ $/\$ $\$ $\$ $\$ $\$
310	305, 306, 309	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $\$ $\$ $\$
311	304, 310	pm2.61d1 171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $\$ $\$ $\$
312	311, 310	jaoi 394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\/$ $\$ $\$ $\$ $\$ $\$
313	300, 312	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
314	299, 313	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
315	298, 314	pm2.61i 176	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
316	291, 315	syl6reqr 2675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
317	316	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
318	317	i1fpos 23473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $/\$ $\$ $\$
319	281, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
320	196, 319	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
321	196, 265	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
322	8	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
323	322, 195, 244	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
324	323	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
325	256	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
326	325	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
327		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
328		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
329	141	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
330	328, 329	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
331	327, 330	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
332	331	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
333	254	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
334	333	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
335		mblss 23299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
336		ovolge0 23249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
337	248, 335, 336	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
338		ltlen 10138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $\$ $\$ $\$ $/\$ $\$
339	48, 254, 338	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $/\$ $\$
340	339	biimprd 238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $/\$ $\$ $\$
341	337, 340	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
342	341	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $\$
343	342	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $\$ $\$
344	343	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
345		2pos 11112	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
346		mulgt0 10115	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $\$ $\$
347	247, 345, 346	mpanl12 718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $\$
348	334, 344, 347	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
349	324, 326, 332, 348	divgt0d 10959	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
350	321, 349	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
351		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
352	351	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
353		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
354	35, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
355	354	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
356		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
357		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
358	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
359		inidm 3822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
360		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
361		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
362	356, 357, 358, 358, 359, 360, 361	ofrfval 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
363	353, 355, 362	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
364	363	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
365		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
366	365	anim2i 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
367	366, 195	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
368		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
369		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
370		simplll 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $\$
371	370	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $\$ $/\$
372	371, 100	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
373	372	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$
374	373	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
375		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
376	375	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
377		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
378	377	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
379	35	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $\$
380	379	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $\$ $/\$
381	380	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $\$ $/\$
382	245	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
383	382	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $\$
384	256	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $\$
385	384	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $\$ $\$
386	383, 385, 264	divcld 10801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $\$ $\$
387	386	adantlll 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $\$ $\$
388	387	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $\$ $/\$ $\$
389	381, 388	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
390	389	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
391		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
392	390, 391	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
393	392	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
394	299	pm2.24d 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
395	394	impcom 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
396	395	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
397	376, 378, 393, 396	ifbothda 4123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
398	368, 369, 374, 397	ifbothda 4123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
399	398	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
400	367, 399	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
401	400	ralimdva 2962	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
402	364, 401	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
403	352, 402	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
404		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $\$ $\$
405	105, 404	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
406	405	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
407		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
408	104, 406, 99, 407, 67	ofrfval2 6915	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
409	408	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
410	403, 409	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
411		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
412	411	ifeq2d 4105	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
413	412	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
414	413	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$
415	414	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
416	350, 410, 415	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
417		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
418	417	eqcoms 2630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
419	418	biantrud 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
420		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $\$
421	420	nfeq2 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $\$
422		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
423	287, 105	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $/\$ $\$ $\$
424		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
425	424	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
426	423, 425	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
427	422, 426	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
428	427	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
429	427	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
430	428, 429	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
431	421, 430	mpteq2da 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
432	431	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
433	432	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
434	419, 433	bitr3d 270	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
435	434	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
436	320, 416, 435	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
437		simplrr 801	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$
438	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $/\$ $\$
439	236, 105	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
440	439	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $/\$ $\$
441		fconstmpt 5163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
442	441	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $\$ $\$
443		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $\$ $\$
444	197, 438, 440, 442, 443	offval2 6914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
445		ovif2 6738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $\$ $\$ $\$
446	267, 268	ifeq12d 4106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
447	445, 446	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
448	447	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
449	444, 448	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
450		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
451	450	i1f1 23457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $/\$ $\$ $\$
452	248, 253, 451	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
453	452	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$
454	453, 265	i1fmulc 23470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$ $\$
455	449, 454	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$ $\$
456		i1fsub 23475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $\$ $\$ $\$
457	234, 455, 456	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$ $\$
458		itg1cl 23452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $\$ $\$
459	457, 458	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$ $\$
460	459	adantlrl 756	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$ $\$ $\$
461	319	adantlrl 756	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
462		itg1cl 23452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
463	461, 462	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
464		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$
465		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
466	8	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
467	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
468	465, 466, 467	ltdiv1d 11917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
469		recn 10026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
470	469	2halvesd 11278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
471	470	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
472	469	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
473	472, 472	pncand 10393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
474	471, 473	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
475	474	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
476	475	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
477		rehalfcl 11258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
478	477	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
479	8	rehalfcld 11279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
480	479	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
481	465, 478, 480	ltsubaddd 10623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
482	468, 476, 481	3bitr2d 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
483	482	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
484	483	adantlrl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$
485	464, 484	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$
486	453, 265	itg1mulc 23471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
487	449	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
488	450	itg11 23458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $/\$ $\$ $\$ $\$
489	248, 253, 488	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
490	489	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $\$ $\$
491	490	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
492	253	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
493	492	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$
494	266, 493	mulcomd 10061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
495	250	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $\$ $\$
496	495	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $\$ $\$
497	260, 383	mulcomd 10061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $\$ $\$
498	496, 497	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $\$ $\$
499	498	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
500	493, 383, 385, 264	divassd 10836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
501	383, 258, 260, 262, 263	divcan5rd 10828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$ $\$
502	499, 500, 501	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $\$ $\$
503	491, 494, 502	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$ $\$
504	486, 487, 503	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$ $\$
505	504	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$ $\$
506		itg1sub 23476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
507	234, 455, 506	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
508	8	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
509	508	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
510	469	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
511	509, 510, 258, 262	divsubdird 10840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
512	511	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
513	508	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
514	513	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
515	472	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
516	513, 514, 515	subsubd 10420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
517	516	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
518	508	2halvesd 11278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
519	518	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
520	508	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
521	520, 520	pncand 10393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
522	519, 521	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
523	522	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
524	523	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
525	512, 517, 524	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
526	505, 507, 525	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$ $\$
527	526	adantlrl 756	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $\$
528	485, 527	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$ $\$ $\$
529	457	adantlrl 756	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $\$
530		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$ $/\$ $\$
531	530	adantlrl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
532	234, 36	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $\$ $/\$
533	265	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $\$ $/\$ $\$
534	532, 533	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $\$ $/\$ $\$
535	534	leidd 10594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $/\$ $\$ $\$
536	535	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$
537	296	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$ $\$ $\$
538	537	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
539	536, 538	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
540	534	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
541	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $/\$ $/\$ $\$
542	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $\$ $/\$
543	534, 542	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $\$ $/\$ $\$ $\$
544	543	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
545	540, 541, 544	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
546		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $\$ $\$ $\$
547	546	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$ $\$
548	547	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
549	545, 548	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
550	539, 549	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$
551	531, 550	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$
552	551	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
553		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $\$ $\$
554	553	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $\$ $\$
555		iba 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$ $\$ $/\$ $\$
556	555	bicomd 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $/\$ $\$ $\$
557	556	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $/\$ $\$ $\$ $\$ $\$
558	554, 557	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
559	558	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
560	552, 559	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$
561	35	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $\$
562	171	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\$ $\$
563		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\$ $/\$
564	562, 563	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $\$ $/\$
565	564	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $\$ $/\$
566	565	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $\$ $/\$
567		pm4.53 513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $\/$
568	208	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
569	568	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
570	569	pm2.24d 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
571	182	simplbda 654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
572	571	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
573	181, 572	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
574	573	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
575	570, 574	jaod 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $\/$
576	567, 575	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
577	566, 576	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $\$
578	577	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$
579	561, 578	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
580	579	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
581	580, 225	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
582	581, 30	syl6eqbr 4692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
583		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $\$
584	583	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $\$
585	300, 299	sylbir 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\/$ $\$ $\$ $/\$ $\$ $\$
586	585	olcs 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $/\$ $\$ $\$
587	584, 586	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$ $/\$ $\$ $\$
588	587	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$
589	582, 588	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$
590	560, 589	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
591	590	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$
592	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$
593		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
594	593	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
595	423	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
596		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
597	596	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$
598	200, 105	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
599	598	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
600	70	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$
601		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
602	592, 597, 599, 600, 601	offval2 6914	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
603		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
604	592, 594, 595, 602, 603	ofrfval2 6915	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$
605	591, 604	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$
606		itg1le 23480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$
607	529, 461, 605, 606	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$
608	437, 460, 463, 528, 607	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
609	608	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
610	609	adantlll 754	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
611		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $\$ $\$
612		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
613	612	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
614	613	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
615		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $\$ $\$ $\$ $/\$ $\$ $\$
616	614, 615	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
617	611, 616	spcev 3300	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $/\$
618	436, 610, 617	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
619	193, 618	pm2.61dane 2881	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
620	619	expr 643	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
621	620	adantllr 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
622	621	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
623	157, 622	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
624	139, 623	pm2.61dane 2881	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
625	624	ex 450	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
626	94, 625	sylbid 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
627	626	imp 445	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
628	627	an32s 846	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
629	628	rexlimdvaa 3032	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
630	629	expimpd 629	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
631	630	ancomsd 470	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
632	631	exlimdv 1861	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
633		eqeq1 2626	. . . . . . . . . 10
634	633	anbi2d 740	. . . . . . . . 9 $/\$ $/\$
635	634	rexbidv 3052	. . . . . . . 8 $/\$ $/\$
636	635	rexab 3369	. . . . . . 7 $/\$ $/\$ $/\$
637		eqeq1 2626	. . . . . . . . . 10
638	637	anbi2d 740	. . . . . . . . 9 $/\$ $/\$
639	638	rexbidv 3052	. . . . . . . 8 $/\$ $/\$
640	639	rexab 3369	. . . . . . 7 $/\$ $/\$ $/\$
641	632, 636, 640	3imtr4g 285	. . . . . 6 $/\$ $/\$ $/\$
642	92, 641	sylbid 230	. . . . 5 $/\$ $/\$ $/\$
643	642	impr 649	. . . 4 $/\$ $/\$ $/\$ $/\$
644	6, 15, 89, 643	eqsupd 8363	. . 3 $/\$ $/\$
645	4, 644	syl5eq 2668	. 2 $/\$
646	2, 645	eqtr4d 2659	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wex 1704

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

cvv 3200 $\$ cdif 3571

wss 3574

c0 3915

cif 4086

csn 4177 class class class wbr 4653

cmpt 4729

wor 5034

cxp 5112

ccnv 5113

cdm 5114

crn 5115

cima 5117

wfun 5882

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cof 6895

cofr 6896

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cmin 10266

cdiv 10684

c2 11070

crp 11832

cicc 12178

covol 23231

cvol 23232

citg1 23384

citg2 23385

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 ax-addf 10015

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-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-ofr 6898 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-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-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-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-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-cmp 21190 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390

This theorem is referenced by: itg2addnc 33464

W3C validator