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 ( 𝜑 → ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶𝐴 ) ) )