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

Metamath Proof Explorer

Theorem eliccelioc

Proof