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 13570

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 11385	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
2		elioc1 13548	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
3	1, 2	sylan2 605	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
4		mnfxr 11396	. . . . . . . 8 ⊢ -∞ ∈ ℝ^*
5	4	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ∈ ℝ^*)
6		simpll 779	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ∈ ℝ^*)
7		simpr1 1213	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ^*)
8		mnfle 13294	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → -∞ ≤ 𝐴)
9	8	ad2antrr 739	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ≤ 𝐴)
10		simpr2 1214	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 < 𝐶)
11	5, 6, 7, 9, 10	xrlelttrd 13319	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐶)
12	1	ad2antlr 740	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 ∈ ℝ^*)
13		pnfxr 11393	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
14	13	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → +∞ ∈ ℝ^*)
15		simpr3 1215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ≤ 𝐵)
16		ltpnf 13279	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
17	16	ad2antlr 740	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 < +∞)
18	7, 12, 14, 15, 17	xrlelttrd 13319	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 < +∞)
19		xrrebnd 13328	. . . . . . 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 11385	. . . 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 2147 class class class wbr 5106 (class class class)co 7446 ℝcr 11229 +∞cpnf 11370 -∞cmnf 11371 ℝ^*cxr 11372 < clt 11373 ≤ cle 11374 (,]cioc 13507

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-pre-lttri 11304 ax-pre-lttrn 11305

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-br 5107 df-opab 5172 df-mpt 5191 df-id 5551 df-po 5564 df-so 5565 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7449 df-oprab 7450 df-mpo 7451 df-er 8748 df-en 9005 df-dom 9006 df-sdom 9007 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-ioc 13511

This theorem is used by: iocssre 13588 ef01bndlem 16384 sin01bnd 16385 cos01bnd 16386 cos1bnd 16387 sinltx 16389 sin01gt0 16390 cos01gt0 16391 sin02gt0 16392 sincos1sgn 16393 sincos2sgn 16394 icoopnst 25293 iocopnst 25294 ismbf3d 26008 aaliou3lem2 26703 aaliou3lem3 26704 pilem2 26812 sinhalfpilem 26825 sincosq1lem 26859 coseq0negpitopi 26865 tangtx 26867 sincos4thpi 26875 efif1olem1 26903 efif1olem2 26904 efif1o 26907 efifo 26908 ellogrn 26920 logimclad 26933 ellogdm 27000 logdmnrp 27002 dvloglem 27009 dvlog2lem 27013 asinneg 27247 atans2 27292 ressatans 27295 abvcxp 27975 ostth2 27997 xrge0iifcv 34649 xrge0iifiso 34650 xrge0iifhom 34652 sinccvglem 36617 bj-pinftyccb 38347 bj-pinftynminfty 38353 dvasin 38827 areacirclem4 38834 gtnelioc 46718 limcicciooub 46862 fourierdlem4 47336 fourierdlem26 47358 fourierdlem33 47365 fourierdlem37 47369 fourierdlem65 47396 fourierdlem79 47410 fouriersw 47456 eenglngeehlnmlem1 50065 eenglngeehlnmlem2 50066 io1ii 50250 sepfsepc 50257

W3C validator