# Metamath Proof Explorer

## Theorem iirev

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

Ref Expression
Assertion iirev ${⊢}{X}\in \left[0,1\right]\to 1-{X}\in \left[0,1\right]$

### Proof

Step Hyp Ref Expression
1 1re ${⊢}1\in ℝ$
2 resubcl ${⊢}\left(1\in ℝ\wedge {X}\in ℝ\right)\to 1-{X}\in ℝ$
3 1 2 mpan ${⊢}{X}\in ℝ\to 1-{X}\in ℝ$
4 3 3ad2ant1 ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to 1-{X}\in ℝ$
5 simp3 ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to {X}\le 1$
6 simp1 ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to {X}\in ℝ$
7 subge0 ${⊢}\left(1\in ℝ\wedge {X}\in ℝ\right)\to \left(0\le 1-{X}↔{X}\le 1\right)$
8 1 6 7 sylancr ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to \left(0\le 1-{X}↔{X}\le 1\right)$
9 5 8 mpbird ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to 0\le 1-{X}$
10 simp2 ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to 0\le {X}$
11 subge02 ${⊢}\left(1\in ℝ\wedge {X}\in ℝ\right)\to \left(0\le {X}↔1-{X}\le 1\right)$
12 1 6 11 sylancr ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to \left(0\le {X}↔1-{X}\le 1\right)$
13 10 12 mpbid ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to 1-{X}\le 1$
14 4 9 13 3jca ${⊢}\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)\to \left(1-{X}\in ℝ\wedge 0\le 1-{X}\wedge 1-{X}\le 1\right)$
15 elicc01 ${⊢}{X}\in \left[0,1\right]↔\left({X}\in ℝ\wedge 0\le {X}\wedge {X}\le 1\right)$
16 elicc01 ${⊢}1-{X}\in \left[0,1\right]↔\left(1-{X}\in ℝ\wedge 0\le 1-{X}\wedge 1-{X}\le 1\right)$
17 14 15 16 3imtr4i ${⊢}{X}\in \left[0,1\right]\to 1-{X}\in \left[0,1\right]$