iintlem1 - Mathbox for Frédéric Liné

Mathbox for Frédéric Liné

< Previous Next >
Related theorems
Unicode version

Theorem iintlem1 15010

Description: Lemma for iint 15012.

**Assertion**
Ref	Expression
iintlem1	$/\$ (,)

Distinct variable groups:

**Proof of Theorem iintlem1**
Step	Hyp	Ref	Expression
1		eliin 3260	. . . . . . 7 (,) (,) (,)
2		resubcl 6601	. . . . . . . . . . . . . . . . . . 19 $/\$
3	2	ancoms 484	. . . . . . . . . . . . . . . . . 18 $/\$
4	3	recnd 6468	. . . . . . . . . . . . . . . . 17 $/\$
5	4	adantr 425	. . . . . . . . . . . . . . . 16 $/\$ $/\$
6		recn 6466	. . . . . . . . . . . . . . . . . . . . . . 23
7		recn 6466	. . . . . . . . . . . . . . . . . . . . . . 23
8	6, 7	anim12i 360	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
9	8	ancoms 484	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
10		subeq0 6563	. . . . . . . . . . . . . . . . . . . . 21 $/\$
11	9, 10	syl 12	. . . . . . . . . . . . . . . . . . . 20 $/\$
12	11	biimpd 170	. . . . . . . . . . . . . . . . . . 19 $/\$
13	12	con3d 111	. . . . . . . . . . . . . . . . . 18 $/\$
14	13	imp 377	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
15		df-ne 2019	. . . . . . . . . . . . . . . . 17
16	14, 15	sylibr 217	. . . . . . . . . . . . . . . 16 $/\$ $/\$
17		absrpcl 8106	. . . . . . . . . . . . . . . 16 $/\$
18	5, 16, 17	syl11anc 524	. . . . . . . . . . . . . . 15 $/\$ $/\$
19		2re 7163	. . . . . . . . . . . . . . . 16
20		2pos 7173	. . . . . . . . . . . . . . . 16
21	19, 20	elrpii 7234	. . . . . . . . . . . . . . 15
22	18, 21	jctir 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
23		rpdivcl 7249	. . . . . . . . . . . . . 14 $/\$
24	22, 23	syl 12	. . . . . . . . . . . . 13 $/\$ $/\$
25		simplr 449	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
26	25	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
27		simpll 448	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
29		0re 6603	. . . . . . . . . . . . . . . . . . . . . . . . 25
30		ltsubadd2 6811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
31		simp2 877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
32		addid1 6463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
33	31, 7, 32	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
34	33	breq2d 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
35	30, 34	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
36	35	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
37	36	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . 26
38	37	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . 25
39	29, 38	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . 24
40	39	imp 377	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
41	40	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
42	41	impcom 378	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
43	26, 28, 42	3jca 1050	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		msra3 15009	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
45		orc 291	. . . . . . . . . . . . . . . . . . . 20 $\/$
46	43, 44, 45	3syl 24	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$
47		pm3.22 486	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
48	47	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
49	48	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
50		msr3 15003	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	49, 50	syl 12	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
52		leloe 6688	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$
53	26, 51, 52	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$
54	46, 53	mpbird 213	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
55		rexr 6668	. . . . . . . . . . . . . . . . . . . . . 22
56	55	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 $/\$
57	56	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
58	57	adantl 424	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
59		rexr 6668	. . . . . . . . . . . . . . . . . . . . 21
60	48, 50, 59	3syl 24	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
61	60	adantl 424	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
62		xrlenlt 6670	. . . . . . . . . . . . . . . . . . 19 $/\$
63	58, 61, 62	syl11anc 524	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
64	54, 63	mpbid 212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
65	64	intn3an2d 14264	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	27	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
67	25	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
68		rexr 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
69	2, 68	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	69	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
71	70	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
72		rexr 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
73	29, 72	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . 26
74	71, 73	jctil 316	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
75		xrlenlt 6670	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
76	74, 75	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
77		subge0 6863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78	77	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
79	78	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
80		ltlen 6692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
81	80	biimprcd 173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
82	81	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
83	82	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
84	83	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
85		df-ne 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
86	84, 85	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
87	86	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
88	79, 87	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
89	76, 88	sylbird 222	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
90	89	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
91	90	impcom 378	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
92	66, 67, 91	3jca 1050	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		mslb1 15007	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
94		orc 291	. . . . . . . . . . . . . . . . . . . 20 $\/$
95	92, 93, 94	3syl 24	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$
96		simprll 456	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
97		msr4 15004	. . . . . . . . . . . . . . . . . . . . 21 $/\$
98	96, 97	syl 12	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
99		leloe 6688	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$
100	98, 67, 99	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\/$
101	95, 100	mpbird 213	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
102		readdcl 6455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
103		rexr 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104	102, 103	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
105	104	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . 25
106		rpre 7236	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	105, 106	syl5 20	. . . . . . . . . . . . . . . . . . . . . . . 24
108	107	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
109	108	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
110	55	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
111	109, 110	jca 310	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
112	111	adantlr 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
113	112	adantl 424	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
114		xrlenlt 6670	. . . . . . . . . . . . . . . . . . 19 $/\$
115	113, 114	syl 12	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
116	101, 115	mpbid 212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
117	116	intn3an3d 14265	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	65, 117	pm2.61ian 534	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
119	106	anim2i 362	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
120		resubcl 6601	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	119, 120, 59	3syl 24	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	119, 102, 103	3syl 24	. . . . . . . . . . . . . . . . . . . 20 $/\$
123	121, 122	jca 310	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
124	123	ex 402	. . . . . . . . . . . . . . . . . 18 $/\$
125	124	ad2antrr 440	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
126	125	imp 377	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
127		elioo1 7545	. . . . . . . . . . . . . . . 16 $/\$ (,) $/\$ $/\$
128	126, 127	syl 12	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ (,) $/\$ $/\$
129	118, 128	mtbird 783	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ (,)
130	129	ex 402	. . . . . . . . . . . . 13 $/\$ $/\$ (,)
131	24, 130	jcai 313	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ (,)
132	131	ex 402	. . . . . . . . . . 11 $/\$ $/\$ (,)
133		opreq2 4890	. . . . . . . . . . . . . . 15
134		opreq2 4890	. . . . . . . . . . . . . . 15
135	133, 134	opreq12d 4900	. . . . . . . . . . . . . 14 (,) (,)
136	135	eleq2d 1964	. . . . . . . . . . . . 13 (,) (,)
137	136	notbid 673	. . . . . . . . . . . 12 (,) (,)
138	137	rcla4ev 2381	. . . . . . . . . . 11 $/\$ (,) (,)
139	132, 138	syl6 25	. . . . . . . . . 10 $/\$ (,)
140		rexnal 2114	. . . . . . . . . 10 (,) (,)
141	139, 140	syl6ib 229	. . . . . . . . 9 $/\$ (,)
142	141	con4d 91	. . . . . . . 8 $/\$ (,)
143	142	com12 14	. . . . . . 7 (,) $/\$
144	1, 143	syl6bi 231	. . . . . 6 (,) (,) $/\$
145	144	pm2.43i 78	. . . . 5 (,) $/\$
146	145	com12 14	. . . 4 $/\$ (,)
147	146	ex 402	. . 3 (,)
148	147	com23 36	. 2 (,)
149	148	imp 377	1 $/\$ (,)

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 163 $\/$ wo 239 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

wne 2017

wral 2105

wrex 2106

ciin 3256 class class class wbr 3338

cfv 3998 (class class class)co 4884

cc 6384

cr 6385

cc0 6386

caddc 6389

cmin 6445

cdiv 6447

cle 6448

crp 6453

cxr 6652

clt 6653

c2 7145 (,)cioo 7524

cabs 8000

This theorem is referenced by: iint 15012

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-nel 2020 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-iin 3258 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-mpt 5006 df-1st 5020 df-2nd 5021 df-iota 5089 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-en 5427 df-dom 5428 df-sdom 5429 df-undef 5556 df-riota 5560 df-sup 5664 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 df-plp 6240 df-mp 6241 df-ltp 6242 df-plpr 6316 df-mpr 6317 df-enr 6318 df-nr 6319 df-plr 6320 df-mr 6321 df-ltr 6322 df-0r 6323 df-1r 6324 df-m1r 6325 df-c 6392 df-0 6393 df-1 6394 df-i 6395 df-r 6396 df-plus 6397 df-mul 6398 df-lt 6399 df-sub 6511 df-neg 6513 df-pnf 6654 df-mnf 6655 df-xr 6656 df-ltxr 6657 df-le 6658 df-div 6892 df-n 7108 df-2 7154 df-rp 7232 df-n0 7309 df-z 7345 df-ioo 7528 df-seq1 7721 df-exp 7812 df-sqr 7920 df-re 8001 df-im 8002 df-cj 8003 df-abs 8004