iirev

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

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

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

Metamath Proof Explorer