Metamath Proof Explorer

Theorem relin01

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

Ref Expression
Assertion relin01 ⊢ A ∈ ℝ → A ≤ 0 ∨ 0 ≤ A ∧ A ≤ 1 ∨ 1 ≤ A

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 letric ⊢ A ∈ ℝ ∧ 1 ∈ ℝ → A ≤ 1 ∨ 1 ≤ A
3 1 2 mpan2 ⊢ A ∈ ℝ → A ≤ 1 ∨ 1 ≤ A
4 0re ⊢ 0 ∈ ℝ
5 letric ⊢ A ∈ ℝ ∧ 0 ∈ ℝ → A ≤ 0 ∨ 0 ≤ A
6 4 5 mpan2 ⊢ A ∈ ℝ → A ≤ 0 ∨ 0 ≤ A
7 pm3.21 ⊢ A ≤ 1 → 0 ≤ A → 0 ≤ A ∧ A ≤ 1
8 7 orim2d ⊢ A ≤ 1 → A ≤ 0 ∨ 0 ≤ A → A ≤ 0 ∨ 0 ≤ A ∧ A ≤ 1
9 6 8 syl5com ⊢ A ∈ ℝ → A ≤ 1 → A ≤ 0 ∨ 0 ≤ A ∧ A ≤ 1
10 9 orim1d ⊢ A ∈ ℝ → A ≤ 1 ∨ 1 ≤ A → A ≤ 0 ∨ 0 ≤ A ∧ A ≤ 1 ∨ 1 ≤ A
11 3 10 mpd ⊢ A ∈ ℝ → A ≤ 0 ∨ 0 ≤ A ∧ A ≤ 1 ∨ 1 ≤ A
12 df-3or ⊢ A ≤ 0 ∨ 0 ≤ A ∧ A ≤ 1 ∨ 1 ≤ A ↔ A ≤ 0 ∨ 0 ≤ A ∧ A ≤ 1 ∨ 1 ≤ A
13 11 12 sylibr ⊢ A ∈ ℝ → A ≤ 0 ∨ 0 ≤ A ∧ A ≤ 1 ∨ 1 ≤ A