Metamath Proof Explorer

Theorem elii1

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

Ref Expression
Assertion elii1 ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) )

Proof

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