Theorem relin01

Description: An interval law for less than or equal. (Contributed by Scott Fenton, 27-Jun-2013)

	Ref	Expression
Assertion	relin01	$$⊢A\in ℝ\to \left(A\le 0\vee \left(0\le A\wedge A\le 1\right)\vee 1\le A\right)$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		letric	$$⊢\left(A\in ℝ\wedge 1\in ℝ\right)\to \left(A\le 1\vee 1\le A\right)$$
3	1 2	mpan2	$$⊢A\in ℝ\to \left(A\le 1\vee 1\le A\right)$$
4		0re	$$⊢0\in ℝ$$
5		letric	$$⊢\left(A\in ℝ\wedge 0\in ℝ\right)\to \left(A\le 0\vee 0\le A\right)$$
6	4 5	mpan2	$$⊢A\in ℝ\to \left(A\le 0\vee 0\le A\right)$$
7		pm3.21	$$⊢A\le 1\to \left(0\le A\to \left(0\le A\wedge A\le 1\right)\right)$$
8	7	orim2d	$$⊢A\le 1\to \left(\left(A\le 0\vee 0\le A\right)\to \left(A\le 0\vee \left(0\le A\wedge A\le 1\right)\right)\right)$$
9	6 8	syl5com	$$⊢A\in ℝ\to \left(A\le 1\to \left(A\le 0\vee \left(0\le A\wedge A\le 1\right)\right)\right)$$
10	9	orim1d	$$⊢A\in ℝ\to \left(\left(A\le 1\vee 1\le A\right)\to \left(\left(A\le 0\vee \left(0\le A\wedge A\le 1\right)\right)\vee 1\le A\right)\right)$$
11	3 10	mpd	$$⊢A\in ℝ\to \left(\left(A\le 0\vee \left(0\le A\wedge A\le 1\right)\right)\vee 1\le A\right)$$
12		df-3or	$$⊢\left(A\le 0\vee \left(0\le A\wedge A\le 1\right)\vee 1\le A\right)\leftrightarrow \left(\left(A\le 0\vee \left(0\le A\wedge A\le 1\right)\right)\vee 1\le A\right)$$
13	11 12	sylibr	$$⊢A\in ℝ\to \left(A\le 0\vee \left(0\le A\wedge A\le 1\right)\vee 1\le A\right)$$