Metamath Proof Explorer

Theorem gtnelioc

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

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

Proof

Step	Hyp	Ref	Expression
1		gtnelioc.a	$⊢ φ \to A \in ℝ^{*}$
2		gtnelioc.b	$⊢ φ \to B \in ℝ$
3		gtnelioc.c	$⊢ φ \to C \in ℝ^{*}$
4		gtnelioc.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	intn3an3d	$⊢ φ \to \neg (C \in ℝ \land A < C \land C \leq B)$
10		elioc2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (C \in (A, B] \leftrightarrow (C \in ℝ \land A < C \land C \leq B))$
11	1 2 10	syl2anc	$⊢ φ \to (C \in (A, B] \leftrightarrow (C \in ℝ \land A < C \land C \leq B))$
12	9 11	mtbird	$⊢ φ \to \neg C \in (A, B]$