elioc2 - Metamath Proof Explorer

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

Theorem elioc2 13466

Description: Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)

**Assertion**
Ref	Expression
elioc2	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))

**Proof of Theorem elioc2**
Step	Hyp	Ref	Expression
1		rexr 11283	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
2		elioc1 13444	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
3	1, 2	sylan2 605	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
4		mnfxr 11294	. . . . . . . 8 ⊢ -∞ ∈ ℝ^*
5	4	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ∈ ℝ^*)
6		simpll 779	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ∈ ℝ^*)
7		simpr1 1213	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ^*)
8		mnfle 13190	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → -∞ ≤ 𝐴)
9	8	ad2antrr 739	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ≤ 𝐴)
10		simpr2 1214	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 < 𝐶)
11	5, 6, 7, 9, 10	xrlelttrd 13215	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐶)
12	1	ad2antlr 740	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 ∈ ℝ^*)
13		pnfxr 11291	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
14	13	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → +∞ ∈ ℝ^*)
15		simpr3 1215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ≤ 𝐵)
16		ltpnf 13175	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
17	16	ad2antlr 740	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 < +∞)
18	7, 12, 14, 15, 17	xrlelttrd 13215	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 < +∞)
19		xrrebnd 13224	. . . . . . 7 ⊢ (𝐶 ∈ ℝ^* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
20	7, 19	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
21	11, 18, 20	mpbir2and 726	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ)
22	21, 10, 15	3jca 1146	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵))
23	22	ex 418	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
24		rexr 11283	. . . 4 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
25	24	3anim1i 1170	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵))
26	23, 25	impbid1 228	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
27	3, 26	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 5107 (class class class)co 7417 ℝcr 11127 +∞cpnf 11268 -∞cmnf 11269 ℝ^*cxr 11270 < clt 11271 ≤ cle 11272 (,]cioc 13403

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 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-pre-lttri 11202 ax-pre-lttrn 11203

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 df-po 5567 df-so 5568 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7420 df-oprab 7421 df-mpo 7422 df-er 8700 df-en 8957 df-dom 8958 df-sdom 8959 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-ioc 13407

This theorem is used by: iocssre 13484 ef01bndlem 16278 sin01bnd 16279 cos01bnd 16280 cos1bnd 16281 sinltx 16283 sin01gt0 16284 cos01gt0 16285 sin02gt0 16286 sincos1sgn 16287 sincos2sgn 16288 icoopnst 25173 iocopnst 25174 ismbf3d 25888 aaliou3lem2 26586 aaliou3lem3 26587 pilem2 26695 sinhalfpilem 26708 sincosq1lem 26742 coseq0negpitopi 26748 tangtx 26750 sincos4thpi 26758 efif1olem1 26787 efif1olem2 26788 efif1o 26791 efifo 26792 ellogrn 26804 logimclad 26817 ellogdm 26884 logdmnrp 26886 dvloglem 26893 dvlog2lem 26897 asinneg 27131 atans2 27176 ressatans 27179 abvcxp 27859 ostth2 27881 xrge0iifcv 34452 xrge0iifiso 34453 xrge0iifhom 34455 sinccvglem 36259 bj-pinftyccb 37981 bj-pinftynminfty 37987 dvasin 38461 areacirclem4 38468 gtnelioc 46329 limcicciooub 46473 fourierdlem4 46947 fourierdlem26 46969 fourierdlem33 46976 fourierdlem37 46980 fourierdlem65 47007 fourierdlem79 47021 fouriersw 47067 eenglngeehlnmlem1 49675 eenglngeehlnmlem2 49676 io1ii 49855 sepfsepc 49862

W3C validator