itg2addnc - Mathbox for Brendan Leahy

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

Theorem itg2addnc 33464

Description: Alternate proof of itg2add 23526 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 23475, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 9257, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.)

**Hypotheses**
Ref	Expression
itg2addnc.f1	MblFn
itg2addnc.f2
itg2addnc.f3
itg2addnc.g2
itg2addnc.g3

**Assertion**
Ref	Expression
itg2addnc

Proof of Theorem itg2addnc Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprr 796	. . . . . . 7 $/\$ $/\$
2		itg1cl 23452	. . . . . . . 8
3	2	adantr 481	. . . . . . 7 $/\$ $/\$
4	1, 3	eqeltrd 2701	. . . . . 6 $/\$ $/\$
5	4	rexlimiva 3028	. . . . 5 $/\$
6	5	abssi 3677	. . . 4 $/\$
7	6	a1i 11	. . 3 $/\$
8		i1f0 23454	. . . . . 6
9		3nn 11186	. . . . . . . 8
10		nnrp 11842	. . . . . . . 8
11		ne0i 3921	. . . . . . . 8
12	9, 10, 11	mp2b 10	. . . . . . 7
13		itg2addnc.f2	. . . . . . . . . . . . 13
14	13	ffvelrnda 6359	. . . . . . . . . . . 12 $/\$
15		elrege0 12278	. . . . . . . . . . . 12 $/\$
16	14, 15	sylib 208	. . . . . . . . . . 11 $/\$ $/\$
17	16	simprd 479	. . . . . . . . . 10 $/\$
18	17	ralrimiva 2966	. . . . . . . . 9
19		reex 10027	. . . . . . . . . . 11
20	19	a1i 11	. . . . . . . . . 10
21		c0ex 10034	. . . . . . . . . . 11
22	21	a1i 11	. . . . . . . . . 10 $/\$
23		eqidd 2623	. . . . . . . . . 10
24	13	feqmptd 6249	. . . . . . . . . 10
25	20, 22, 14, 23, 24	ofrfval2 6915	. . . . . . . . 9
26	18, 25	mpbird 247	. . . . . . . 8
27	26	ralrimivw 2967	. . . . . . 7
28		r19.2z 4060	. . . . . . 7 $/\$
29	12, 27, 28	sylancr 695	. . . . . 6
30		fveq2 6191	. . . . . . . . . 10
31		itg10 23455	. . . . . . . . . 10
32	30, 31	syl6req 2673	. . . . . . . . 9
33	32	biantrud 528	. . . . . . . 8 $/\$
34		fveq1 6190	. . . . . . . . . . . . 13
35	21	fvconst2 6469	. . . . . . . . . . . . 13
36	34, 35	sylan9eq 2676	. . . . . . . . . . . 12 $/\$
37	36	iftrued 4094	. . . . . . . . . . 11 $/\$
38	37	mpteq2dva 4744	. . . . . . . . . 10
39	38	breq1d 4663	. . . . . . . . 9
40	39	rexbidv 3052	. . . . . . . 8
41	33, 40	bitr3d 270	. . . . . . 7 $/\$
42	41	rspcev 3309	. . . . . 6 $/\$ $/\$
43	8, 29, 42	sylancr 695	. . . . 5 $/\$
44		eqeq1 2626	. . . . . . . 8
45	44	anbi2d 740	. . . . . . 7 $/\$ $/\$
46	45	rexbidv 3052	. . . . . 6 $/\$ $/\$
47	21, 46	elab 3350	. . . . 5 $/\$ $/\$
48	43, 47	sylibr 224	. . . 4 $/\$
49		ne0i 3921	. . . 4 $/\$ $/\$
50	48, 49	syl 17	. . 3 $/\$
51		icossicc 12260	. . . . . . 7
52		fss 6056	. . . . . . 7 $/\$
53	51, 52	mpan2 707	. . . . . 6
54		eqid 2622	. . . . . . 7 $/\$ $/\$
55	54	itg2addnclem 33461	. . . . . 6 $/\$
56	13, 53, 55	3syl 18	. . . . 5 $/\$
57		itg2addnc.f3	. . . . 5
58	56, 57	eqeltrrd 2702	. . . 4 $/\$
59		ressxr 10083	. . . . . . 7
60	6, 59	sstri 3612	. . . . . 6 $/\$
61		supxrub 12154	. . . . . 6 $/\$ $/\$ $/\$ $/\$
62	60, 61	mpan 706	. . . . 5 $/\$ $/\$
63	62	rgen 2922	. . . 4 $/\$ $/\$
64		breq2 4657	. . . . . 6 $/\$ $/\$
65	64	ralbidv 2986	. . . . 5 $/\$ $/\$ $/\$ $/\$
66	65	rspcev 3309	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
67	58, 63, 66	sylancl 694	. . 3 $/\$
68		simprr 796	. . . . . . 7 $/\$ $/\$
69		itg1cl 23452	. . . . . . . 8
70	69	adantr 481	. . . . . . 7 $/\$ $/\$
71	68, 70	eqeltrd 2701	. . . . . 6 $/\$ $/\$
72	71	rexlimiva 3028	. . . . 5 $/\$
73	72	abssi 3677	. . . 4 $/\$
74	73	a1i 11	. . 3 $/\$
75		itg2addnc.g2	. . . . . . . . . . . . 13
76	75	ffvelrnda 6359	. . . . . . . . . . . 12 $/\$
77		elrege0 12278	. . . . . . . . . . . 12 $/\$
78	76, 77	sylib 208	. . . . . . . . . . 11 $/\$ $/\$
79	78	simprd 479	. . . . . . . . . 10 $/\$
80	79	ralrimiva 2966	. . . . . . . . 9
81	75	feqmptd 6249	. . . . . . . . . 10
82	20, 22, 76, 23, 81	ofrfval2 6915	. . . . . . . . 9
83	80, 82	mpbird 247	. . . . . . . 8
84	83	ralrimivw 2967	. . . . . . 7
85		r19.2z 4060	. . . . . . 7 $/\$
86	12, 84, 85	sylancr 695	. . . . . 6
87		fveq2 6191	. . . . . . . . . 10
88	87, 31	syl6req 2673	. . . . . . . . 9
89	88	biantrud 528	. . . . . . . 8 $/\$
90		fveq1 6190	. . . . . . . . . . . . 13
91	90, 35	sylan9eq 2676	. . . . . . . . . . . 12 $/\$
92	91	iftrued 4094	. . . . . . . . . . 11 $/\$
93	92	mpteq2dva 4744	. . . . . . . . . 10
94	93	breq1d 4663	. . . . . . . . 9
95	94	rexbidv 3052	. . . . . . . 8
96	89, 95	bitr3d 270	. . . . . . 7 $/\$
97	96	rspcev 3309	. . . . . 6 $/\$ $/\$
98	8, 86, 97	sylancr 695	. . . . 5 $/\$
99		eqeq1 2626	. . . . . . . 8
100	99	anbi2d 740	. . . . . . 7 $/\$ $/\$
101	100	rexbidv 3052	. . . . . 6 $/\$ $/\$
102	21, 101	elab 3350	. . . . 5 $/\$ $/\$
103	98, 102	sylibr 224	. . . 4 $/\$
104		ne0i 3921	. . . 4 $/\$ $/\$
105	103, 104	syl 17	. . 3 $/\$
106		fss 6056	. . . . . . 7 $/\$
107	51, 106	mpan2 707	. . . . . 6
108		eqid 2622	. . . . . . 7 $/\$ $/\$
109	108	itg2addnclem 33461	. . . . . 6 $/\$
110	75, 107, 109	3syl 18	. . . . 5 $/\$
111		itg2addnc.g3	. . . . 5
112	110, 111	eqeltrrd 2702	. . . 4 $/\$
113	73, 59	sstri 3612	. . . . . 6 $/\$
114		supxrub 12154	. . . . . 6 $/\$ $/\$ $/\$ $/\$
115	113, 114	mpan 706	. . . . 5 $/\$ $/\$
116	115	rgen 2922	. . . 4 $/\$ $/\$
117		breq2 4657	. . . . . 6 $/\$ $/\$
118	117	ralbidv 2986	. . . . 5 $/\$ $/\$ $/\$ $/\$
119	118	rspcev 3309	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
120	112, 116, 119	sylancl 694	. . 3 $/\$
121		eqid 2622	. . 3 $/\$ $/\$ $/\$ $/\$
122	7, 50, 67, 74, 105, 120, 121	supadd 10991	. 2 $/\$ $/\$ $/\$ $/\$
123		supxrre 12157	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124	7, 50, 67, 123	syl3anc 1326	. . . 4 $/\$ $/\$
125	56, 124	eqtrd 2656	. . 3 $/\$
126		supxrre 12157	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	74, 105, 120, 126	syl3anc 1326	. . . 4 $/\$ $/\$
128	110, 127	eqtrd 2656	. . 3 $/\$
129	125, 128	oveq12d 6668	. 2 $/\$ $/\$
130		ge0addcl 12284	. . . . . . 7 $/\$
131	51, 130	sseldi 3601	. . . . . 6 $/\$
132	131	adantl 482	. . . . 5 $/\$ $/\$
133		inidm 3822	. . . . 5
134	132, 13, 75, 20, 20, 133	off 6912	. . . 4
135		eqid 2622	. . . . 5 $/\$ $/\$
136	135	itg2addnclem 33461	. . . 4 $/\$
137	134, 136	syl 17	. . 3 $/\$
138		itg2addnc.f1	. . . . . . . 8 MblFn
139	138, 13, 57, 75, 111	itg2addnclem3 33463	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
140		simpl 473	. . . . . . . . . . . . . 14 $/\$
141		simpr 477	. . . . . . . . . . . . . 14 $/\$
142	140, 141	i1fadd 23462	. . . . . . . . . . . . 13 $/\$
143	142	ad3antlr 767	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
144		reeanv 3107	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
145	144	biimpri 218	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	145	ad2ant2r 783	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147		ifcl 4130	. . . . . . . . . . . . . . . . . . 19 $/\$
148	147	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . 24
150	149	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
151	150	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
152		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . 24
153	152	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
154	153	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
155		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . 25
156	155	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	156	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
158		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
160	159	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
161		oveq12 6659	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
162		00id 10211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
163	161, 162	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
164	163	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
165	164	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
167	15	simplbi 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
168	14, 167	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
169	77	simplbi 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
170	76, 169	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
171	168, 170, 17, 79	addge0d 10603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
172	166, 171	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	165, 173	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175	174	a1d 25	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	172	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
178		simplrr 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
179		i1ff 23443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
180	179	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
181	178, 180	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
182	181	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
183	182	addid2d 10237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
184	177, 183	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
185	184	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
186	185	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
187	147	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
188	187	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
189	181, 188	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
190	189	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
191	166, 170	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
193	166, 168	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
194	193, 191	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
195	194	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
196		simplrr 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
197	196	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
198		rpre 11839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
199		rpre 11839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
200		min2 12021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
201	198, 199, 200	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
202	201	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
203	188, 197, 181, 202	leadd2dd 10642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
204	181, 197	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
205		letr 10131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
206	189, 204, 191, 205	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
207	203, 206	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
208	207	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
209	170, 168	addge02d 10616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
210	17, 209	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
211	166, 210	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
212	211	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
213	190, 192, 195, 208, 212	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
214	213	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
215	186, 214	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
216		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
217		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218	216, 217	ifboth 4124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
219	176, 215, 218	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
220	219	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
221	220	adantld 483	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
222	221	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
223	157, 160, 175, 222	ifbothda 4123	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
224	155	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
225	224	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
226	158	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
227	226	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
228	172	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
229		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
230		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
231		i1ff 23443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
232	231	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
233	230, 232	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
234	233	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
235	234	addid1d 10236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
236	229, 235	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
237	236	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
238	237	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
239	233, 188	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
240	239	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
241	193	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
242	194	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
243		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
244	243	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
245		min1 12020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
246	198, 199, 245	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
247	246	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
248	188, 244, 233, 247	leadd2dd 10642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
249	233, 244	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
250		letr 10131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
251	239, 249, 193, 250	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
252	248, 251	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
253	252	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254	168, 170	addge01d 10615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
255	79, 254	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
256	166, 255	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
257	256	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
258	240, 241, 242, 253, 257	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
259	258	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
260	238, 259	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
261	228, 260, 218	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
262	261	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
263	262	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
264	263	adantrd 484	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
265	172	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
266	188	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
267	234, 182, 266	addassd 10062	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
268	267	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
269	233, 243	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
270	233, 249, 269	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
271		letr 10131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
272	233, 249, 193, 271	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
273	270, 272	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
274		le2add 10510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
275	233, 189, 193, 191, 274	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
276	273, 207, 275	syl2and 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
277	276	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
278	268, 277	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
279	265, 278, 218	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
280	279	ex 450	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
281	280	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
282	225, 227, 264, 281	ifbothda 4123	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
283	151, 154, 223, 282	ifbothda 4123	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
284	283	ralimdva 2962	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
285		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . 26
286	21, 285	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . 25
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
288		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . 24
289	20, 287, 14, 288, 24	ofrfval2 6915	. . . . . . . . . . . . . . . . . . . . . . 23
290		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . 26
291	21, 290	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . 25
292	291	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
293		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . 24
294	20, 292, 76, 293, 81	ofrfval2 6915	. . . . . . . . . . . . . . . . . . . . . . 23
295	289, 294	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
296		r19.26 3064	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
297	295, 296	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
298	297	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
299	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
300		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
301	21, 300	ifex 4156	. . . . . . . . . . . . . . . . . . . . . 22
302	301	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
303		ovexd 6680	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
304		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
305	231, 304	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
306	305	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
307	306	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
308		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
309	179, 308	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
310	309	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
311	310	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
312		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
313		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
314	307, 311, 299, 299, 133, 312, 313	ofval 6906	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
315	314	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
316	314	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
317	315, 316	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
318	317	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
319		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . 24
320	13, 319	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
321		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . 24
322	75, 321	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
323		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
324		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
325	320, 322, 20, 20, 133, 323, 324	offval 6904	. . . . . . . . . . . . . . . . . . . . . 22
326	325	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
327	299, 302, 303, 318, 326	ofrfval2 6915	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
328	284, 298, 327	3imtr4d 283	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
329	328	imp 445	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
330		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22
331	330	ifeq2d 4105	. . . . . . . . . . . . . . . . . . . . 21
332	331	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . 20
333	332	breq1d 4663	. . . . . . . . . . . . . . . . . . 19
334	333	rspcev 3309	. . . . . . . . . . . . . . . . . 18 $/\$
335	148, 329, 334	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
336	335	ex 450	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
337	336	rexlimdvva 3038	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
338	146, 337	syl5 34	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
339	338	a1dd 50	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
340	339	imp31 448	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
341		oveq12 6659	. . . . . . . . . . . . . . 15 $/\$
342	341	ad2ant2l 782	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
343	140, 141	itg1add 23468	. . . . . . . . . . . . . . . 16 $/\$
344	343	eqcomd 2628	. . . . . . . . . . . . . . 15 $/\$
345	344	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
346	342, 345	sylan9eqr 2678	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
347		eqtr 2641	. . . . . . . . . . . . . 14 $/\$
348	347	ancoms 469	. . . . . . . . . . . . 13 $/\$
349	346, 348	sylan 488	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
350		fveq1 6190	. . . . . . . . . . . . . . . . . . 19
351	350	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18
352	350	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
353	351, 352	ifbieq2d 4111	. . . . . . . . . . . . . . . . 17
354	353	mpteq2dv 4745	. . . . . . . . . . . . . . . 16
355	354	breq1d 4663	. . . . . . . . . . . . . . 15
356	355	rexbidv 3052	. . . . . . . . . . . . . 14
357		fveq2 6191	. . . . . . . . . . . . . . 15
358	357	eqeq2d 2632	. . . . . . . . . . . . . 14
359	356, 358	anbi12d 747	. . . . . . . . . . . . 13 $/\$ $/\$
360	359	rspcev 3309	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
361	143, 340, 349, 360	syl12anc 1324	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
362	361	exp31 630	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
363	362	rexlimdvva 3038	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
364	363	impd 447	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
365	364	exlimdvv 1862	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
366	139, 365	impbid 202	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
367		eqeq1 2626	. . . . . . . . . 10
368	367	anbi2d 740	. . . . . . . . 9 $/\$ $/\$
369	368	rexbidv 3052	. . . . . . . 8 $/\$ $/\$
370	369	rexab 3369	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
371		eqeq1 2626	. . . . . . . . . . . . 13
372	371	anbi2d 740	. . . . . . . . . . . 12 $/\$ $/\$
373	372	rexbidv 3052	. . . . . . . . . . 11 $/\$ $/\$
374	373	rexab 3369	. . . . . . . . . 10 $/\$ $/\$ $/\$
375	374	anbi2i 730	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
376		19.42v 1918	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
377		reeanv 3107	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
378	377	anbi1i 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
379		anass 681	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
380	378, 379	bitr2i 265	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
381	380	exbii 1774	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
382	375, 376, 381	3bitr2i 288	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
383	382	exbii 1774	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
384	370, 383	bitri 264	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
385	366, 384	syl6bbr 278	. . . . 5 $/\$ $/\$ $/\$
386	385	abbidv 2741	. . . 4 $/\$ $/\$ $/\$
387	386	supeq1d 8352	. . 3 $/\$ $/\$ $/\$
388		simpr 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
389	6	sseli 3599	. . . . . . . . . . 11 $/\$
390	389	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
391	73	sseli 3599	. . . . . . . . . . 11 $/\$
392	391	ad2antlr 763	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
393	390, 392	readdcld 10069	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
394	388, 393	eqeltrd 2701	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
395	394	ex 450	. . . . . . 7 $/\$ $/\$ $/\$
396	395	rexlimivv 3036	. . . . . 6 $/\$ $/\$
397	396	abssi 3677	. . . . 5 $/\$ $/\$
398	397	a1i 11	. . . 4 $/\$ $/\$
399	162	eqcomi 2631	. . . . . . . 8
400		rspceov 6692	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
401	399, 400	mp3an3 1413	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
402	48, 103, 401	syl2anc 693	. . . . . 6 $/\$ $/\$
403		eqeq1 2626	. . . . . . . 8
404	403	2rexbidv 3057	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
405	21, 404	spcev 3300	. . . . . 6 $/\$ $/\$ $/\$ $/\$
406	402, 405	syl 17	. . . . 5 $/\$ $/\$
407		abn0 3954	. . . . 5 $/\$ $/\$ $/\$ $/\$
408	406, 407	sylibr 224	. . . 4 $/\$ $/\$
409	58, 112	readdcld 10069	. . . . 5 $/\$ $/\$
410		simpr 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
411	389	ad2antrl 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
412	391	ad2antll 765	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
413	58	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
414	112	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
415		supxrub 12154	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
416	60, 415	mpan 706	. . . . . . . . . . . 12 $/\$ $/\$
417	416	ad2antrl 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
418		supxrub 12154	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
419	113, 418	mpan 706	. . . . . . . . . . . 12 $/\$ $/\$
420	419	ad2antll 765	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
421	411, 412, 413, 414, 417, 420	le2addd 10646	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
422	421	adantr 481	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
423	410, 422	eqbrtrd 4675	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
424	423	ex 450	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
425	424	rexlimdvva 3038	. . . . . 6 $/\$ $/\$ $/\$ $/\$
426	425	alrimiv 1855	. . . . 5 $/\$ $/\$ $/\$ $/\$
427		breq2 4657	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
428	427	ralbidv 2986	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
429		eqeq1 2626	. . . . . . . . 9
430	429	2rexbidv 3057	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
431	430	ralab 3367	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
432	428, 431	syl6bb 276	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
433	432	rspcev 3309	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
434	409, 426, 433	syl2anc 693	. . . 4 $/\$ $/\$
435		supxrre 12157	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
436	398, 408, 434, 435	syl3anc 1326	. . 3 $/\$ $/\$ $/\$ $/\$
437	137, 387, 436	3eqtrd 2660	. 2 $/\$ $/\$
438	122, 129, 437	3eqtr4rd 2667	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wal 1481

wceq 1483

wex 1704

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

cvv 3200

wss 3574

c0 3915

cif 4086

csn 4177 class class class wbr 4653

cmpt 4729

cxp 5112

cdm 5114

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cof 6895

cofr 6896

csup 8346

cr 9935

cc0 9936

caddc 9939

cpnf 10071

cxr 10073

clt 10074

cle 10075

cn 11020

c3 11071

crp 11832

cico 12177

cicc 12178 MblFncmbf 23383

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: ibladdnclem 33466 itgaddnclem1 33468 iblabsnclem 33473 iblabsnc 33474 iblmulc2nc 33475 ftc1anclem4 33488 ftc1anclem5 33489 ftc1anclem6 33490 ftc1anclem8 33492

W3C validator