Theorem subge0

Description: Nonnegative subtraction. (Contributed by NM, 14-Mar-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ∈ ℝ )
2		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
3		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
4		leaddsub	⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 + 𝐵 ) ≤ 𝐴 ↔ 0 ≤ ( 𝐴 − 𝐵 ) ) )
5	1 2 3 4	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 + 𝐵 ) ≤ 𝐴 ↔ 0 ≤ ( 𝐴 − 𝐵 ) ) )
6	2	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℂ )
7	6	addlidd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 + 𝐵 ) = 𝐵 )
8	7	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 + 𝐵 ) ≤ 𝐴 ↔ 𝐵 ≤ 𝐴 ) )
9	5 8	bitr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ ( 𝐴 − 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )