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 ∈ 0 1 2 ↔ X ∈ 0 1 ∧ X ≤ 1 2

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 halfre ⊢ 1 2 ∈ ℝ
3 1 2 elicc2i ⊢ X ∈ 0 1 2 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 2
4 3 simp1bi ⊢ X ∈ 0 1 2 → X ∈ ℝ
5 2 a1i ⊢ X ∈ 0 1 2 → 1 2 ∈ ℝ
6 1re ⊢ 1 ∈ ℝ
7 6 a1i ⊢ X ∈ 0 1 2 → 1 ∈ ℝ
8 3 simp3bi ⊢ X ∈ 0 1 2 → X ≤ 1 2
9 halflt1 ⊢ 1 2 < 1
10 2 6 9 ltleii ⊢ 1 2 ≤ 1
11 10 a1i ⊢ X ∈ 0 1 2 → 1 2 ≤ 1
12 4 5 7 8 11 letrd ⊢ X ∈ 0 1 2 → X ≤ 1
13 12 pm4.71ri ⊢ X ∈ 0 1 2 ↔ X ≤ 1 ∧ X ∈ 0 1 2
14 ancom ⊢ X ≤ 1 ∧ X ∈ 0 1 2 ↔ X ∈ 0 1 2 ∧ X ≤ 1
15 an32 ⊢ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 2 ∧ X ≤ 1 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 ∧ X ≤ 1 2
16 df-3an ⊢ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 2 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 2
17 3 16 bitri ⊢ X ∈ 0 1 2 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 2
18 17 anbi1i ⊢ X ∈ 0 1 2 ∧ X ≤ 1 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 2 ∧ X ≤ 1
19 1 6 elicc2i ⊢ X ∈ 0 1 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1
20 df-3an ⊢ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1
21 19 20 bitri ⊢ X ∈ 0 1 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1
22 21 anbi1i ⊢ X ∈ 0 1 ∧ X ≤ 1 2 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1 ∧ X ≤ 1 2
23 15 18 22 3bitr4i ⊢ X ∈ 0 1 2 ∧ X ≤ 1 ↔ X ∈ 0 1 ∧ X ≤ 1 2
24 14 23 bitri ⊢ X ≤ 1 ∧ X ∈ 0 1 2 ↔ X ∈ 0 1 ∧ X ≤ 1 2
25 13 24 bitri ⊢ X ∈ 0 1 2 ↔ X ∈ 0 1 ∧ X ≤ 1 2