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 ) )