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