This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 0 ∨ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∨ 1 ≤ 𝐴 ) )

Proof

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