elii2

Description: Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014)

		Ref	Expression
	Assertion	elii2	$⊢ (X \in [0, 1] \land \neg X \leq \frac{1}{2}) \to X \in [\frac{1}{2}, 1]$

Step	Hyp	Ref	Expression
1		elicc01	$⊢ X \in [0, 1] \leftrightarrow (X \in ℝ \land 0 \leq X \land X \leq 1)$
2	1	simp1bi	$⊢ X \in [0, 1] \to X \in ℝ$
3	2	adantr	$⊢ (X \in [0, 1] \land \neg X \leq \frac{1}{2}) \to X \in ℝ$
4		halfre	$⊢ \frac{1}{2} \in ℝ$
5		letric	$⊢ (X \in ℝ \land \frac{1}{2} \in ℝ) \to (X \leq \frac{1}{2} \lor \frac{1}{2} \leq X)$
6	2 4 5	sylancl	$⊢ X \in [0, 1] \to (X \leq \frac{1}{2} \lor \frac{1}{2} \leq X)$
7	6	orcanai	$⊢ (X \in [0, 1] \land \neg X \leq \frac{1}{2}) \to \frac{1}{2} \leq X$
8	1	simp3bi	$⊢ X \in [0, 1] \to X \leq 1$
9	8	adantr	$⊢ (X \in [0, 1] \land \neg X \leq \frac{1}{2}) \to X \leq 1$
10		1re	$⊢ 1 \in ℝ$
11	4 10	elicc2i	$⊢ X \in [\frac{1}{2}, 1] \leftrightarrow (X \in ℝ \land \frac{1}{2} \leq X \land X \leq 1)$
12	3 7 9 11	syl3anbrc	$⊢ (X \in [0, 1] \land \neg X \leq \frac{1}{2}) \to X \in [\frac{1}{2}, 1]$

Metamath Proof Explorer