Metamath Proof Explorer

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 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ∧ B ≤ B − A ↔ A = 0

Proof

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