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 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )

Proof

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