Metamath Proof Explorer

Theorem cnfldexp

Description: The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Assertion cnfldexp 
|- ( ( A e. CC /\ B e. NN0 ) -> ( B ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ B ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = 0 -> ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( 0 ( .g ` ( mulGrp ` CCfld ) ) A ) )
2 oveq2 
 |-  ( x = 0 -> ( A ^ x ) = ( A ^ 0 ) )
3 1 2 eqeq12d 
 |-  ( x = 0 -> ( ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ x ) <-> ( 0 ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ 0 ) ) )
4 3 imbi2d 
 |-  ( x = 0 -> ( ( A e. CC -> ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ x ) ) <-> ( A e. CC -> ( 0 ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ 0 ) ) ) )
5 oveq1 
 |-  ( x = y -> ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( y ( .g ` ( mulGrp ` CCfld ) ) A ) )
6 oveq2 
 |-  ( x = y -> ( A ^ x ) = ( A ^ y ) )
7 5 6 eqeq12d 
 |-  ( x = y -> ( ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ x ) <-> ( y ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ y ) ) )
8 7 imbi2d 
 |-  ( x = y -> ( ( A e. CC -> ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ x ) ) <-> ( A e. CC -> ( y ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ y ) ) ) )
9 oveq1 
 |-  ( x = ( y + 1 ) -> ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) )
10 oveq2 
 |-  ( x = ( y + 1 ) -> ( A ^ x ) = ( A ^ ( y + 1 ) ) )
11 9 10 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ x ) <-> ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ ( y + 1 ) ) ) )
12 11 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( A e. CC -> ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ x ) ) <-> ( A e. CC -> ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ ( y + 1 ) ) ) ) )
13 oveq1 
 |-  ( x = B -> ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( B ( .g ` ( mulGrp ` CCfld ) ) A ) )
14 oveq2 
 |-  ( x = B -> ( A ^ x ) = ( A ^ B ) )
15 13 14 eqeq12d 
 |-  ( x = B -> ( ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ x ) <-> ( B ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ B ) ) )
16 15 imbi2d 
 |-  ( x = B -> ( ( A e. CC -> ( x ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ x ) ) <-> ( A e. CC -> ( B ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ B ) ) ) )
17 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
18 cnfldbas 
 |-  CC = ( Base ` CCfld )
19 17 18 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
20 cnfld1 
 |-  1 = ( 1r ` CCfld )
21 17 20 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
22 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
23 19 21 22 mulg0 
 |-  ( A e. CC -> ( 0 ( .g ` ( mulGrp ` CCfld ) ) A ) = 1 )
24 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
25 23 24 eqtr4d 
 |-  ( A e. CC -> ( 0 ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ 0 ) )
26 oveq1 
 |-  ( ( y ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ y ) -> ( ( y ( .g ` ( mulGrp ` CCfld ) ) A ) x. A ) = ( ( A ^ y ) x. A ) )
27 cnring 
 |-  CCfld e. Ring
28 17 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
29 27 28 ax-mp 
 |-  ( mulGrp ` CCfld ) e. Mnd
30 cnfldmul 
 |-  x. = ( .r ` CCfld )
31 17 30 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
32 19 22 31 mulgnn0p1 
 |-  ( ( ( mulGrp ` CCfld ) e. Mnd /\ y e. NN0 /\ A e. CC ) -> ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( ( y ( .g ` ( mulGrp ` CCfld ) ) A ) x. A ) )
33 29 32 mp3an1 
 |-  ( ( y e. NN0 /\ A e. CC ) -> ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( ( y ( .g ` ( mulGrp ` CCfld ) ) A ) x. A ) )
34 33 ancoms 
 |-  ( ( A e. CC /\ y e. NN0 ) -> ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( ( y ( .g ` ( mulGrp ` CCfld ) ) A ) x. A ) )
35 expp1 
 |-  ( ( A e. CC /\ y e. NN0 ) -> ( A ^ ( y + 1 ) ) = ( ( A ^ y ) x. A ) )
36 34 35 eqeq12d 
 |-  ( ( A e. CC /\ y e. NN0 ) -> ( ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ ( y + 1 ) ) <-> ( ( y ( .g ` ( mulGrp ` CCfld ) ) A ) x. A ) = ( ( A ^ y ) x. A ) ) )
37 26 36 syl5ibr 
 |-  ( ( A e. CC /\ y e. NN0 ) -> ( ( y ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ y ) -> ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ ( y + 1 ) ) ) )
38 37 expcom 
 |-  ( y e. NN0 -> ( A e. CC -> ( ( y ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ y ) -> ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ ( y + 1 ) ) ) ) )
39 38 a2d 
 |-  ( y e. NN0 -> ( ( A e. CC -> ( y ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ y ) ) -> ( A e. CC -> ( ( y + 1 ) ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ ( y + 1 ) ) ) ) )
40 4 8 12 16 25 39 nn0ind 
 |-  ( B e. NN0 -> ( A e. CC -> ( B ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ B ) ) )
41 40 impcom 
 |-  ( ( A e. CC /\ B e. NN0 ) -> ( B ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ B ) )