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∈012↔X∈01∧X≤12

Proof

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