Theorem suble0

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

	Ref	Expression
Assertion	suble0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 − 𝐵 ) ≤ 0 ↔ 𝐴 ≤ 𝐵 ) )

Proof

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