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 ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 ≤ ( 1 / 2 ) ) → 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) )

Proof

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