eliocd - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > eliocd		Structured version Visualization version GIF version

Theorem eliocd 45516

Description: Membership in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
eliocd.a	⊢ (𝜑 → 𝐴 ∈ ℝ^*)
eliocd.b	⊢ (𝜑 → 𝐵 ∈ ℝ^*)
eliocd.c	⊢ (𝜑 → 𝐶 ∈ ℝ^*)
eliocd.altc	⊢ (𝜑 → 𝐴 < 𝐶)
eliocd.cleb	⊢ (𝜑 → 𝐶 ≤ 𝐵)

**Assertion**
Ref	Expression
eliocd	⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵))

**Proof of Theorem eliocd**
Step	Hyp	Ref	Expression
1		eliocd.c	. 2 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
2		eliocd.altc	. 2 ⊢ (𝜑 → 𝐴 < 𝐶)
3		eliocd.cleb	. 2 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
4		eliocd.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
5		eliocd.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
6		elioc1 13409	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
7	4, 5, 6	syl2anc 584	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
8	1, 2, 3, 7	mpbir3and 1343	1 ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1086 ∈ wcel 2109 class class class wbr 5124 (class class class)co 7410 ℝ^*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-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 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-ral 3053 df-rex 3062 df-rab 3421 df-v 3466 df-sbc 3771 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-id 5553 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-iota 6489 df-fun 6538 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-xr 11278 df-ioc 13372

This theorem is referenced by: iocopn 45529 eliccelioc 45530 iccdificc 45548 ressiocsup 45563 iooiinioc 45565 preimaiocmnf 45569 xlimpnfvlem2 45846 ioccncflimc 45894 fourierdlem41 46157 fourierdlem46 46161 fourierdlem48 46163 fourierdlem49 46164 fourierdlem51 46166 fourierswlem 46239 smfsuplem1 46820

W3C validator