Metamath Proof Explorer

Theorem add20i

Description: Two nonnegative numbers are zero iff their sum is zero. (Contributed by NM, 28-Jul-1999)

Ref Expression
Hypotheses lt2.1 ⊢ A ∈ ℝ
lt2.2 ⊢ B ∈ ℝ
Assertion add20i ⊢ 0 ≤ A ∧ 0 ≤ B → A + B = 0 ↔ A = 0 ∧ B = 0

Proof

Step Hyp Ref Expression
1 lt2.1 ⊢ A ∈ ℝ
2 lt2.2 ⊢ B ∈ ℝ
3 add20 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A + B = 0 ↔ A = 0 ∧ B = 0
4 3 an4s ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ 0 ≤ B → A + B = 0 ↔ A = 0 ∧ B = 0
5 1 2 4 mpanl12 ⊢ 0 ≤ A ∧ 0 ≤ B → A + B = 0 ↔ A = 0 ∧ B = 0