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	imbitrrid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ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 ) ) 𝐴 ) = ( 𝐴 ↑ 𝐵 ) )