cju

Description: The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013)

		Ref	Expression
	Assertion	cju	$⊢ A \in ℂ \to \exists! x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		cnre	$⊢ A \in ℂ \to \exists y \in ℝ \exists z \in ℝ A = y + i z$
2		recn	$⊢ y \in ℝ \to y \in ℂ$
3		ax-icn	$⊢ i \in ℂ$
4		recn	$⊢ z \in ℝ \to z \in ℂ$
5		mulcl	$⊢ (i \in ℂ \land z \in ℂ) \to i z \in ℂ$
6	3 4 5	sylancr	$⊢ z \in ℝ \to i z \in ℂ$
7		subcl	$⊢ (y \in ℂ \land i z \in ℂ) \to y - i z \in ℂ$
8	2 6 7	syl2an	$⊢ (y \in ℝ \land z \in ℝ) \to y - i z \in ℂ$
9	2	adantr	$⊢ (y \in ℝ \land z \in ℝ) \to y \in ℂ$
10	6	adantl	$⊢ (y \in ℝ \land z \in ℝ) \to i z \in ℂ$
11	9 10 9	ppncand	$⊢ (y \in ℝ \land z \in ℝ) \to y + i z + (y - i z) = y + y$
12		readdcl	$⊢ (y \in ℝ \land y \in ℝ) \to y + y \in ℝ$
13	12	anidms	$⊢ y \in ℝ \to y + y \in ℝ$
14	13	adantr	$⊢ (y \in ℝ \land z \in ℝ) \to y + y \in ℝ$
15	11 14	eqeltrd	$⊢ (y \in ℝ \land z \in ℝ) \to y + i z + (y - i z) \in ℝ$
16	9 10 10	pnncand	$⊢ (y \in ℝ \land z \in ℝ) \to y + i z - (y - i z) = i z + i z$
17	3	a1i	$⊢ (y \in ℝ \land z \in ℝ) \to i \in ℂ$
18	4	adantl	$⊢ (y \in ℝ \land z \in ℝ) \to z \in ℂ$
19	17 18 18	adddid	$⊢ (y \in ℝ \land z \in ℝ) \to i (z + z) = i z + i z$
20	16 19	eqtr4d	$⊢ (y \in ℝ \land z \in ℝ) \to y + i z - (y - i z) = i (z + z)$
21	20	oveq2d	$⊢ (y \in ℝ \land z \in ℝ) \to i (y + i z - (y - i z)) = i i (z + z)$
22	18 18	addcld	$⊢ (y \in ℝ \land z \in ℝ) \to z + z \in ℂ$
23		mulass	$⊢ (i \in ℂ \land i \in ℂ \land z + z \in ℂ) \to i i (z + z) = i i (z + z)$
24	3 3 22 23	mp3an12i	$⊢ (y \in ℝ \land z \in ℝ) \to i i (z + z) = i i (z + z)$
25	21 24	eqtr4d	$⊢ (y \in ℝ \land z \in ℝ) \to i (y + i z - (y - i z)) = i i (z + z)$
26		ixi	$⊢ i i = - 1$
27		1re	$⊢ 1 \in ℝ$
28	27	renegcli	$⊢ - 1 \in ℝ$
29	26 28	eqeltri	$⊢ i i \in ℝ$
30		simpr	$⊢ (y \in ℝ \land z \in ℝ) \to z \in ℝ$
31	30 30	readdcld	$⊢ (y \in ℝ \land z \in ℝ) \to z + z \in ℝ$
32		remulcl	$⊢ (i i \in ℝ \land z + z \in ℝ) \to i i (z + z) \in ℝ$
33	29 31 32	sylancr	$⊢ (y \in ℝ \land z \in ℝ) \to i i (z + z) \in ℝ$
34	25 33	eqeltrd	$⊢ (y \in ℝ \land z \in ℝ) \to i (y + i z - (y - i z)) \in ℝ$
35		oveq2	$⊢ x = y - i z \to y + i z + x = y + i z + (y - i z)$
36	35	eleq1d	$⊢ x = y - i z \to (y + i z + x \in ℝ \leftrightarrow y + i z + (y - i z) \in ℝ)$
37		oveq2	$⊢ x = y - i z \to y + i z - x = y + i z - (y - i z)$
38	37	oveq2d	$⊢ x = y - i z \to i (y + i z - x) = i (y + i z - (y - i z))$
39	38	eleq1d	$⊢ x = y - i z \to (i (y + i z - x) \in ℝ \leftrightarrow i (y + i z - (y - i z)) \in ℝ)$
40	36 39	anbi12d	$⊢ x = y - i z \to ((y + i z + x \in ℝ \land i (y + i z - x) \in ℝ) \leftrightarrow (y + i z + (y - i z) \in ℝ \land i (y + i z - (y - i z)) \in ℝ))$
41	40	rspcev	$⊢ (y - i z \in ℂ \land (y + i z + (y - i z) \in ℝ \land i (y + i z - (y - i z)) \in ℝ)) \to \exists x \in ℂ (y + i z + x \in ℝ \land i (y + i z - x) \in ℝ)$
42	8 15 34 41	syl12anc	$⊢ (y \in ℝ \land z \in ℝ) \to \exists x \in ℂ (y + i z + x \in ℝ \land i (y + i z - x) \in ℝ)$
43		oveq1	$⊢ A = y + i z \to A + x = y + i z + x$
44	43	eleq1d	$⊢ A = y + i z \to (A + x \in ℝ \leftrightarrow y + i z + x \in ℝ)$
45		oveq1	$⊢ A = y + i z \to A - x = y + i z - x$
46	45	oveq2d	$⊢ A = y + i z \to i (A - x) = i (y + i z - x)$
47	46	eleq1d	$⊢ A = y + i z \to (i (A - x) \in ℝ \leftrightarrow i (y + i z - x) \in ℝ)$
48	44 47	anbi12d	$⊢ A = y + i z \to ((A + x \in ℝ \land i (A - x) \in ℝ) \leftrightarrow (y + i z + x \in ℝ \land i (y + i z - x) \in ℝ))$
49	48	rexbidv	$⊢ A = y + i z \to (\exists x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ) \leftrightarrow \exists x \in ℂ (y + i z + x \in ℝ \land i (y + i z - x) \in ℝ))$
50	42 49	syl5ibrcom	$⊢ (y \in ℝ \land z \in ℝ) \to (A = y + i z \to \exists x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ))$
51	50	rexlimivv	$⊢ \exists y \in ℝ \exists z \in ℝ A = y + i z \to \exists x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ)$
52	1 51	syl	$⊢ A \in ℂ \to \exists x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ)$
53		an4	$⊢ ((A + x \in ℝ \land i (A - x) \in ℝ) \land (A + y \in ℝ \land i (A - y) \in ℝ)) \leftrightarrow ((A + x \in ℝ \land A + y \in ℝ) \land (i (A - x) \in ℝ \land i (A - y) \in ℝ))$
54		resubcl	$⊢ (A + x \in ℝ \land A + y \in ℝ) \to A + x - (A + y) \in ℝ$
55		pnpcan	$⊢ (A \in ℂ \land x \in ℂ \land y \in ℂ) \to A + x - (A + y) = x - y$
56	55	3expb	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to A + x - (A + y) = x - y$
57	56	eleq1d	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to (A + x - (A + y) \in ℝ \leftrightarrow x - y \in ℝ)$
58	54 57	imbitrid	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to ((A + x \in ℝ \land A + y \in ℝ) \to x - y \in ℝ)$
59		resubcl	$⊢ (i (A - y) \in ℝ \land i (A - x) \in ℝ) \to i (A - y) - i (A - x) \in ℝ$
60	59	ancoms	$⊢ (i (A - x) \in ℝ \land i (A - y) \in ℝ) \to i (A - y) - i (A - x) \in ℝ$
61	3	a1i	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to i \in ℂ$
62		subcl	$⊢ (A \in ℂ \land y \in ℂ) \to A - y \in ℂ$
63	62	adantrl	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to A - y \in ℂ$
64		subcl	$⊢ (A \in ℂ \land x \in ℂ) \to A - x \in ℂ$
65	64	adantrr	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to A - x \in ℂ$
66	61 63 65	subdid	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to i (A - y - (A - x)) = i (A - y) - i (A - x)$
67		nnncan1	$⊢ (A \in ℂ \land y \in ℂ \land x \in ℂ) \to A - y - (A - x) = x - y$
68	67	3com23	$⊢ (A \in ℂ \land x \in ℂ \land y \in ℂ) \to A - y - (A - x) = x - y$
69	68	3expb	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to A - y - (A - x) = x - y$
70	69	oveq2d	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to i (A - y - (A - x)) = i (x - y)$
71	66 70	eqtr3d	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to i (A - y) - i (A - x) = i (x - y)$
72	71	eleq1d	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to (i (A - y) - i (A - x) \in ℝ \leftrightarrow i (x - y) \in ℝ)$
73	60 72	imbitrid	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to ((i (A - x) \in ℝ \land i (A - y) \in ℝ) \to i (x - y) \in ℝ)$
74	58 73	anim12d	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to (((A + x \in ℝ \land A + y \in ℝ) \land (i (A - x) \in ℝ \land i (A - y) \in ℝ)) \to (x - y \in ℝ \land i (x - y) \in ℝ))$
75		rimul	$⊢ (x - y \in ℝ \land i (x - y) \in ℝ) \to x - y = 0$
76	75	a1i	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to ((x - y \in ℝ \land i (x - y) \in ℝ) \to x - y = 0)$
77		subeq0	$⊢ (x \in ℂ \land y \in ℂ) \to (x - y = 0 \leftrightarrow x = y)$
78	77	biimpd	$⊢ (x \in ℂ \land y \in ℂ) \to (x - y = 0 \to x = y)$
79	78	adantl	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to (x - y = 0 \to x = y)$
80	74 76 79	3syld	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to (((A + x \in ℝ \land A + y \in ℝ) \land (i (A - x) \in ℝ \land i (A - y) \in ℝ)) \to x = y)$
81	53 80	biimtrid	$⊢ (A \in ℂ \land (x \in ℂ \land y \in ℂ)) \to (((A + x \in ℝ \land i (A - x) \in ℝ) \land (A + y \in ℝ \land i (A - y) \in ℝ)) \to x = y)$
82	81	ralrimivva	$⊢ A \in ℂ \to \forall x \in ℂ \forall y \in ℂ (((A + x \in ℝ \land i (A - x) \in ℝ) \land (A + y \in ℝ \land i (A - y) \in ℝ)) \to x = y)$
83		oveq2	$⊢ x = y \to A + x = A + y$
84	83	eleq1d	$⊢ x = y \to (A + x \in ℝ \leftrightarrow A + y \in ℝ)$
85		oveq2	$⊢ x = y \to A - x = A - y$
86	85	oveq2d	$⊢ x = y \to i (A - x) = i (A - y)$
87	86	eleq1d	$⊢ x = y \to (i (A - x) \in ℝ \leftrightarrow i (A - y) \in ℝ)$
88	84 87	anbi12d	$⊢ x = y \to ((A + x \in ℝ \land i (A - x) \in ℝ) \leftrightarrow (A + y \in ℝ \land i (A - y) \in ℝ))$
89	88	reu4	$⊢ \exists! x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ) \leftrightarrow (\exists x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ) \land \forall x \in ℂ \forall y \in ℂ (((A + x \in ℝ \land i (A - x) \in ℝ) \land (A + y \in ℝ \land i (A - y) \in ℝ)) \to x = y))$
90	52 82 89	sylanbrc	$⊢ A \in ℂ \to \exists! x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ)$

Metamath Proof Explorer

Theorem cju

Proof