Metamath Proof Explorer

Theorem eliccelioc

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

Ref Expression
Hypotheses eliccelioc.a ⊢ φ → A ∈ ℝ
eliccelioc.b ⊢ φ → B ∈ ℝ
eliccelioc.c ⊢ φ → C ∈ ℝ *
Assertion eliccelioc ⊢ φ → C ∈ A B ↔ C ∈ A B ∧ C ≠ A

Proof

Step Hyp Ref Expression
1 eliccelioc.a ⊢ φ → A ∈ ℝ
2 eliccelioc.b ⊢ φ → B ∈ ℝ
3 eliccelioc.c ⊢ φ → C ∈ ℝ *
4 iocssicc ⊢ A B ⊆ A B
5 4 sseli ⊢ C ∈ A B → C ∈ A B
6 5 adantl ⊢ φ ∧ C ∈ A B → C ∈ A B
7 1 adantr ⊢ φ ∧ C ∈ A B → A ∈ ℝ
8 1 rexrd ⊢ φ → A ∈ ℝ *
9 8 adantr ⊢ φ ∧ C ∈ A B → A ∈ ℝ *
10 2 adantr ⊢ φ ∧ C ∈ A B → B ∈ ℝ
11 10 rexrd ⊢ φ ∧ C ∈ A B → B ∈ ℝ *
12 simpr ⊢ φ ∧ C ∈ A B → C ∈ A B
13 iocgtlb ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → A < C
14 9 11 12 13 syl3anc ⊢ φ ∧ C ∈ A B → A < C
15 7 14 gtned ⊢ φ ∧ C ∈ A B → C ≠ A
16 6 15 jca ⊢ φ ∧ C ∈ A B → C ∈ A B ∧ C ≠ A
17 8 adantr ⊢ φ ∧ C ∈ A B ∧ C ≠ A → A ∈ ℝ *
18 2 rexrd ⊢ φ → B ∈ ℝ *
19 18 adantr ⊢ φ ∧ C ∈ A B ∧ C ≠ A → B ∈ ℝ *
20 3 adantr ⊢ φ ∧ C ∈ A B ∧ C ≠ A → C ∈ ℝ *
21 1 adantr ⊢ φ ∧ C ∈ A B ∧ C ≠ A → A ∈ ℝ
22 1 2 iccssred ⊢ φ → A B ⊆ ℝ
23 22 sselda ⊢ φ ∧ C ∈ A B → C ∈ ℝ
24 23 adantrr ⊢ φ ∧ C ∈ A B ∧ C ≠ A → C ∈ ℝ
25 8 adantr ⊢ φ ∧ C ∈ A B → A ∈ ℝ *
26 18 adantr ⊢ φ ∧ C ∈ A B → B ∈ ℝ *
27 simpr ⊢ φ ∧ C ∈ A B → C ∈ A B
28 iccgelb ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → A ≤ C
29 25 26 27 28 syl3anc ⊢ φ ∧ C ∈ A B → A ≤ C
30 29 adantrr ⊢ φ ∧ C ∈ A B ∧ C ≠ A → A ≤ C
31 simprr ⊢ φ ∧ C ∈ A B ∧ C ≠ A → C ≠ A
32 21 24 30 31 leneltd ⊢ φ ∧ C ∈ A B ∧ C ≠ A → A < C
33 iccleub ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → C ≤ B
34 25 26 27 33 syl3anc ⊢ φ ∧ C ∈ A B → C ≤ B
35 34 adantrr ⊢ φ ∧ C ∈ A B ∧ C ≠ A → C ≤ B
36 17 19 20 32 35 eliocd ⊢ φ ∧ C ∈ A B ∧ C ≠ A → C ∈ A B
37 16 36 impbida ⊢ φ → C ∈ A B ↔ C ∈ A B ∧ C ≠ A