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 ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝐴 ) )

Proof

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