This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 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 bitrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ↔ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ ( 𝐵 − 𝐴 ) ) ) )
17 3 16 bitr2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ ( 𝐵 − 𝐴 ) ) ↔ 𝐴 = 0 ) )