# Metamath Proof Explorer

## Theorem elii1

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

Ref Expression
Assertion elii1 ${⊢}{X}\in \left[0,\frac{1}{2}\right]↔\left({X}\in \left[0,1\right]\wedge {X}\le \frac{1}{2}\right)$

### Proof

Step Hyp Ref Expression
1 0re ${⊢}0\in ℝ$
2 halfre ${⊢}\frac{1}{2}\in ℝ$
3 1 2 elicc2i ${⊢}{X}\in \left[0,\frac{1}{2}\right]↔\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le \frac{1}{2}\right)$
4 3 simp1bi ${⊢}{X}\in \left[0,\frac{1}{2}\right]\to {X}\in ℝ$
5 2 a1i ${⊢}{X}\in \left[0,\frac{1}{2}\right]\to \frac{1}{2}\in ℝ$
6 1re ${⊢}1\in ℝ$
7 6 a1i ${⊢}{X}\in \left[0,\frac{1}{2}\right]\to 1\in ℝ$
8 3 simp3bi ${⊢}{X}\in \left[0,\frac{1}{2}\right]\to {X}\le \frac{1}{2}$
9 halflt1 ${⊢}\frac{1}{2}<1$
10 2 6 9 ltleii ${⊢}\frac{1}{2}\le 1$
11 10 a1i ${⊢}{X}\in \left[0,\frac{1}{2}\right]\to \frac{1}{2}\le 1$
12 4 5 7 8 11 letrd ${⊢}{X}\in \left[0,\frac{1}{2}\right]\to {X}\le 1$
13 12 pm4.71ri ${⊢}{X}\in \left[0,\frac{1}{2}\right]↔\left({X}\le 1\wedge {X}\in \left[0,\frac{1}{2}\right]\right)$
14 ancom ${⊢}\left({X}\le 1\wedge {X}\in \left[0,\frac{1}{2}\right]\right)↔\left({X}\in \left[0,\frac{1}{2}\right]\wedge {X}\le 1\right)$
15 an32 ${⊢}\left(\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge {X}\le \frac{1}{2}\right)\wedge {X}\le 1\right)↔\left(\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge {X}\le 1\right)\wedge {X}\le \frac{1}{2}\right)$
16 df-3an ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le \frac{1}{2}\right)↔\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge {X}\le \frac{1}{2}\right)$
17 3 16 bitri ${⊢}{X}\in \left[0,\frac{1}{2}\right]↔\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge {X}\le \frac{1}{2}\right)$
18 17 anbi1i ${⊢}\left({X}\in \left[0,\frac{1}{2}\right]\wedge {X}\le 1\right)↔\left(\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge {X}\le \frac{1}{2}\right)\wedge {X}\le 1\right)$
19 1 6 elicc2i ${⊢}{X}\in \left[0,1\right]↔\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)$
20 df-3an ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)↔\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge {X}\le 1\right)$
21 19 20 bitri ${⊢}{X}\in \left[0,1\right]↔\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge {X}\le 1\right)$
22 21 anbi1i ${⊢}\left({X}\in \left[0,1\right]\wedge {X}\le \frac{1}{2}\right)↔\left(\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge {X}\le 1\right)\wedge {X}\le \frac{1}{2}\right)$
23 15 18 22 3bitr4i ${⊢}\left({X}\in \left[0,\frac{1}{2}\right]\wedge {X}\le 1\right)↔\left({X}\in \left[0,1\right]\wedge {X}\le \frac{1}{2}\right)$
24 14 23 bitri ${⊢}\left({X}\le 1\wedge {X}\in \left[0,\frac{1}{2}\right]\right)↔\left({X}\in \left[0,1\right]\wedge {X}\le \frac{1}{2}\right)$
25 13 24 bitri ${⊢}{X}\in \left[0,\frac{1}{2}\right]↔\left({X}\in \left[0,1\right]\wedge {X}\le \frac{1}{2}\right)$