Metamath Proof Explorer

Theorem gtnelicc

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

		Ref	Expression
	Hypotheses	gtnelicc.a	$⊢ φ \to A \in ℝ^{*}$
		gtnelicc.b	$⊢ φ \to B \in ℝ$
		gtnelicc.c	$⊢ φ \to C \in ℝ^{*}$
		gtnelicc.bltc	$⊢ φ \to B < C$
	Assertion	gtnelicc	$⊢ φ \to \neg C \in [A, B]$

Proof

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