eliccnelico

Description: An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	eliccnelico.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
	eliccnelico.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
	eliccnelico.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
	eliccnelico.nel	⊢ ( 𝜑 → ¬ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) )
Assertion	eliccnelico	⊢ ( 𝜑 → 𝐶 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eliccnelico.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
2		eliccnelico.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
3		eliccnelico.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
4		eliccnelico.nel	⊢ ( 𝜑 → ¬ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) )
5		eliccxr	⊢ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) → 𝐶 ∈ ℝ^* )
6	3 5	syl	⊢ ( 𝜑 → 𝐶 ∈ ℝ^* )
7		iccleub	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ≤ 𝐵 )
8	1 2 3 7	syl3anc	⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
9	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → 𝐴 ∈ ℝ^* )
10	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → 𝐵 ∈ ℝ^* )
11	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → 𝐶 ∈ ℝ^* )
12		iccgelb	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝐶 )
13	1 2 3 12	syl3anc	⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
14	13	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → 𝐴 ≤ 𝐶 )
15		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → ¬ 𝐵 ≤ 𝐶 )
16		xrltnle	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐶 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐶 ) )
17	6 2 16	syl2anc	⊢ ( 𝜑 → ( 𝐶 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐶 ) )
18	17	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → ( 𝐶 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐶 ) )
19	15 18	mpbird	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → 𝐶 < 𝐵 )
20	9 10 11 14 19	elicod	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → 𝐶 ∈ ( 𝐴 [,) 𝐵 ) )
21	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐶 ) → ¬ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) )
22	20 21	condan	⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
23	6 2 8 22	xrletrid	⊢ ( 𝜑 → 𝐶 = 𝐵 )

Metamath Proof Explorer

Theorem eliccnelico

Proof