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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐵 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 0 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) )
2 oveq2 ⊢ ( 𝑥 = 0 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 0 ) )
3 1 2 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑥 ) ↔ ( 0 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 0 ) ) )
4 3 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝐴 ∈ ℂ → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑥 ) ) ↔ ( 𝐴 ∈ ℂ → ( 0 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 0 ) ) ) )
5 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) )
6 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑦 ) )
7 5 6 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑥 ) ↔ ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑦 ) ) )
8 7 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ ℂ → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑥 ) ) ↔ ( 𝐴 ∈ ℂ → ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑦 ) ) ) )
9 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) )
10 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ ( 𝑦 + 1 ) ) )
11 9 10 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑥 ) ↔ ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ ( 𝑦 + 1 ) ) ) )
12 11 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐴 ∈ ℂ → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑥 ) ) ↔ ( 𝐴 ∈ ℂ → ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ ( 𝑦 + 1 ) ) ) ) )
13 oveq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐵 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) )
14 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝐵 ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑥 ) ↔ ( 𝐵 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝐵 ) ) )
16 15 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ ℂ → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑥 ) ) ↔ ( 𝐴 ∈ ℂ → ( 𝐵 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝐵 ) ) ) )
17 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
18 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
19 17 18 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
20 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
21 17 20 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
22 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
23 19 21 22 mulg0 ⊢ ( 𝐴 ∈ ℂ → ( 0 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = 1 )
24 exp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
25 23 24 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( 0 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 0 ) )
26 oveq1 ⊢ ( ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑦 ) → ( ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) · 𝐴 ) = ( ( 𝐴 ↑ 𝑦 ) · 𝐴 ) )
27 cnring ⊢ ℂfld ∈ Ring
28 17 ringmgp ⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
29 27 28 ax-mp ⊢ ( mulGrp ‘ ℂfld ) ∈ Mnd
30 cnfldmul ⊢ · = ( .r ‘ ℂfld )
31 17 30 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
32 19 22 31 mulgnn0p1 ⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) · 𝐴 ) )
33 29 32 mp3an1 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) · 𝐴 ) )
34 33 ancoms ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) · 𝐴 ) )
35 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑦 + 1 ) ) = ( ( 𝐴 ↑ 𝑦 ) · 𝐴 ) )
36 34 35 eqeq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ ( 𝑦 + 1 ) ) ↔ ( ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) · 𝐴 ) = ( ( 𝐴 ↑ 𝑦 ) · 𝐴 ) ) )
37 26 36 syl5ibr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑦 ) → ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ ( 𝑦 + 1 ) ) ) )
38 37 expcom ⊢ ( 𝑦 ∈ ℕ0 → ( 𝐴 ∈ ℂ → ( ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑦 ) → ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ ( 𝑦 + 1 ) ) ) ) )
39 38 a2d ⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝐴 ∈ ℂ → ( 𝑦 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝑦 ) ) → ( 𝐴 ∈ ℂ → ( ( 𝑦 + 1 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ ( 𝑦 + 1 ) ) ) ) )
40 4 8 12 16 25 39 nn0ind ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐴 ∈ ℂ → ( 𝐵 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝐵 ) ) )
41 40 impcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐵 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 𝐵 ) )