Metamath Proof Explorer


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 ) = 𝐴 )