elicc2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elicc2		Structured version Visualization version GIF version

Theorem elicc2 13542

Description: Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)

**Assertion**
Ref	Expression
elicc2	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))

**Proof of Theorem elicc2**
Step	Hyp	Ref	Expression
1		rexr 11355	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
2		rexr 11355	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
3		elicc1 13520	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
4	1, 2, 3	syl2an 608	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
5		mnfxr 11366	. . . . . . . 8 ⊢ -∞ ∈ ℝ^*
6	5	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ∈ ℝ^*)
7	1	ad2antrr 739	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ∈ ℝ^*)
8		simpr1 1213	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ^*)
9		mnflt 13252	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
10	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐴)
11		simpr2 1214	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ≤ 𝐶)
12	6, 7, 8, 10, 11	xrltletrd 13290	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐶)
13	2	ad2antlr 740	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 ∈ ℝ^*)
14		pnfxr 11363	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
15	14	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → +∞ ∈ ℝ^*)
16		simpr3 1215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ≤ 𝐵)
17		ltpnf 13249	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
18	17	ad2antlr 740	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 < +∞)
19	8, 13, 15, 16, 18	xrlelttrd 13289	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 < +∞)
20		xrrebnd 13298	. . . . . . 7 ⊢ (𝐶 ∈ ℝ^* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
21	8, 20	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
22	12, 19, 21	mpbir2and 726	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ)
23	22, 11, 16	3jca 1146	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))
24	23	ex 418	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
25		rexr 11355	. . . 4 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
26	25	3anim1i 1170	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))
27	24, 26	impbid1 228	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
28	4, 27	bitrd 282	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∈ wcel 2145 class class class wbr 5103 (class class class)co 7420 ℝcr 11199 +∞cpnf 11340 -∞cmnf 11341 ℝ^*cxr 11342 < clt 11343 ≤ cle 11344 [,]cicc 13479

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-pre-lttri 11274 ax-pre-lttrn 11275

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-po 5559 df-so 5560 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-icc 13483

This theorem is used by: elicc2i 13543 iccssre 13560 iccsupr 13573 iccneg 13603 iccsplit 13616 iccshftr 13617 iccshftl 13619 iccdil 13621 icccntr 13623 iccf1o 13627 supicc 13632 icco1 15707 iccntr 25141 icccmplem1 25142 icccmplem2 25143 icccmplem3 25144 reconnlem1 25146 reconnlem2 25147 cnmpopc 25249 icoopnst 25260 iocopnst 25261 cnheiborlem 25275 ivthlem2 25773 ivthlem3 25774 ivthicc 25779 evthicc2 25781 ovolficc 25789 ovolicc1 25837 ovolicc2lem2 25839 ovolicc2lem5 25842 ovolicopnf 25845 dyadmaxlem 25918 opnmbllem 25922 volsup2 25926 volcn 25927 mbfi1fseqlem6 26041 itgspliticc 26157 itgsplitioo 26158 ditgcl 26178 ditgswap 26179 ditgsplitlem 26180 ditgsplit 26181 dvlip 26313 dvlip2 26315 dveq0 26320 dvgt0lem1 26322 dvivthlem1 26328 dvne0 26331 dvcnvrelem1 26337 dvcnvrelem2 26338 dvcnvre 26339 dvfsumlem2 26347 ftc1lem1 26355 ftc1lem2 26356 ftc1a 26357 ftc1lem4 26359 ftc2 26364 ftc2ditglem 26365 itgsubstlem 26368 pserulm 26749 loglesqrt 27089 log2tlbnd 27273 ppisval 27431 chtleppi 27537 fsumvma2 27541 chpchtsum 27546 chpub 27547 rplogsumlem2 27812 chpdifbndlem1 27880 pntibndlem2a 27917 pntibndlem2 27918 pntlemj 27930 pntlem3 27936 pntleml 27938 resconn 36011 cvmliftlem10 36059 opnmbllem0 38574 ftc2nc 38620 areacirclem2 38627 areacirclem4 38629 areacirc 38631 isbnd3 38718 isbnd3b 38719 prdsbnd 38727 iccbnd 38774 intlewftc 43111 dvrelog2 43114 aks4d1p1p5 43125 eliccd 46515 eliccre 46516 iccshift 46529 iccsuble 46530 limcicciooub 46646 icccncfext 46896 itgsubsticc 46985 iblcncfioo 46987 itgiccshift 46989 itgperiod 46990 itgsbtaddcnst 46991 fourierdlem42 47158 fourierdlem54 47169 fourierdlem63 47178 fourierdlem65 47180 fourierdlem74 47189 fourierdlem75 47190 fourierdlem82 47197 fourierdlem93 47208 fourierdlem101 47216 fourierdlem104 47219 fourierdlem111 47226 reorelicc 49821

W3C validator