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 46463

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ w3a 1103 ∈ wcel 2145 class class class wbr 5103 (class class class)co 7412 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 (,]cioc 13458

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-iota 6487 df-fun 6533 df-fv 6539 df-ov 7415 df-oprab 7416 df-mpo 7417 df-xr 11328 df-ioc 13462

This theorem is used by: iocopn 46476 eliccelioc 46477 iccdificc 46495 ressiocsup 46510 iooiinioc 46512 preimaiocmnf 46516 xlimpnfvlem2 46791 ioccncflimc 46839 fourierdlem41 47102 fourierdlem46 47106 fourierdlem48 47108 fourierdlem49 47109 fourierdlem51 47111 fourierswlem 47184 smfsuplem1 47765

W3C validator