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 \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A + B = 0 \leftrightarrow (A = 0 \land B = 0))$

Proof

Step	Hyp	Ref	Expression
1		simpllr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to 0 \leq A$
2		simplrl	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to B \in ℝ$
3		simplll	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to A \in ℝ$
4		addge02	$⊢ (B \in ℝ \land A \in ℝ) \to (0 \leq A \leftrightarrow B \leq A + B)$
5	2 3 4	syl2anc	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to (0 \leq A \leftrightarrow B \leq A + B)$
6	1 5	mpbid	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to B \leq A + B$
7		simpr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to A + B = 0$
8	6 7	breqtrd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to B \leq 0$
9		simplrr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to 0 \leq B$
10		0red	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to 0 \in ℝ$
11	2 10	letri3d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to (B = 0 \leftrightarrow (B \leq 0 \land 0 \leq B))$
12	8 9 11	mpbir2and	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to B = 0$
13	12	oveq2d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to A + B = A + 0$
14	3	recnd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to A \in ℂ$
15	14	addid1d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to A + 0 = A$
16	13 7 15	3eqtr3rd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to A = 0$
17	16 12	jca	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \land A + B = 0) \to (A = 0 \land B = 0)$
18	17	ex	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A + B = 0 \to (A = 0 \land B = 0))$
19		oveq12	$⊢ (A = 0 \land B = 0) \to A + B = 0 + 0$
20		00id	$⊢ 0 + 0 = 0$
21	19 20	syl6eq	$⊢ (A = 0 \land B = 0) \to A + B = 0$
22	18 21	impbid1	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A + B = 0 \leftrightarrow (A = 0 \land B = 0))$

Metamath Proof Explorer

Theorem add20

Proof