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\in ℂ\to {\sqrt{A}}^2=A$$

Proof

Step	Hyp	Ref	Expression
1		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
2		0cxp	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)\to 0^2=0$$
3	1 2	ax-mp	$$⊢0^2=0$$
4		fveq2	$$⊢A=0\to \sqrt{A}=\sqrt{0}$$
5		sqrt0	$$⊢\sqrt{0}=0$$
6	4 5	eqtrdi	$$⊢A=0\to \sqrt{A}=0$$
7	6	oveq1d	$$⊢A=0\to {\sqrt{A}}^2=0^2$$
8		id	$$⊢A=0\to A=0$$
9	3 7 8	3eqtr4a	$$⊢A=0\to {\sqrt{A}}^2=A$$
10	9	a1d	$$⊢A=0\to \left(A\in ℂ\to {\sqrt{A}}^2=A\right)$$
11		sqrtcl	$$⊢A\in ℂ\to \sqrt{A}\in ℂ$$
12	11	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \sqrt{A}\in ℂ$$
13		simpl	$$⊢\left(A\in ℂ\wedge \sqrt{A}=0\right)\to A\in ℂ$$
14		simpr	$$⊢\left(A\in ℂ\wedge \sqrt{A}=0\right)\to \sqrt{A}=0$$
15	13 14	sqr00d	$$⊢\left(A\in ℂ\wedge \sqrt{A}=0\right)\to A=0$$
16	15	ex	$$⊢A\in ℂ\to \left(\sqrt{A}=0\to A=0\right)$$
17	16	necon3d	$$⊢A\in ℂ\to \left(A\ne 0\to \sqrt{A}\ne 0\right)$$
18	17	imp	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \sqrt{A}\ne 0$$
19		2z	$$⊢2\in \mathbb{Z}$$
20	19	a1i	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to 2\in \mathbb{Z}$$
21	12 18 20	cxpexpzd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\sqrt{A}}^2={\sqrt{A}}^2$$
22		sqrtth	$$⊢A\in ℂ\to {\sqrt{A}}^2=A$$
23	22	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\sqrt{A}}^2=A$$
24	21 23	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\sqrt{A}}^2=A$$
25	24	expcom	$$⊢A\ne 0\to \left(A\in ℂ\to {\sqrt{A}}^2=A\right)$$
26	10 25	pm2.61ine	$$⊢A\in ℂ\to {\sqrt{A}}^2=A$$