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

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 e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A + B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )

Proof

Step Hyp Ref Expression
1 simpllr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> 0 <_ A )
2 simplrl 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> B e. RR )
3 simplll 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> A e. RR )
4 addge02 
 |-  ( ( B e. RR /\ A e. RR ) -> ( 0 <_ A <-> B <_ ( A + B ) ) )
5 2 3 4 syl2anc 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> ( 0 <_ A <-> B <_ ( A + B ) ) )
6 1 5 mpbid 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> B <_ ( A + B ) )
7 simpr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> ( A + B ) = 0 )
8 6 7 breqtrd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> B <_ 0 )
9 simplrr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> 0 <_ B )
10 0red 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> 0 e. RR )
11 2 10 letri3d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> ( B = 0 <-> ( B <_ 0 /\ 0 <_ B ) ) )
12 8 9 11 mpbir2and 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> B = 0 )
13 12 oveq2d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> ( A + B ) = ( A + 0 ) )
14 3 recnd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> A e. CC )
15 14 addridd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> ( A + 0 ) = A )
16 13 7 15 3eqtr3rd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> A = 0 )
17 16 12 jca 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) /\ ( A + B ) = 0 ) -> ( A = 0 /\ B = 0 ) )
18 17 ex 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 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 e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A + B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )