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 13431

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 11286	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
2		elioc1 13409	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
3	1, 2	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
4		mnfxr 11297	. . . . . . . 8 ⊢ -∞ ∈ ℝ^*
5	4	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ∈ ℝ^*)
6		simpll 766	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ∈ ℝ^*)
7		simpr1 1195	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ^*)
8		mnfle 13156	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → -∞ ≤ 𝐴)
9	8	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ≤ 𝐴)
10		simpr2 1196	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 < 𝐶)
11	5, 6, 7, 9, 10	xrlelttrd 13181	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐶)
12	1	ad2antlr 727	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 ∈ ℝ^*)
13		pnfxr 11294	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
14	13	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → +∞ ∈ ℝ^*)
15		simpr3 1197	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ≤ 𝐵)
16		ltpnf 13141	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
17	16	ad2antlr 727	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 < +∞)
18	7, 12, 14, 15, 17	xrlelttrd 13181	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 < +∞)
19		xrrebnd 13189	. . . . . . 7 ⊢ (𝐶 ∈ ℝ^* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
20	7, 19	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
21	11, 18, 20	mpbir2and 713	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ)
22	21, 10, 15	3jca 1128	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵))
23	22	ex 412	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
24		rexr 11286	. . . 4 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
25	24	3anim1i 1152	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵))
26	23, 25	impbid1 225	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
27	3, 26	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 5124 (class class class)co 7410 ℝcr 11133 +∞cpnf 11271 -∞cmnf 11272 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 (,]cioc 13368

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 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-pre-lttri 11208 ax-pre-lttrn 11209

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 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-po 5566 df-so 5567 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 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-er 8724 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-ioc 13372

This theorem is referenced by: iocssre 13449 ef01bndlem 16207 sin01bnd 16208 cos01bnd 16209 cos1bnd 16210 sinltx 16212 sin01gt0 16213 cos01gt0 16214 sin02gt0 16215 sincos1sgn 16216 sincos2sgn 16217 icoopnst 24892 iocopnst 24893 ismbf3d 25612 aaliou3lem2 26308 aaliou3lem3 26309 pilem2 26419 sinhalfpilem 26429 sincosq1lem 26463 coseq0negpitopi 26469 tangtx 26471 sincos4thpi 26479 efif1olem1 26508 efif1olem2 26509 efif1o 26512 efifo 26513 ellogrn 26525 logimclad 26538 ellogdm 26605 logdmnrp 26607 dvloglem 26614 dvlog2lem 26618 asinneg 26853 atans2 26898 ressatans 26901 abvcxp 27583 ostth2 27605 xrge0iifcv 33970 xrge0iifiso 33971 xrge0iifhom 33973 sinccvglem 35699 bj-pinftyccb 37244 bj-pinftynminfty 37250 dvasin 37733 areacirclem4 37740 gtnelioc 45487 limcicciooub 45633 fourierdlem4 46107 fourierdlem26 46129 fourierdlem33 46136 fourierdlem37 46140 fourierdlem65 46167 fourierdlem79 46181 fouriersw 46227 eenglngeehlnmlem1 48684 eenglngeehlnmlem2 48685 io1ii 48862 sepfsepc 48869

W3C validator