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 13372

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 11220	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
2		rexr 11220	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
3		elicc1 13350	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
5		mnfxr 11231	. . . . . . . 8 ⊢ -∞ ∈ ℝ^*
6	5	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ∈ ℝ^*)
7	1	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ∈ ℝ^*)
8		simpr1 1195	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ^*)
9		mnflt 13083	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
10	9	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐴)
11		simpr2 1196	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ≤ 𝐶)
12	6, 7, 8, 10, 11	xrltletrd 13121	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐶)
13	2	ad2antlr 727	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 ∈ ℝ^*)
14		pnfxr 11228	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
15	14	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → +∞ ∈ ℝ^*)
16		simpr3 1197	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ≤ 𝐵)
17		ltpnf 13080	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
18	17	ad2antlr 727	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 < +∞)
19	8, 13, 15, 16, 18	xrlelttrd 13120	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 < +∞)
20		xrrebnd 13128	. . . . . . 7 ⊢ (𝐶 ∈ ℝ^* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
21	8, 20	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
22	12, 19, 21	mpbir2and 713	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ)
23	22, 11, 16	3jca 1128	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))
24	23	ex 412	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
25		rexr 11220	. . . 4 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
26	25	3anim1i 1152	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))
27	24, 26	impbid1 225	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
28	4, 27	bitrd 279	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∈ wcel 2109 class class class wbr 5107 (class class class)co 7387 ℝcr 11067 +∞cpnf 11205 -∞cmnf 11206 ℝ^*cxr 11207 < clt 11208 ≤ cle 11209 [,]cicc 13309

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-pre-lttri 11142 ax-pre-lttrn 11143

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-br 5108 df-opab 5170 df-mpt 5189 df-id 5533 df-po 5546 df-so 5547 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-ov 7390 df-oprab 7391 df-mpo 7392 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-icc 13313

This theorem is referenced by: elicc2i 13373 iccssre 13390 iccsupr 13403 iccneg 13433 iccsplit 13446 iccshftr 13447 iccshftl 13449 iccdil 13451 icccntr 13453 iccf1o 13457 supicc 13462 icco1 15506 iccntr 24710 icccmplem1 24711 icccmplem2 24712 icccmplem3 24713 reconnlem1 24715 reconnlem2 24716 cnmpopc 24822 icoopnst 24836 iocopnst 24837 cnheiborlem 24853 ivthlem2 25353 ivthlem3 25354 ivthicc 25359 evthicc2 25361 ovolficc 25369 ovolicc1 25417 ovolicc2lem2 25419 ovolicc2lem5 25422 ovolicopnf 25425 dyadmaxlem 25498 opnmbllem 25502 volsup2 25506 volcn 25507 mbfi1fseqlem6 25621 itgspliticc 25738 itgsplitioo 25739 ditgcl 25759 ditgswap 25760 ditgsplitlem 25761 ditgsplit 25762 dvlip 25898 dvlip2 25900 dveq0 25905 dvgt0lem1 25907 dvivthlem1 25913 dvne0 25916 dvcnvrelem1 25922 dvcnvrelem2 25923 dvcnvre 25924 dvfsumlem2 25933 dvfsumlem2OLD 25934 ftc1lem1 25942 ftc1lem2 25943 ftc1a 25944 ftc1lem4 25946 ftc2 25951 ftc2ditglem 25952 itgsubstlem 25955 pserulm 26331 loglesqrt 26671 log2tlbnd 26855 ppisval 27014 chtleppi 27121 fsumvma2 27125 chpchtsum 27130 chpub 27131 rplogsumlem2 27396 chpdifbndlem1 27464 pntibndlem2a 27501 pntibndlem2 27502 pntlemj 27514 pntlem3 27520 pntleml 27522 resconn 35233 cvmliftlem10 35281 opnmbllem0 37650 ftc2nc 37696 areacirclem2 37703 areacirclem4 37705 areacirc 37707 isbnd3 37778 isbnd3b 37779 prdsbnd 37787 iccbnd 37834 intlewftc 42049 dvrelog2 42052 aks4d1p1p5 42063 eliccd 45502 eliccre 45503 iccshift 45516 iccsuble 45517 limcicciooub 45635 icccncfext 45885 itgsubsticc 45974 iblcncfioo 45976 itgiccshift 45978 itgperiod 45979 itgsbtaddcnst 45980 fourierdlem42 46147 fourierdlem54 46158 fourierdlem63 46167 fourierdlem65 46169 fourierdlem74 46178 fourierdlem75 46179 fourierdlem82 46186 fourierdlem93 46197 fourierdlem101 46205 fourierdlem104 46208 fourierdlem111 46215 reorelicc 48699

W3C validator