This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elii2

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

Ref Expression
Assertion elii2 ⊢ X ∈ 0 1 ∧ ¬ X ≤ 1 2 → X ∈ 1 2 1

Proof

Step Hyp Ref Expression
1 elicc01 ⊢ X ∈ 0 1 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1
2 1 simp1bi ⊢ X ∈ 0 1 → X ∈ ℝ
3 2 adantr ⊢ X ∈ 0 1 ∧ ¬ X ≤ 1 2 → X ∈ ℝ
4 halfre ⊢ 1 2 ∈ ℝ
5 letric ⊢ X ∈ ℝ ∧ 1 2 ∈ ℝ → X ≤ 1 2 ∨ 1 2 ≤ X
6 2 4 5 sylancl ⊢ X ∈ 0 1 → X ≤ 1 2 ∨ 1 2 ≤ X
7 6 orcanai ⊢ X ∈ 0 1 ∧ ¬ X ≤ 1 2 → 1 2 ≤ X
8 1 simp3bi ⊢ X ∈ 0 1 → X ≤ 1
9 8 adantr ⊢ X ∈ 0 1 ∧ ¬ X ≤ 1 2 → X ≤ 1
10 1re ⊢ 1 ∈ ℝ
11 4 10 elicc2i ⊢ X ∈ 1 2 1 ↔ X ∈ ℝ ∧ 1 2 ≤ X ∧ X ≤ 1
12 3 7 9 11 syl3anbrc ⊢ X ∈ 0 1 ∧ ¬ X ≤ 1 2 → X ∈ 1 2 1