Theorem cju

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

	Ref	Expression
Assertion	cju	⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )

Proof

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