cru

Description: The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of Gleason p. 130. (Contributed by NM, 9-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	cru	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A + i B = C + i D \leftrightarrow (A = C \land B = D))$

Proof

Step	Hyp	Ref	Expression
1		simplrl	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to C \in ℝ$
2	1	recnd	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to C \in ℂ$
3		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to A \in ℝ$
4	3	recnd	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to A \in ℂ$
5		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to A + i B = C + i D$
6		ax-icn	$⊢ i \in ℂ$
7	6	a1i	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i \in ℂ$
8		simpllr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to B \in ℝ$
9	8	recnd	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to B \in ℂ$
10	7 9	mulcld	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i B \in ℂ$
11		simplrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to D \in ℝ$
12	11	recnd	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to D \in ℂ$
13	7 12	mulcld	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i D \in ℂ$
14	4 10 2 13	addsubeq4d	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to (A + i B = C + i D \leftrightarrow C - A = i B - i D)$
15	5 14	mpbid	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to C - A = i B - i D$
16	8 11	resubcld	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to B - D \in ℝ$
17	7 9 12	subdid	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i (B - D) = i B - i D$
18	17 15	eqtr4d	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i (B - D) = C - A$
19	1 3	resubcld	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to C - A \in ℝ$
20	18 19	eqeltrd	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i (B - D) \in ℝ$
21		rimul	$⊢ (B - D \in ℝ \land i (B - D) \in ℝ) \to B - D = 0$
22	16 20 21	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to B - D = 0$
23	9 12 22	subeq0d	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to B = D$
24	23	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i B = i D$
25	24	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i B - i D = i D - i D$
26	13	subidd	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to i D - i D = 0$
27	15 25 26	3eqtrd	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to C - A = 0$
28	2 4 27	subeq0d	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to C = A$
29	28	eqcomd	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to A = C$
30	29 23	jca	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land A + i B = C + i D) \to (A = C \land B = D)$
31	30	ex	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A + i B = C + i D \to (A = C \land B = D))$
32		oveq2	$⊢ B = D \to i B = i D$
33		oveq12	$⊢ (A = C \land i B = i D) \to A + i B = C + i D$
34	32 33	sylan2	$⊢ (A = C \land B = D) \to A + i B = C + i D$
35	31 34	impbid1	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A + i B = C + i D \leftrightarrow (A = C \land B = D))$

Metamath Proof Explorer

Theorem cru

Proof