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 
|- ( A e. CC -> ( ( sqrt ` A ) ^c 2 ) = A )

Proof

Step Hyp Ref Expression
1 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
2 0cxp 
 |-  ( ( 2 e. CC /\ 2 =/= 0 ) -> ( 0 ^c 2 ) = 0 )
3 1 2 ax-mp 
 |-  ( 0 ^c 2 ) = 0
4 fveq2 
 |-  ( A = 0 -> ( sqrt ` A ) = ( sqrt ` 0 ) )
5 sqrt0 
 |-  ( sqrt ` 0 ) = 0
6 4 5 eqtrdi 
 |-  ( A = 0 -> ( sqrt ` A ) = 0 )
7 6 oveq1d 
 |-  ( A = 0 -> ( ( sqrt ` A ) ^c 2 ) = ( 0 ^c 2 ) )
8 id 
 |-  ( A = 0 -> A = 0 )
9 3 7 8 3eqtr4a 
 |-  ( A = 0 -> ( ( sqrt ` A ) ^c 2 ) = A )
10 9 a1d 
 |-  ( A = 0 -> ( A e. CC -> ( ( sqrt ` A ) ^c 2 ) = A ) )
11 sqrtcl 
 |-  ( A e. CC -> ( sqrt ` A ) e. CC )
12 11 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( sqrt ` A ) e. CC )
13 simpl 
 |-  ( ( A e. CC /\ ( sqrt ` A ) = 0 ) -> A e. CC )
14 simpr 
 |-  ( ( A e. CC /\ ( sqrt ` A ) = 0 ) -> ( sqrt ` A ) = 0 )
15 13 14 sqr00d 
 |-  ( ( A e. CC /\ ( sqrt ` A ) = 0 ) -> A = 0 )
16 15 ex 
 |-  ( A e. CC -> ( ( sqrt ` A ) = 0 -> A = 0 ) )
17 16 necon3d 
 |-  ( A e. CC -> ( A =/= 0 -> ( sqrt ` A ) =/= 0 ) )
18 17 imp 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( sqrt ` A ) =/= 0 )
19 2z 
 |-  2 e. ZZ
20 19 a1i 
 |-  ( ( A e. CC /\ A =/= 0 ) -> 2 e. ZZ )
21 12 18 20 cxpexpzd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( sqrt ` A ) ^c 2 ) = ( ( sqrt ` A ) ^ 2 ) )
22 sqrtth 
 |-  ( A e. CC -> ( ( sqrt ` A ) ^ 2 ) = A )
23 22 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( sqrt ` A ) ^ 2 ) = A )
24 21 23 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( sqrt ` A ) ^c 2 ) = A )
25 24 expcom 
 |-  ( A =/= 0 -> ( A e. CC -> ( ( sqrt ` A ) ^c 2 ) = A ) )
26 10 25 pm2.61ine 
 |-  ( A e. CC -> ( ( sqrt ` A ) ^c 2 ) = A )