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 
|- ( A e. CC -> E! x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )

Proof

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