Metamath Proof Explorer

Theorem cxpsqrt

Description: The complex exponential function with exponent 1 / 2 exactly matches the complex square root function (the branch cut is in the same place for both functions), and thus serves as a suitable generalization to other n -th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpsqrt 
|- ( A e. CC -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) )

Proof

Step Hyp Ref Expression
1 halfcn 
 |-  ( 1 / 2 ) e. CC
2 halfre 
 |-  ( 1 / 2 ) e. RR
3 halfgt0 
 |-  0 < ( 1 / 2 )
4 2 3 gt0ne0ii 
 |-  ( 1 / 2 ) =/= 0
5 0cxp 
 |-  ( ( ( 1 / 2 ) e. CC /\ ( 1 / 2 ) =/= 0 ) -> ( 0 ^c ( 1 / 2 ) ) = 0 )
6 1 4 5 mp2an 
 |-  ( 0 ^c ( 1 / 2 ) ) = 0
7 sqrt0 
 |-  ( sqrt ` 0 ) = 0
8 6 7 eqtr4i 
 |-  ( 0 ^c ( 1 / 2 ) ) = ( sqrt ` 0 )
9 oveq1 
 |-  ( A = 0 -> ( A ^c ( 1 / 2 ) ) = ( 0 ^c ( 1 / 2 ) ) )
10 fveq2 
 |-  ( A = 0 -> ( sqrt ` A ) = ( sqrt ` 0 ) )
11 8 9 10 3eqtr4a 
 |-  ( A = 0 -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) )
12 11 a1i 
 |-  ( A e. CC -> ( A = 0 -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) ) )
13 ax-icn 
 |-  _i e. CC
14 sqrtcl 
 |-  ( A e. CC -> ( sqrt ` A ) e. CC )
15 14 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( sqrt ` A ) e. CC )
16 sqmul 
 |-  ( ( _i e. CC /\ ( sqrt ` A ) e. CC ) -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( sqrt ` A ) ^ 2 ) ) )
17 13 15 16 sylancr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( sqrt ` A ) ^ 2 ) ) )
18 i2 
 |-  ( _i ^ 2 ) = -u 1
19 18 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( _i ^ 2 ) = -u 1 )
20 sqrtth 
 |-  ( A e. CC -> ( ( sqrt ` A ) ^ 2 ) = A )
21 20 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( sqrt ` A ) ^ 2 ) = A )
22 19 21 oveq12d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( _i ^ 2 ) x. ( ( sqrt ` A ) ^ 2 ) ) = ( -u 1 x. A ) )
23 mulm1 
 |-  ( A e. CC -> ( -u 1 x. A ) = -u A )
24 23 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( -u 1 x. A ) = -u A )
25 17 22 24 3eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = -u A )
26 cxpsqrtlem 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( _i x. ( sqrt ` A ) ) e. RR )
27 26 resqcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) e. RR )
28 25 27 eqeltrrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> -u A e. RR )
29 negeq0 
 |-  ( A e. CC -> ( A = 0 <-> -u A = 0 ) )
30 29 necon3bid 
 |-  ( A e. CC -> ( A =/= 0 <-> -u A =/= 0 ) )
31 30 biimpa 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u A =/= 0 )
32 31 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> -u A =/= 0 )
33 25 32 eqnetrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) =/= 0 )
34 sq0i 
 |-  ( ( _i x. ( sqrt ` A ) ) = 0 -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = 0 )
35 34 necon3i 
 |-  ( ( ( _i x. ( sqrt ` A ) ) ^ 2 ) =/= 0 -> ( _i x. ( sqrt ` A ) ) =/= 0 )
36 33 35 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( _i x. ( sqrt ` A ) ) =/= 0 )
37 26 36 sqgt0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> 0 < ( ( _i x. ( sqrt ` A ) ) ^ 2 ) )
38 37 25 breqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> 0 < -u A )
39 28 38 elrpd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> -u A e. RR+ )
40 logneg 
 |-  ( -u A e. RR+ -> ( log ` -u -u A ) = ( ( log ` -u A ) + ( _i x. _pi ) ) )
41 39 40 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( log ` -u -u A ) = ( ( log ` -u A ) + ( _i x. _pi ) ) )
42 negneg 
 |-  ( A e. CC -> -u -u A = A )
43 42 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> -u -u A = A )
44 43 fveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( log ` -u -u A ) = ( log ` A ) )
45 39 relogcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( log ` -u A ) e. RR )
46 45 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( log ` -u A ) e. CC )
47 picn 
 |-  _pi e. CC
48 13 47 mulcli 
 |-  ( _i x. _pi ) e. CC
49 addcom 
 |-  ( ( ( log ` -u A ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( ( log ` -u A ) + ( _i x. _pi ) ) = ( ( _i x. _pi ) + ( log ` -u A ) ) )
50 46 48 49 sylancl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( log ` -u A ) + ( _i x. _pi ) ) = ( ( _i x. _pi ) + ( log ` -u A ) ) )
51 41 44 50 3eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( log ` A ) = ( ( _i x. _pi ) + ( log ` -u A ) ) )
52 51 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( 1 / 2 ) x. ( log ` A ) ) = ( ( 1 / 2 ) x. ( ( _i x. _pi ) + ( log ` -u A ) ) ) )
53 adddi 
 |-  ( ( ( 1 / 2 ) e. CC /\ ( _i x. _pi ) e. CC /\ ( log ` -u A ) e. CC ) -> ( ( 1 / 2 ) x. ( ( _i x. _pi ) + ( log ` -u A ) ) ) = ( ( ( 1 / 2 ) x. ( _i x. _pi ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) ) )
54 1 48 46 53 mp3an12i 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( 1 / 2 ) x. ( ( _i x. _pi ) + ( log ` -u A ) ) ) = ( ( ( 1 / 2 ) x. ( _i x. _pi ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) ) )
55 52 54 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( 1 / 2 ) x. ( log ` A ) ) = ( ( ( 1 / 2 ) x. ( _i x. _pi ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) ) )
56 2cn 
 |-  2 e. CC
57 2ne0 
 |-  2 =/= 0
58 divrec2 
 |-  ( ( ( _i x. _pi ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( _i x. _pi ) / 2 ) = ( ( 1 / 2 ) x. ( _i x. _pi ) ) )
59 48 56 57 58 mp3an 
 |-  ( ( _i x. _pi ) / 2 ) = ( ( 1 / 2 ) x. ( _i x. _pi ) )
60 13 47 56 57 divassi 
 |-  ( ( _i x. _pi ) / 2 ) = ( _i x. ( _pi / 2 ) )
61 59 60 eqtr3i 
 |-  ( ( 1 / 2 ) x. ( _i x. _pi ) ) = ( _i x. ( _pi / 2 ) )
62 61 oveq1i 
 |-  ( ( ( 1 / 2 ) x. ( _i x. _pi ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) ) = ( ( _i x. ( _pi / 2 ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) )
63 55 62 eqtrdi 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( 1 / 2 ) x. ( log ` A ) ) = ( ( _i x. ( _pi / 2 ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) ) )
64 63 fveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( exp ` ( ( 1 / 2 ) x. ( log ` A ) ) ) = ( exp ` ( ( _i x. ( _pi / 2 ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) ) ) )
65 47 56 57 divcli 
 |-  ( _pi / 2 ) e. CC
66 13 65 mulcli 
 |-  ( _i x. ( _pi / 2 ) ) e. CC
67 mulcl 
 |-  ( ( ( 1 / 2 ) e. CC /\ ( log ` -u A ) e. CC ) -> ( ( 1 / 2 ) x. ( log ` -u A ) ) e. CC )
68 1 46 67 sylancr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( 1 / 2 ) x. ( log ` -u A ) ) e. CC )
69 efadd 
 |-  ( ( ( _i x. ( _pi / 2 ) ) e. CC /\ ( ( 1 / 2 ) x. ( log ` -u A ) ) e. CC ) -> ( exp ` ( ( _i x. ( _pi / 2 ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) ) ) = ( ( exp ` ( _i x. ( _pi / 2 ) ) ) x. ( exp ` ( ( 1 / 2 ) x. ( log ` -u A ) ) ) ) )
70 66 68 69 sylancr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( exp ` ( ( _i x. ( _pi / 2 ) ) + ( ( 1 / 2 ) x. ( log ` -u A ) ) ) ) = ( ( exp ` ( _i x. ( _pi / 2 ) ) ) x. ( exp ` ( ( 1 / 2 ) x. ( log ` -u A ) ) ) ) )
71 efhalfpi 
 |-  ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i
72 71 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i )
73 negcl 
 |-  ( A e. CC -> -u A e. CC )
74 73 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> -u A e. CC )
75 1 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( 1 / 2 ) e. CC )
76 cxpef 
 |-  ( ( -u A e. CC /\ -u A =/= 0 /\ ( 1 / 2 ) e. CC ) -> ( -u A ^c ( 1 / 2 ) ) = ( exp ` ( ( 1 / 2 ) x. ( log ` -u A ) ) ) )
77 74 32 75 76 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( -u A ^c ( 1 / 2 ) ) = ( exp ` ( ( 1 / 2 ) x. ( log ` -u A ) ) ) )
78 ax-1cn 
 |-  1 e. CC
79 2halves 
 |-  ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
80 78 79 ax-mp 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
81 80 oveq2i 
 |-  ( -u A ^c ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( -u A ^c 1 )
82 cxp1 
 |-  ( -u A e. CC -> ( -u A ^c 1 ) = -u A )
83 74 82 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( -u A ^c 1 ) = -u A )
84 81 83 syl5eq 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( -u A ^c ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = -u A )
85 rpcxpcl 
 |-  ( ( -u A e. RR+ /\ ( 1 / 2 ) e. RR ) -> ( -u A ^c ( 1 / 2 ) ) e. RR+ )
86 39 2 85 sylancl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( -u A ^c ( 1 / 2 ) ) e. RR+ )
87 86 rpcnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( -u A ^c ( 1 / 2 ) ) e. CC )
88 87 sqvald 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( -u A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( -u A ^c ( 1 / 2 ) ) x. ( -u A ^c ( 1 / 2 ) ) ) )
89 cxpadd 
 |-  ( ( ( -u A e. CC /\ -u A =/= 0 ) /\ ( 1 / 2 ) e. CC /\ ( 1 / 2 ) e. CC ) -> ( -u A ^c ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( -u A ^c ( 1 / 2 ) ) x. ( -u A ^c ( 1 / 2 ) ) ) )
90 74 32 75 75 89 syl211anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( -u A ^c ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( -u A ^c ( 1 / 2 ) ) x. ( -u A ^c ( 1 / 2 ) ) ) )
91 88 90 eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( -u A ^c ( 1 / 2 ) ) ^ 2 ) = ( -u A ^c ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
92 74 sqsqrtd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( sqrt ` -u A ) ^ 2 ) = -u A )
93 84 91 92 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( -u A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( sqrt ` -u A ) ^ 2 ) )
94 86 rprege0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( -u A ^c ( 1 / 2 ) ) e. RR /\ 0 <_ ( -u A ^c ( 1 / 2 ) ) ) )
95 39 rpsqrtcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( sqrt ` -u A ) e. RR+ )
96 95 rprege0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( sqrt ` -u A ) e. RR /\ 0 <_ ( sqrt ` -u A ) ) )
97 sq11 
 |-  ( ( ( ( -u A ^c ( 1 / 2 ) ) e. RR /\ 0 <_ ( -u A ^c ( 1 / 2 ) ) ) /\ ( ( sqrt ` -u A ) e. RR /\ 0 <_ ( sqrt ` -u A ) ) ) -> ( ( ( -u A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( sqrt ` -u A ) ^ 2 ) <-> ( -u A ^c ( 1 / 2 ) ) = ( sqrt ` -u A ) ) )
98 94 96 97 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( ( -u A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( sqrt ` -u A ) ^ 2 ) <-> ( -u A ^c ( 1 / 2 ) ) = ( sqrt ` -u A ) ) )
99 93 98 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( -u A ^c ( 1 / 2 ) ) = ( sqrt ` -u A ) )
100 77 99 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( exp ` ( ( 1 / 2 ) x. ( log ` -u A ) ) ) = ( sqrt ` -u A ) )
101 72 100 oveq12d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( ( exp ` ( _i x. ( _pi / 2 ) ) ) x. ( exp ` ( ( 1 / 2 ) x. ( log ` -u A ) ) ) ) = ( _i x. ( sqrt ` -u A ) ) )
102 64 70 101 3eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( exp ` ( ( 1 / 2 ) x. ( log ` A ) ) ) = ( _i x. ( sqrt ` -u A ) ) )
103 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( 1 / 2 ) e. CC ) -> ( A ^c ( 1 / 2 ) ) = ( exp ` ( ( 1 / 2 ) x. ( log ` A ) ) ) )
104 1 103 mp3an3 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A ^c ( 1 / 2 ) ) = ( exp ` ( ( 1 / 2 ) x. ( log ` A ) ) ) )
105 104 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( A ^c ( 1 / 2 ) ) = ( exp ` ( ( 1 / 2 ) x. ( log ` A ) ) ) )
106 43 fveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( sqrt ` -u -u A ) = ( sqrt ` A ) )
107 39 rpge0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> 0 <_ -u A )
108 28 107 sqrtnegd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( sqrt ` -u -u A ) = ( _i x. ( sqrt ` -u A ) ) )
109 106 108 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( sqrt ` A ) = ( _i x. ( sqrt ` -u A ) ) )
110 102 105 109 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) )
111 110 ex 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) ) )
112 80 oveq2i 
 |-  ( A ^c ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( A ^c 1 )
113 cxpadd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( 1 / 2 ) e. CC /\ ( 1 / 2 ) e. CC ) -> ( A ^c ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( A ^c ( 1 / 2 ) ) x. ( A ^c ( 1 / 2 ) ) ) )
114 1 1 113 mp3an23 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A ^c ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( A ^c ( 1 / 2 ) ) x. ( A ^c ( 1 / 2 ) ) ) )
115 cxp1 
 |-  ( A e. CC -> ( A ^c 1 ) = A )
116 115 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A ^c 1 ) = A )
117 112 114 116 3eqtr3a 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^c ( 1 / 2 ) ) x. ( A ^c ( 1 / 2 ) ) ) = A )
118 cxpcl 
 |-  ( ( A e. CC /\ ( 1 / 2 ) e. CC ) -> ( A ^c ( 1 / 2 ) ) e. CC )
119 1 118 mpan2 
 |-  ( A e. CC -> ( A ^c ( 1 / 2 ) ) e. CC )
120 119 sqvald 
 |-  ( A e. CC -> ( ( A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( A ^c ( 1 / 2 ) ) x. ( A ^c ( 1 / 2 ) ) ) )
121 120 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( A ^c ( 1 / 2 ) ) x. ( A ^c ( 1 / 2 ) ) ) )
122 20 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( sqrt ` A ) ^ 2 ) = A )
123 117 121 122 3eqtr4d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( sqrt ` A ) ^ 2 ) )
124 sqeqor 
 |-  ( ( ( A ^c ( 1 / 2 ) ) e. CC /\ ( sqrt ` A ) e. CC ) -> ( ( ( A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( sqrt ` A ) ^ 2 ) <-> ( ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) \/ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) ) )
125 119 14 124 syl2anc 
 |-  ( A e. CC -> ( ( ( A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( sqrt ` A ) ^ 2 ) <-> ( ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) \/ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) ) )
126 125 biimpa 
 |-  ( ( A e. CC /\ ( ( A ^c ( 1 / 2 ) ) ^ 2 ) = ( ( sqrt ` A ) ^ 2 ) ) -> ( ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) \/ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) )
127 123 126 syldan 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) \/ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) )
128 127 ord 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -. ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) -> ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) )
129 128 con1d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -. ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) ) )
130 111 129 pm2.61d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) )
131 130 ex 
 |-  ( A e. CC -> ( A =/= 0 -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) ) )
132 12 131 pm2.61dne 
 |-  ( A e. CC -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) )