Metamath Proof Explorer

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 · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )