Metamath Proof Explorer


Theorem add20

Description: Two nonnegative numbers are zero iff their sum is zero. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion add20 A 0 A B 0 B A + B = 0 A = 0 B = 0

Proof

Step Hyp Ref Expression
1 simpllr A 0 A B 0 B A + B = 0 0 A
2 simplrl A 0 A B 0 B A + B = 0 B
3 simplll A 0 A B 0 B A + B = 0 A
4 addge02 B A 0 A B A + B
5 2 3 4 syl2anc A 0 A B 0 B A + B = 0 0 A B A + B
6 1 5 mpbid A 0 A B 0 B A + B = 0 B A + B
7 simpr A 0 A B 0 B A + B = 0 A + B = 0
8 6 7 breqtrd A 0 A B 0 B A + B = 0 B 0
9 simplrr A 0 A B 0 B A + B = 0 0 B
10 0red A 0 A B 0 B A + B = 0 0
11 2 10 letri3d A 0 A B 0 B A + B = 0 B = 0 B 0 0 B
12 8 9 11 mpbir2and A 0 A B 0 B A + B = 0 B = 0
13 12 oveq2d A 0 A B 0 B A + B = 0 A + B = A + 0
14 3 recnd A 0 A B 0 B A + B = 0 A
15 14 addid1d A 0 A B 0 B A + B = 0 A + 0 = A
16 13 7 15 3eqtr3rd A 0 A B 0 B A + B = 0 A = 0
17 16 12 jca A 0 A B 0 B A + B = 0 A = 0 B = 0
18 17 ex A 0 A B 0 B A + B = 0 A = 0 B = 0
19 oveq12 A = 0 B = 0 A + B = 0 + 0
20 00id 0 + 0 = 0
21 19 20 eqtrdi A = 0 B = 0 A + B = 0
22 18 21 impbid1 A 0 A B 0 B A + B = 0 A = 0 B = 0