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	$⊢ (2 \in ℂ \land 2 \neq 0)$
2		0cxp	$⊢ (2 \in ℂ \land 2 \neq 0) \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 (A \in ℂ \to {\sqrt{A}}^{2} = A)$
11		sqrtcl	$⊢ A \in ℂ \to \sqrt{A} \in ℂ$
12	11	adantr	$⊢ (A \in ℂ \land A \neq 0) \to \sqrt{A} \in ℂ$
13		simpl	$⊢ (A \in ℂ \land \sqrt{A} = 0) \to A \in ℂ$
14		simpr	$⊢ (A \in ℂ \land \sqrt{A} = 0) \to \sqrt{A} = 0$
15	13 14	sqr00d	$⊢ (A \in ℂ \land \sqrt{A} = 0) \to A = 0$
16	15	ex	$⊢ A \in ℂ \to (\sqrt{A} = 0 \to A = 0)$
17	16	necon3d	$⊢ A \in ℂ \to (A \neq 0 \to \sqrt{A} \neq 0)$
18	17	imp	$⊢ (A \in ℂ \land A \neq 0) \to \sqrt{A} \neq 0$
19		2z	$⊢ 2 \in ℤ$
20	19	a1i	$⊢ (A \in ℂ \land A \neq 0) \to 2 \in ℤ$
21	12 18 20	cxpexpzd	$⊢ (A \in ℂ \land A \neq 0) \to {\sqrt{A}}^{2} = {\sqrt{A}}^{2}$
22		sqrtth	$⊢ A \in ℂ \to {\sqrt{A}}^{2} = A$
23	22	adantr	$⊢ (A \in ℂ \land A \neq 0) \to {\sqrt{A}}^{2} = A$
24	21 23	eqtrd	$⊢ (A \in ℂ \land A \neq 0) \to {\sqrt{A}}^{2} = A$
25	24	expcom	$⊢ A \neq 0 \to (A \in ℂ \to {\sqrt{A}}^{2} = A)$
26	10 25	pm2.61ine	$⊢ A \in ℂ \to {\sqrt{A}}^{2} = A$

Metamath Proof Explorer

Theorem cxpsqrtth

Proof