Theorem cxpsqrtth

Description: Square root theorem over the complex numbers for the complex power function. Theorem I.35 of Apostol p. 29. Compare with sqrtth . (Contributed by AV, 23-Dec-2022)

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

Proof

Step	Hyp	Ref	Expression
1		2cnne0	|- ( 2 e. CC /\ 2 =/= 0 )
2		0cxp	|- ( ( 2 e. CC /\ 2 =/= 0 ) -> ( 0 ^c 2 ) = 0 )
3	1 2	ax-mp	|- ( 0 ^c 2 ) = 0
4		fveq2	|- ( A = 0 -> ( sqrt ` A ) = ( sqrt ` 0 ) )
5		sqrt0	|- ( sqrt ` 0 ) = 0
6	4 5	eqtrdi	|- ( A = 0 -> ( sqrt ` A ) = 0 )
7	6	oveq1d	|- ( A = 0 -> ( ( sqrt ` A ) ^c 2 ) = ( 0 ^c 2 ) )
8		id	|- ( A = 0 -> A = 0 )
9	3 7 8	3eqtr4a	|- ( A = 0 -> ( ( sqrt ` A ) ^c 2 ) = A )
10	9	a1d	|- ( A = 0 -> ( A e. CC -> ( ( sqrt ` A ) ^c 2 ) = A ) )
11		sqrtcl	|- ( A e. CC -> ( sqrt ` A ) e. CC )
12	11	adantr	|- ( ( A e. CC /\ A =/= 0 ) -> ( sqrt ` A ) e. CC )
13		simpl	|- ( ( A e. CC /\ ( sqrt ` A ) = 0 ) -> A e. CC )
14		simpr	|- ( ( A e. CC /\ ( sqrt ` A ) = 0 ) -> ( sqrt ` A ) = 0 )
15	13 14	sqr00d	|- ( ( A e. CC /\ ( sqrt ` A ) = 0 ) -> A = 0 )
16	15	ex	|- ( A e. CC -> ( ( sqrt ` A ) = 0 -> A = 0 ) )
17	16	necon3d	|- ( A e. CC -> ( A =/= 0 -> ( sqrt ` A ) =/= 0 ) )
18	17	imp	|- ( ( A e. CC /\ A =/= 0 ) -> ( sqrt ` A ) =/= 0 )
19		2z	|- 2 e. ZZ
20	19	a1i	|- ( ( A e. CC /\ A =/= 0 ) -> 2 e. ZZ )
21	12 18 20	cxpexpzd	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( sqrt ` A ) ^c 2 ) = ( ( sqrt ` A ) ^ 2 ) )
22		sqrtth	|- ( A e. CC -> ( ( sqrt ` A ) ^ 2 ) = A )
23	22	adantr	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( sqrt ` A ) ^ 2 ) = A )
24	21 23	eqtrd	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( sqrt ` A ) ^c 2 ) = A )
25	24	expcom	|- ( A =/= 0 -> ( A e. CC -> ( ( sqrt ` A ) ^c 2 ) = A ) )
26	10 25	pm2.61ine	|- ( A e. CC -> ( ( sqrt ` A ) ^c 2 ) = A )