itg2gt0cn - Mathbox for Brendan Leahy

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

Theorem itg2gt0cn 33465

Description: itg2gt0 23527 holds on functions continuous on an open interval in the absence of ax-cc 9257. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.)

**Hypotheses**
Ref	Expression
itg2gt0cn.2
itg2gt0cn.3
itg2gt0cn.5	$/\$
itg2gt0cn.cn

**Assertion**
Ref	Expression
itg2gt0cn

Distinct variable groups:

Proof of Theorem itg2gt0cn Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0xr 10086	. . . 4
2	1	a1i 11	. . 3
3		imassrn 5477	. . . . 5
4		itg2gt0cn.3	. . . . . . 7
5		frn 6053	. . . . . . 7
6	4, 5	syl 17	. . . . . 6
7		icossxr 12258	. . . . . 6
8	6, 7	syl6ss 3615	. . . . 5
9	3, 8	syl5ss 3614	. . . 4
10		supxrcl 12145	. . . 4
11	9, 10	syl 17	. . 3
12		itg2gt0cn.2	. . . . . 6
13		ltrelxr 10099	. . . . . . . . . 10
14	13	ssbri 4697	. . . . . . . . 9
15	12, 14	syl 17	. . . . . . . 8
16		brxp 5147	. . . . . . . 8 $/\$
17	15, 16	sylib 208	. . . . . . 7 $/\$
18		ioon0 12201	. . . . . . 7 $/\$
19	17, 18	syl 17	. . . . . 6
20	12, 19	mpbird 247	. . . . 5
21		itg2gt0cn.5	. . . . . 6 $/\$
22	21	ralrimiva 2966	. . . . 5
23		r19.2z 4060	. . . . 5 $/\$
24	20, 22, 23	syl2anc 693	. . . 4
25		supxrlub 12155	. . . . . 6 $/\$
26	9, 1, 25	sylancl 694	. . . . 5
27		ffn 6045	. . . . . . 7
28	4, 27	syl 17	. . . . . 6
29		ioossre 12235	. . . . . 6
30		breq2 4657	. . . . . . 7
31	30	rexima 6497	. . . . . 6 $/\$
32	28, 29, 31	sylancl 694	. . . . 5
33	26, 32	bitrd 268	. . . 4
34	24, 33	mpbird 247	. . 3
35		qbtwnxr 12031	. . 3 $/\$ $/\$ $/\$
36	2, 11, 34, 35	syl3anc 1326	. 2 $/\$
37		qre 11793	. . . . . . . . 9
38	37	adantr 481	. . . . . . . 8 $/\$
39		simpr 477	. . . . . . . 8 $/\$
40	38, 39	elrpd 11869	. . . . . . 7 $/\$
41	40	anim1i 592	. . . . . 6 $/\$ $/\$ $/\$
42	41	anasss 679	. . . . 5 $/\$ $/\$ $/\$
43		simplr 792	. . . . . . 7 $/\$ $/\$
44		rpxr 11840	. . . . . . . . . . 11
45		supxrlub 12155	. . . . . . . . . . 11 $/\$
46	9, 44, 45	syl2an 494	. . . . . . . . . 10 $/\$
47		breq2 4657	. . . . . . . . . . . . 13
48	47	rexima 6497	. . . . . . . . . . . 12 $/\$
49	28, 29, 48	sylancl 694	. . . . . . . . . . 11
50	49	adantr 481	. . . . . . . . . 10 $/\$
51	46, 50	bitrd 268	. . . . . . . . 9 $/\$
52	1	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
53		ioorp 12251	. . . . . . . . . . . . . . . . . . . 20
54		ioossicc 12259	. . . . . . . . . . . . . . . . . . . 20
55	53, 54	eqsstr3i 3636	. . . . . . . . . . . . . . . . . . 19
56	55	sseli 3599	. . . . . . . . . . . . . . . . . 18
57		0e0iccpnf 12283	. . . . . . . . . . . . . . . . . 18
58		ifcl 4130	. . . . . . . . . . . . . . . . . 18 $/\$
59	56, 57, 58	sylancl 694	. . . . . . . . . . . . . . . . 17
60	59	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
61		eqid 2622	. . . . . . . . . . . . . . . 16
62	60, 61	fmptd 6385	. . . . . . . . . . . . . . 15
63		itg2cl 23499	. . . . . . . . . . . . . . 15
64	62, 63	syl 17	. . . . . . . . . . . . . 14
65	64	ad5antlr 771	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
66		ifcl 4130	. . . . . . . . . . . . . . . . . 18 $/\$
67	56, 57, 66	sylancl 694	. . . . . . . . . . . . . . . . 17
68	67	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
69		eqid 2622	. . . . . . . . . . . . . . . 16
70	68, 69	fmptd 6385	. . . . . . . . . . . . . . 15
71		itg2cl 23499	. . . . . . . . . . . . . . 15
72	70, 71	syl 17	. . . . . . . . . . . . . 14
73	72	ad5antlr 771	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
74		rpre 11839	. . . . . . . . . . . . . . . . 17
75	74	ad4antlr 769	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
76		ioombl 23333	. . . . . . . . . . . . . . . . . . 19
77		mblvol 23298	. . . . . . . . . . . . . . . . . . 19
78	76, 77	ax-mp 5	. . . . . . . . . . . . . . . . . 18
79		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . 23
80	79	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
81		rpre 11839	. . . . . . . . . . . . . . . . . . . . . . 23
82	81	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
83	80, 82	resubcld 10458	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
84	83	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
85	83	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
86	85	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
87	17	simpld 475	. . . . . . . . . . . . . . . . . . . . . 22
88	87	ad5antr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
89	17	simprd 479	. . . . . . . . . . . . . . . . . . . . . 22
90	89	ad5antr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
91	87	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
92		xrltnle 10105	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	85, 91, 92	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
94	93	biimpar 502	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
95	12	ad5antr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
96		xrre2 12001	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
97	86, 88, 90, 94, 95, 96	syl32anc 1334	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
98	84, 97	ifclda 4120	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
99	89	ad5antr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
100	82, 80	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
101	100	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
102		mnfxr 10096	. . . . . . . . . . . . . . . . . . . . . . . 24
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
104		mnfle 11969	. . . . . . . . . . . . . . . . . . . . . . . 24
105	87, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
106	103, 87, 89, 105, 12	xrlelttrd 11991	. . . . . . . . . . . . . . . . . . . . . 22
107	106	ad5antr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
108		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
109		xrre 12000	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
110	99, 101, 107, 108, 109	syl22anc 1327	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
111	100	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
112	110, 111	ifclda 4120	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
113	80	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
114	89	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
115		rpgt0 11844	. . . . . . . . . . . . . . . . . . . . . . . . 25
116	115	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
117	82, 80	ltsubposd 10613	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
118	116, 117	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
119		eliooord 12233	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
120	119	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . 24
121	120	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
122	85, 113, 114, 118, 121	xrlttrd 11990	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
123	82, 80	ltaddpos2d 10612	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
124	116, 123	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
125	83, 80, 100, 118, 124	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
126		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . 23
127		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . 23
128	126, 127	ifboth 4124	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
129	122, 125, 128	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
130	12	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
131	100	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
132	119	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . 24
133	132	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
134	91, 113, 131, 133, 124	xrlttrd 11990	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
135		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . 23
136		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . 23
137	135, 136	ifboth 4124	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	130, 134, 137	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
139		breq1 4656	. . . . . . . . . . . . . . . . . . . . . 22
140		breq1 4656	. . . . . . . . . . . . . . . . . . . . . 22
141	139, 140	ifboth 4124	. . . . . . . . . . . . . . . . . . . . 21 $/\$
142	129, 138, 141	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
143	98, 112, 142	ltled 10185	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
144		ovolioo 23336	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
145	98, 112, 143, 144	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
146	78, 145	syl5eq 2668	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
147	112, 98	resubcld 10458	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
148	146, 147	eqeltrd 2701	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
149		rpgt0 11844	. . . . . . . . . . . . . . . . 17
150	149	ad4antlr 769	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
151	98, 112	posdifd 10614	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
152	142, 151	mpbid 222	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
153	152, 146	breqtrrd 4681	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
154	75, 148, 150, 153	mulgt0d 10192	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
155		iooin 12209	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
156	91, 114, 85, 131, 155	syl22anc 1327	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
157	156	eleq2d 2687	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
158	157	ifbid 4108	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
159	158	mpteq2dv 4745	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
160	159	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
161	76	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
162		rpge0 11845	. . . . . . . . . . . . . . . . . . 19
163		elrege0 12278	. . . . . . . . . . . . . . . . . . 19 $/\$
164	74, 162, 163	sylanbrc 698	. . . . . . . . . . . . . . . . . 18
165	164	ad4antlr 769	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
166		itg2const 23507	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
167	161, 148, 165, 166	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
168	160, 167	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
169	154, 168	breqtrrd 4681	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
170	169	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
171	62	ad5antlr 771	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
172	70	ad5antlr 771	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
173		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . 26
174	173	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
175	174	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . 24
176		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
177	176	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26
178	177	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
179	178	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . 24
180	175, 179	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23
181	180	rspccva 3308	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
182		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . 23
183		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . 23
184	74	leidd 10594	. . . . . . . . . . . . . . . . . . . . . . . . 25
185	184	ad6antlr 773	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
186	79	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
187	81	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
188	186, 187	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
189	188	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
190	187, 186	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
191	190	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
192		elioo2 12216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
193	189, 191, 192	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
194		3anass 1042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
195	193, 194	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
196		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	79	ad5antlr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
198	196, 197	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
199	81	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
200	198, 199	absltd 14168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
201	199	renegcld 10457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
202	197, 201, 196	ltaddsub2d 10628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
203	197	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
204	199	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
205	203, 204	negsubd 10398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
206	205	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
207	202, 206	bitr3d 270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
208	196, 197, 199	ltsubaddd 10623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
209	207, 208	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
210	200, 209	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
211	210	pm5.32da 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
212	195, 211	bitr4d 271	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
213	212	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
214		pm3.35 611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
215	214	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
216	74	ad6antlr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
217		rge0ssre 12280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
218	4	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
219	218	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
220	217, 219	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
221	220	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
222	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
223	222	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
224	217, 223	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
225	79, 224	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
226	225	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
227	220, 226	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
228	74	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
229	225, 228	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
230	229	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
231	227, 230	absltd 14168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
232	225	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
233		rpcn 11841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
234	233	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
235	232, 234	negsubdi2d 10408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
236	235	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
237	236	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
238	237	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
239	231, 238	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
240	239	simprbda 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
241	225	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
242	216, 221, 241	ltsub1d 10636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
243	240, 242	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
244	216, 221, 243	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245	215, 244	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
246	245	an4s 869	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
247	213, 246	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248	247	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
249	185, 248	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
250		0le0 11110	. . . . . . . . . . . . . . . . . . . . . . . . 25
251		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . 26
252		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . 26
253	251, 252	ifboth 4124	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
254	162, 250, 253	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . 24
255	254	ad6antlr 773	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
256	182, 183, 249, 255	ifbothda 4123	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
257	181, 256	sylan2 491	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
258	257	anassrs 680	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
259		iftrue 4092	. . . . . . . . . . . . . . . . . . . . 21
260	259	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
261		iftrue 4092	. . . . . . . . . . . . . . . . . . . . 21
262	261	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
263	258, 260, 262	3brtr4d 4685	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
264	263	ex 450	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
265	250	a1i 11	. . . . . . . . . . . . . . . . . . 19
266		iffalse 4095	. . . . . . . . . . . . . . . . . . 19
267		iffalse 4095	. . . . . . . . . . . . . . . . . . 19
268	265, 266, 267	3brtr4d 4685	. . . . . . . . . . . . . . . . . 18
269	264, 268	pm2.61d1 171	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
270		elin 3796	. . . . . . . . . . . . . . . . . . 19 $/\$
271		ifbi 4107	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
272	270, 271	ax-mp 5	. . . . . . . . . . . . . . . . . 18 $/\$
273		ifan 4134	. . . . . . . . . . . . . . . . . 18 $/\$
274	272, 273	eqtri 2644	. . . . . . . . . . . . . . . . 17
275		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
276	275	breq2d 4665	. . . . . . . . . . . . . . . . . . . 20
277	276	elrab 3363	. . . . . . . . . . . . . . . . . . 19 $/\$
278		ifbi 4107	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
279	277, 278	ax-mp 5	. . . . . . . . . . . . . . . . . 18 $/\$
280		ifan 4134	. . . . . . . . . . . . . . . . . 18 $/\$
281	279, 280	eqtri 2644	. . . . . . . . . . . . . . . . 17
282	269, 274, 281	3brtr4g 4687	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
283	282	ralrimivw 2967	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
284		reex 10027	. . . . . . . . . . . . . . . . 17
285	284	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
286	59	ad6antlr 773	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
287	67	ad6antlr 773	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
288		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
289		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
290	285, 286, 287, 288, 289	ofrfval2 6915	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
291	283, 290	mpbird 247	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
292		itg2le 23506	. . . . . . . . . . . . . 14 $/\$ $/\$
293	171, 172, 291, 292	syl3anc 1326	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
294	52, 65, 73, 170, 293	xrltletrd 11992	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
295		itg2gt0cn.cn	. . . . . . . . . . . . . . . . 17
296	295	ad3antrrr 766	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
297		simplr 792	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
298		fssres 6070	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
299	29, 298	mpan2 707	. . . . . . . . . . . . . . . . . . . . . 22
300		fss 6056	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
301	217, 300	mpan2 707	. . . . . . . . . . . . . . . . . . . . . 22
302	4, 299, 301	3syl 18	. . . . . . . . . . . . . . . . . . . . 21
303	302	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
304	303	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
305	304, 228	resubcld 10458	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
306	305	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
307	228, 304	posdifd 10614	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
308	307	biimpa 501	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
309	306, 308	elrpd 11869	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
310		cncfi 22697	. . . . . . . . . . . . . . . 16 $/\$ $/\$
311	296, 297, 309, 310	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
312	311	ex 450	. . . . . . . . . . . . . 14 $/\$ $/\$
313		fvres 6207	. . . . . . . . . . . . . . . 16
314	313	breq2d 4665	. . . . . . . . . . . . . . 15
315	314	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
316		fvres 6207	. . . . . . . . . . . . . . . . . . . . 21
317	316	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
318	313	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
319	317, 318	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
320	319	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
321	313	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
322	321	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
323	320, 322	breq12d 4666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
324	323	imbi2d 330	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
325	324	ralbidva 2985	. . . . . . . . . . . . . . 15 $/\$ $/\$
326	325	rexbidv 3052	. . . . . . . . . . . . . 14 $/\$ $/\$
327	312, 315, 326	3imtr3d 282	. . . . . . . . . . . . 13 $/\$ $/\$
328	327	imp 445	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
329	294, 328	r19.29a 3078	. . . . . . . . . . 11 $/\$ $/\$ $/\$
330	329	ex 450	. . . . . . . . . 10 $/\$ $/\$
331	330	rexlimdva 3031	. . . . . . . . 9 $/\$
332	51, 331	sylbid 230	. . . . . . . 8 $/\$
333	332	imp 445	. . . . . . 7 $/\$ $/\$
334	70	ad2antlr 763	. . . . . . . 8 $/\$ $/\$
335		icossicc 12260	. . . . . . . . . 10
336		fss 6056	. . . . . . . . . 10 $/\$
337	4, 335, 336	sylancl 694	. . . . . . . . 9
338	337	ad2antrr 762	. . . . . . . 8 $/\$ $/\$
339		breq1 4656	. . . . . . . . . . . 12
340		breq1 4656	. . . . . . . . . . . 12
341	277	simprbi 480	. . . . . . . . . . . . 13
342	341	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$
343	4	ffvelrnda 6359	. . . . . . . . . . . . . . 15 $/\$
344		elrege0 12278	. . . . . . . . . . . . . . 15 $/\$
345	343, 344	sylib 208	. . . . . . . . . . . . . 14 $/\$ $/\$
346	345	simprd 479	. . . . . . . . . . . . 13 $/\$
347	346	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$
348	339, 340, 342, 347	ifbothda 4123	. . . . . . . . . . 11 $/\$
349	348	ralrimiva 2966	. . . . . . . . . 10
350	349	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$
351	284	a1i 11	. . . . . . . . . 10 $/\$ $/\$
352	67	ad3antlr 767	. . . . . . . . . 10 $/\$ $/\$ $/\$
353		fvexd 6203	. . . . . . . . . 10 $/\$ $/\$ $/\$
354		eqidd 2623	. . . . . . . . . 10 $/\$ $/\$
355	4	feqmptd 6249	. . . . . . . . . . 11
356	355	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$
357	351, 352, 353, 354, 356	ofrfval2 6915	. . . . . . . . 9 $/\$ $/\$
358	350, 357	mpbird 247	. . . . . . . 8 $/\$ $/\$
359		itg2le 23506	. . . . . . . 8 $/\$ $/\$
360	334, 338, 358, 359	syl3anc 1326	. . . . . . 7 $/\$ $/\$
361	43, 333, 360	jca32 558	. . . . . 6 $/\$ $/\$ $/\$ $/\$
362	361	expl 648	. . . . 5 $/\$ $/\$ $/\$
363	42, 362	syl5 34	. . . 4 $/\$ $/\$ $/\$ $/\$
364	363	reximdv2 3014	. . 3 $/\$ $/\$
365	1	a1i 11	. . . . 5 $/\$
366	72	adantl 482	. . . . 5 $/\$
367		itg2cl 23499	. . . . . . 7
368	337, 367	syl 17	. . . . . 6
369	368	adantr 481	. . . . 5 $/\$
370		xrltletr 11988	. . . . 5 $/\$ $/\$ $/\$
371	365, 366, 369, 370	syl3anc 1326	. . . 4 $/\$ $/\$
372	371	rexlimdva 3031	. . 3 $/\$
373	364, 372	syld 47	. 2 $/\$
374	36, 373	mpd 15	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

cin 3573

wss 3574

c0 3915

cif 4086 class class class wbr 4653

cmpt 4729

cxp 5112

cdm 5114

crn 5115

cres 5116

cima 5117

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cofr 6896

csup 8346

cc 9934

cr 9935

cc0 9936

caddc 9939

cmul 9941

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cq 11788

crp 11832

cioo 12175

cico 12177

cicc 12178

cabs 13974

ccncf 22679

covol 23231

cvol 23232

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-rlim 14220 df-sum 14417 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-cncf 22681 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-0p 23437

This theorem is referenced by: itggt0cn 33482

W3C validator