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

Proof

Step	Hyp	Ref	Expression
1		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
2		0cxp	⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 0 ↑𝑐 2 ) = 0 )
3	1 2	ax-mp	⊢ ( 0 ↑𝑐 2 ) = 0
4		fveq2	⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = ( √ ‘ 0 ) )
5		sqrt0	⊢ ( √ ‘ 0 ) = 0
6	4 5	eqtrdi	⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = 0 )
7	6	oveq1d	⊢ ( 𝐴 = 0 → ( ( √ ‘ 𝐴 ) ↑𝑐 2 ) = ( 0 ↑𝑐 2 ) )
8		id	⊢ ( 𝐴 = 0 → 𝐴 = 0 )
9	3 7 8	3eqtr4a	⊢ ( 𝐴 = 0 → ( ( √ ‘ 𝐴 ) ↑𝑐 2 ) = 𝐴 )
10	9	a1d	⊢ ( 𝐴 = 0 → ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) ↑𝑐 2 ) = 𝐴 ) )
11		sqrtcl	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) ∈ ℂ )
12	11	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( √ ‘ 𝐴 ) ∈ ℂ )
13		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( √ ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℂ )
14		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( √ ‘ 𝐴 ) = 0 ) → ( √ ‘ 𝐴 ) = 0 )
15	13 14	sqr00d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( √ ‘ 𝐴 ) = 0 ) → 𝐴 = 0 )
16	15	ex	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) = 0 → 𝐴 = 0 ) )
17	16	necon3d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ≠ 0 → ( √ ‘ 𝐴 ) ≠ 0 ) )
18	17	imp	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( √ ‘ 𝐴 ) ≠ 0 )
19		2z	⊢ 2 ∈ ℤ
20	19	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 2 ∈ ℤ )
21	12 18 20	cxpexpzd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( √ ‘ 𝐴 ) ↑𝑐 2 ) = ( ( √ ‘ 𝐴 ) ↑ 2 ) )
22		sqrtth	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
23	22	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
24	21 23	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( √ ‘ 𝐴 ) ↑𝑐 2 ) = 𝐴 )
25	24	expcom	⊢ ( 𝐴 ≠ 0 → ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) ↑𝑐 2 ) = 𝐴 ) )
26	10 25	pm2.61ine	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) ↑𝑐 2 ) = 𝐴 )