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 AB0ABBAA=0

Proof

Step Hyp Ref Expression
1 0red B0
2 letri3 A0A=0A00A
3 1 2 sylan2 ABA=0A00A
4 ancom A00A0AA0
5 simpr BAA
6 0red BA0
7 simpl BAB
8 lesub2 A0BA0B0BA
9 5 6 7 8 syl3anc BAA0B0BA
10 7 recnd BAB
11 10 subid1d BAB0=B
12 11 breq1d BAB0BABBA
13 9 12 bitrd BAA0BBA
14 13 ancoms ABA0BBA
15 14 anbi2d AB0AA00ABBA
16 4 15 syl5bb ABA00A0ABBA
17 3 16 bitr2d AB0ABBAA=0