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 45966

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 13335	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
7	4, 5, 6	syl2anc 591	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
8	1, 2, 3, 7	mpbir3and 1350	1 ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ w3a 1093 ∈ wcel 2121 class class class wbr 5075 (class class class)co 7360 ℝ^*cxr 11173 < clt 11174 ≤ cle 11175 (,]cioc 13294

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5221 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ral 3056 df-rex 3066 df-rab 3394 df-v 3435 df-sbc 3726 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-br 5076 df-opab 5138 df-id 5516 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-iota 6445 df-fun 6491 df-fv 6497 df-ov 7363 df-oprab 7364 df-mpo 7365 df-xr 11178 df-ioc 13298

This theorem is referenced by: iocopn 45979 eliccelioc 45980 iccdificc 45998 ressiocsup 46013 iooiinioc 46015 preimaiocmnf 46019 xlimpnfvlem2 46294 ioccncflimc 46342 fourierdlem41 46605 fourierdlem46 46609 fourierdlem48 46611 fourierdlem49 46612 fourierdlem51 46614 fourierswlem 46687 smfsuplem1 47268

W3C validator