Metamath Proof Explorer

Theorem addsub4

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005)

		Ref	Expression
	Assertion	addsub4	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B - (C + D) = (A - C) + B - D$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A \in ℂ$
2		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B \in ℂ$
3		simprl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C \in ℂ$
4		addsub	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A + B - C = A - C + B$
5	1 2 3 4	syl3anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B - C = A - C + B$
6	5	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) - C - D = (A - C) + B - D$
7	1 2	addcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B \in ℂ$
8		simprr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D \in ℂ$
9		subsub4	$⊢ (A + B \in ℂ \land C \in ℂ \land D \in ℂ) \to (A + B) - C - D = A + B - (C + D)$
10	7 3 8 9	syl3anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) - C - D = A + B - (C + D)$
11		subcl	$⊢ (A \in ℂ \land C \in ℂ) \to A - C \in ℂ$
12	11	ad2ant2r	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A - C \in ℂ$
13		addsubass	$⊢ (A - C \in ℂ \land B \in ℂ \land D \in ℂ) \to (A - C) + B - D = (A - C) + B - D$
14	12 2 8 13	syl3anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A - C) + B - D = (A - C) + B - D$
15	6 10 14	3eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B - (C + D) = (A - C) + B - D$