This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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