Theorem lesub0

Description: Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		0red	⊢ ( 𝐵 ∈ ℝ → 0 ∈ ℝ )
2		letri3	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 = 0 ↔ ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 = 0 ↔ ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ) )
4		ancom	⊢ ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ↔ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 0 ) )
5		simpr	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
6		0red	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 0 ∈ ℝ )
7		simpl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝐵 ∈ ℝ )
8		lesub2	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 0 ↔ ( 𝐵 − 0 ) ≤ ( 𝐵 − 𝐴 ) ) )
9	5 6 7 8	syl3anc	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ≤ 0 ↔ ( 𝐵 − 0 ) ≤ ( 𝐵 − 𝐴 ) ) )
10	7	recnd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝐵 ∈ ℂ )
11	10	subid1d	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 − 0 ) = 𝐵 )
12	11	breq1d	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 − 0 ) ≤ ( 𝐵 − 𝐴 ) ↔ 𝐵 ≤ ( 𝐵 − 𝐴 ) ) )
13	9 12	bitrd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ≤ 0 ↔ 𝐵 ≤ ( 𝐵 − 𝐴 ) ) )
14	13	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 0 ↔ 𝐵 ≤ ( 𝐵 − 𝐴 ) ) )
15	14	anbi2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 0 ) ↔ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ ( 𝐵 − 𝐴 ) ) ) )
16	4 15	syl5bb	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ↔ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ ( 𝐵 − 𝐴 ) ) ) )
17	3 16	bitr2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ ( 𝐵 − 𝐴 ) ) ↔ 𝐴 = 0 ) )