This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
eliccelioc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
eliccelioc.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
Assertion eliccelioc ( 𝜑 → ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ≠ 𝐴 ) ) )

Proof

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