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