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 ) ) = ( √ ‘ 𝐴 ) )