Metamath Proof Explorer

Theorem xrgtnelicc

Description: A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021)

		Ref	Expression
	Hypotheses	xrgtnelicc.1	$⊢ φ \to A \in ℝ^{*}$
		xrgtnelicc.2	$⊢ φ \to B \in ℝ^{*}$
		xrgtnelicc.3	$⊢ φ \to C \in ℝ^{*}$
		xrgtnelicc.4	$⊢ φ \to B < C$
	Assertion	xrgtnelicc	$⊢ φ \to \neg C \in [A, B]$

Proof

Step	Hyp	Ref	Expression
1		xrgtnelicc.1	$⊢ φ \to A \in ℝ^{*}$
2		xrgtnelicc.2	$⊢ φ \to B \in ℝ^{*}$
3		xrgtnelicc.3	$⊢ φ \to C \in ℝ^{*}$
4		xrgtnelicc.4	$⊢ φ \to B < C$
5		xrltnle	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (B < C \leftrightarrow \neg C \leq B)$
6	2 3 5	syl2anc	$⊢ φ \to (B < C \leftrightarrow \neg C \leq B)$
7	4 6	mpbid	$⊢ φ \to \neg C \leq B$
8	7	intnand	$⊢ φ \to \neg (A \leq C \land C \leq B)$
9		elicc4	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (C \in [A, B] \leftrightarrow (A \leq C \land C \leq B))$
10	1 2 3 9	syl3anc	$⊢ φ \to (C \in [A, B] \leftrightarrow (A \leq C \land C \leq B))$
11	8 10	mtbird	$⊢ φ \to \neg C \in [A, B]$