Metamath Proof Explorer

Theorem suble0

Description: Nonpositive subtraction. (Contributed by NM, 20-Mar-2008) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion suble0 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ≤ 0 ↔ A ≤ B

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 suble ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ∈ ℝ → A − B ≤ 0 ↔ A − 0 ≤ B
3 1 2 mp3an3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ≤ 0 ↔ A − 0 ≤ B
4 simpl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
5 4 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℂ
6 5 subid1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − 0 = A
7 6 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − 0 ≤ B ↔ A ≤ B
8 3 7 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ≤ 0 ↔ A ≤ B