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 ) ) )