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	$⊢ φ \to A \in ℝ^{*}$
	eliccnelico.b	$⊢ φ \to B \in ℝ^{*}$
	eliccnelico.c	$⊢ φ \to C \in [A, B]$
	eliccnelico.nel	$⊢ φ \to \neg C \in [A, B)$
Assertion	eliccnelico	$⊢ φ \to C = B$

Proof

Step	Hyp	Ref	Expression
1		eliccnelico.1	$⊢ φ \to A \in ℝ^{*}$
2		eliccnelico.b	$⊢ φ \to B \in ℝ^{*}$
3		eliccnelico.c	$⊢ φ \to C \in [A, B]$
4		eliccnelico.nel	$⊢ φ \to \neg C \in [A, B)$
5		eliccxr	$⊢ C \in [A, B] \to C \in ℝ^{*}$
6	3 5	syl	$⊢ φ \to C \in ℝ^{*}$
7		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in [A, B]) \to C \leq B$
8	1 2 3 7	syl3anc	$⊢ φ \to C \leq B$
9	1	adantr	$⊢ (φ \land \neg B \leq C) \to A \in ℝ^{*}$
10	2	adantr	$⊢ (φ \land \neg B \leq C) \to B \in ℝ^{*}$
11	6	adantr	$⊢ (φ \land \neg B \leq C) \to C \in ℝ^{*}$
12		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in [A, B]) \to A \leq C$
13	1 2 3 12	syl3anc	$⊢ φ \to A \leq C$
14	13	adantr	$⊢ (φ \land \neg B \leq C) \to A \leq C$
15		simpr	$⊢ (φ \land \neg B \leq C) \to \neg B \leq C$
16		xrltnle	$⊢ (C \in ℝ^{} \land B \in ℝ^{}) \to (C < B \leftrightarrow \neg B \leq C)$
17	6 2 16	syl2anc	$⊢ φ \to (C < B \leftrightarrow \neg B \leq C)$
18	17	adantr	$⊢ (φ \land \neg B \leq C) \to (C < B \leftrightarrow \neg B \leq C)$
19	15 18	mpbird	$⊢ (φ \land \neg B \leq C) \to C < B$
20	9 10 11 14 19	elicod	$⊢ (φ \land \neg B \leq C) \to C \in [A, B)$
21	4	adantr	$⊢ (φ \land \neg B \leq C) \to \neg C \in [A, B)$
22	20 21	condan	$⊢ φ \to B \leq C$
23	6 2 8 22	xrletrid	$⊢ φ \to C = B$

Metamath Proof Explorer

Theorem eliccnelico

Proof