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 45952

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1087 ∈ wcel 2114 class class class wbr 5086 (class class class)co 7358 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 (,]cioc 13288

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-sbc 3730 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-iota 6446 df-fun 6492 df-fv 6498 df-ov 7361 df-oprab 7362 df-mpo 7363 df-xr 11172 df-ioc 13292

This theorem is referenced by: iocopn 45965 eliccelioc 45966 iccdificc 45984 ressiocsup 45999 iooiinioc 46001 preimaiocmnf 46005 xlimpnfvlem2 46280 ioccncflimc 46328 fourierdlem41 46591 fourierdlem46 46595 fourierdlem48 46597 fourierdlem49 46598 fourierdlem51 46600 fourierswlem 46673 smfsuplem1 47254

W3C validator