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 45526

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 13279	. . 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 2110 class class class wbr 5089 (class class class)co 7341 ℝ^*cxr 11137 < clt 11138 ≤ cle 11139 (,]cioc 13238

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pr 5368 ax-un 7663 ax-cnex 11054 ax-resscn 11055

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ral 3046 df-rex 3055 df-rab 3394 df-v 3436 df-sbc 3740 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-br 5090 df-opab 5152 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-iota 6433 df-fun 6479 df-fv 6485 df-ov 7344 df-oprab 7345 df-mpo 7346 df-xr 11142 df-ioc 13242

This theorem is referenced by: iocopn 45539 eliccelioc 45540 iccdificc 45558 ressiocsup 45573 iooiinioc 45575 preimaiocmnf 45579 xlimpnfvlem2 45854 ioccncflimc 45902 fourierdlem41 46165 fourierdlem46 46169 fourierdlem48 46171 fourierdlem49 46172 fourierdlem51 46174 fourierswlem 46247 smfsuplem1 46828

W3C validator