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

Metamath Proof Explorer

Theorem iirev

Description: Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion iirev ( 𝑋 ∈ ( 0 [,] 1 ) → ( 1 − 𝑋 ) ∈ ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 1 − 𝑋 ) ∈ ℝ )
3 1 2 mpan ⊢ ( 𝑋 ∈ ℝ → ( 1 − 𝑋 ) ∈ ℝ )
4 3 3ad2ant1 ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → ( 1 − 𝑋 ) ∈ ℝ )
5 simp3 ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → 𝑋 ≤ 1 )
6 simp1 ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → 𝑋 ∈ ℝ )
7 subge0 ⊢ ( ( 1 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 0 ≤ ( 1 − 𝑋 ) ↔ 𝑋 ≤ 1 ) )
8 1 6 7 sylancr ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → ( 0 ≤ ( 1 − 𝑋 ) ↔ 𝑋 ≤ 1 ) )
9 5 8 mpbird ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → 0 ≤ ( 1 − 𝑋 ) )
10 simp2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → 0 ≤ 𝑋 )
11 subge02 ⊢ ( ( 1 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 0 ≤ 𝑋 ↔ ( 1 − 𝑋 ) ≤ 1 ) )
12 1 6 11 sylancr ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → ( 0 ≤ 𝑋 ↔ ( 1 − 𝑋 ) ≤ 1 ) )
13 10 12 mpbid ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → ( 1 − 𝑋 ) ≤ 1 )
14 4 9 13 3jca ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → ( ( 1 − 𝑋 ) ∈ ℝ ∧ 0 ≤ ( 1 − 𝑋 ) ∧ ( 1 − 𝑋 ) ≤ 1 ) )
15 elicc01 ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) ↔ ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) )
16 elicc01 ⊢ ( ( 1 − 𝑋 ) ∈ ( 0 [,] 1 ) ↔ ( ( 1 − 𝑋 ) ∈ ℝ ∧ 0 ≤ ( 1 − 𝑋 ) ∧ ( 1 − 𝑋 ) ≤ 1 ) )
17 14 15 16 3imtr4i ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → ( 1 − 𝑋 ) ∈ ( 0 [,] 1 ) )