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	$$⊢\left(A\in ℂ\wedge B\in {\mathbb{N}}_0\right)\to B{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^B$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=0\to x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=0{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A$$
2		oveq2	$$⊢x=0\to A^x=A^0$$
3	1 2	eqeq12d	$$⊢x=0\to \left(x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^x\leftrightarrow 0{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^0\right)$$
4	3	imbi2d	$$⊢x=0\to \left(\left(A\in ℂ\to x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^x\right)\leftrightarrow \left(A\in ℂ\to 0{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^0\right)\right)$$
5		oveq1	$$⊢x=y\to x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A$$
6		oveq2	$$⊢x=y\to A^x=A^y$$
7	5 6	eqeq12d	$$⊢x=y\to \left(x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^x\leftrightarrow y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^y\right)$$
8	7	imbi2d	$$⊢x=y\to \left(\left(A\in ℂ\to x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^x\right)\leftrightarrow \left(A\in ℂ\to y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^y\right)\right)$$
9		oveq1	$$⊢x=y+1\to x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=\left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A$$
10		oveq2	$$⊢x=y+1\to A^x=A^{y+1}$$
11	9 10	eqeq12d	$$⊢x=y+1\to \left(x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^x\leftrightarrow \left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^{y+1}\right)$$
12	11	imbi2d	$$⊢x=y+1\to \left(\left(A\in ℂ\to x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^x\right)\leftrightarrow \left(A\in ℂ\to \left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^{y+1}\right)\right)$$
13		oveq1	$$⊢x=B\to x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=B{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A$$
14		oveq2	$$⊢x=B\to A^x=A^B$$
15	13 14	eqeq12d	$$⊢x=B\to \left(x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^x\leftrightarrow B{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^B\right)$$
16	15	imbi2d	$$⊢x=B\to \left(\left(A\in ℂ\to x{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^x\right)\leftrightarrow \left(A\in ℂ\to B{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^B\right)\right)$$
17		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
18		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
19	17 18	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
20		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
21	17 20	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
22		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}={\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
23	19 21 22	mulg0	$$⊢A\in ℂ\to 0{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=1$$
24		exp0	$$⊢A\in ℂ\to A^0=1$$
25	23 24	eqtr4d	$$⊢A\in ℂ\to 0{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^0$$
26		oveq1	$$⊢y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^y\to \left(y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A\right)A=A^{y}A$$
27		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
28	17	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
29	27 28	ax-mp	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
30		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
31	17 30	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
32	19 22 31	mulgnn0p1	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge A\in ℂ\right)\to \left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=\left(y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A\right)A$$
33	29 32	mp3an1	$$⊢\left(y\in {\mathbb{N}}_0\wedge A\in ℂ\right)\to \left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=\left(y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A\right)A$$
34	33	ancoms	$$⊢\left(A\in ℂ\wedge y\in {\mathbb{N}}_0\right)\to \left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=\left(y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A\right)A$$
35		expp1	$$⊢\left(A\in ℂ\wedge y\in {\mathbb{N}}_0\right)\to A^{y+1}=A^{y}A$$
36	34 35	eqeq12d	$$⊢\left(A\in ℂ\wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^{y+1}\leftrightarrow \left(y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A\right)A=A^{y}A\right)$$
37	26 36	syl5ibr	$$⊢\left(A\in ℂ\wedge y\in {\mathbb{N}}_0\right)\to \left(y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^y\to \left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^{y+1}\right)$$
38	37	expcom	$$⊢y\in {\mathbb{N}}_0\to \left(A\in ℂ\to \left(y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^y\to \left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^{y+1}\right)\right)$$
39	38	a2d	$$⊢y\in {\mathbb{N}}_0\to \left(\left(A\in ℂ\to y{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^y\right)\to \left(A\in ℂ\to \left(y+1\right){\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^{y+1}\right)\right)$$
40	4 8 12 16 25 39	nn0ind	$$⊢B\in {\mathbb{N}}_0\to \left(A\in ℂ\to B{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^B\right)$$
41	40	impcom	$$⊢\left(A\in ℂ\wedge B\in {\mathbb{N}}_0\right)\to B{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^B$$