Theorem efexp

Description: The exponential of an integer power. Corollary 15-4.4 of Gleason p. 309, restricted to integers. (Contributed by NM, 13-Jan-2006) (Revised by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Assertion	efexp	$$⊢\left(A\in ℂ\wedge N\in \mathbb{Z}\right)\to {\mathrm{e}}^{NA}={{\mathrm{e}}^A}^N$$

Proof

Step	Hyp	Ref	Expression
1		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
2		mulcom	$$⊢\left(A\in ℂ\wedge N\in ℂ\right)\to A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=NA$$
3	1 2	sylan2	$$⊢\left(A\in ℂ\wedge N\in \mathbb{Z}\right)\to A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=NA$$
4	3	fveq2d	$$⊢\left(A\in ℂ\wedge N\in \mathbb{Z}\right)\to {\mathrm{e}}^{A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={\mathrm{e}}^{NA}$$
5		oveq2	$$⊢j=0\to Aj=A\cdot 0$$
6	5	fveq2d	$$⊢j=0\to {\mathrm{e}}^{Aj}={\mathrm{e}}^{A\cdot 0}$$
7		oveq2	$$⊢j=0\to {{\mathrm{e}}^A}^j={{\mathrm{e}}^A}^0$$
8	6 7	eqeq12d	$$⊢j=0\to \left({\mathrm{e}}^{Aj}={{\mathrm{e}}^A}^j\leftrightarrow {\mathrm{e}}^{A\cdot 0}={{\mathrm{e}}^A}^0\right)$$
9		oveq2	$$⊢j=k\to Aj=Ak$$
10	9	fveq2d	$$⊢j=k\to {\mathrm{e}}^{Aj}={\mathrm{e}}^{Ak}$$
11		oveq2	$$⊢j=k\to {{\mathrm{e}}^A}^j={{\mathrm{e}}^A}^k$$
12	10 11	eqeq12d	$$⊢j=k\to \left({\mathrm{e}}^{Aj}={{\mathrm{e}}^A}^j\leftrightarrow {\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\right)$$
13		oveq2	$$⊢j=k+1\to Aj=A\left(k+1\right)$$
14	13	fveq2d	$$⊢j=k+1\to {\mathrm{e}}^{Aj}={\mathrm{e}}^{A\left(k+1\right)}$$
15		oveq2	$$⊢j=k+1\to {{\mathrm{e}}^A}^j={{\mathrm{e}}^A}^{k+1}$$
16	14 15	eqeq12d	$$⊢j=k+1\to \left({\mathrm{e}}^{Aj}={{\mathrm{e}}^A}^j\leftrightarrow {\mathrm{e}}^{A\left(k+1\right)}={{\mathrm{e}}^A}^{k+1}\right)$$
17		oveq2	$$⊢j=-k\to Aj=A\left(-k\right)$$
18	17	fveq2d	$$⊢j=-k\to {\mathrm{e}}^{Aj}={\mathrm{e}}^{A\left(-k\right)}$$
19		oveq2	$$⊢j=-k\to {{\mathrm{e}}^A}^j={{\mathrm{e}}^A}^{-k}$$
20	18 19	eqeq12d	$$⊢j=-k\to \left({\mathrm{e}}^{Aj}={{\mathrm{e}}^A}^j\leftrightarrow {\mathrm{e}}^{A\left(-k\right)}={{\mathrm{e}}^A}^{-k}\right)$$
21		oveq2	$$⊢j=N\to Aj=A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
22	21	fveq2d	$$⊢j=N\to {\mathrm{e}}^{Aj}={\mathrm{e}}^{A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
23		oveq2	$$⊢j=N\to {{\mathrm{e}}^A}^j={{\mathrm{e}}^A}^N$$
24	22 23	eqeq12d	$$⊢j=N\to \left({\mathrm{e}}^{Aj}={{\mathrm{e}}^A}^j\leftrightarrow {\mathrm{e}}^{A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={{\mathrm{e}}^A}^N\right)$$
25		ef0	$$⊢{\mathrm{e}}^0=1$$
26		mul01	$$⊢A\in ℂ\to A\cdot 0=0$$
27	26	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{A\cdot 0}={\mathrm{e}}^0$$
28		efcl	$$⊢A\in ℂ\to {\mathrm{e}}^A\in ℂ$$
29	28	exp0d	$$⊢A\in ℂ\to {{\mathrm{e}}^A}^0=1$$
30	25 27 29	3eqtr4a	$$⊢A\in ℂ\to {\mathrm{e}}^{A\cdot 0}={{\mathrm{e}}^A}^0$$
31		oveq1	$$⊢{\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\to {\mathrm{e}}^{Ak}{\mathrm{e}}^A={{\mathrm{e}}^A}^k{\mathrm{e}}^A$$
32	31	adantl	$$⊢\left(\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\wedge {\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\right)\to {\mathrm{e}}^{Ak}{\mathrm{e}}^A={{\mathrm{e}}^A}^k{\mathrm{e}}^A$$
33		nn0cn	$$⊢k\in {\mathbb{N}}_0\to k\in ℂ$$
34		ax-1cn	$$⊢1\in ℂ$$
35		adddi	$$⊢\left(A\in ℂ\wedge k\in ℂ\wedge 1\in ℂ\right)\to A\left(k+1\right)=Ak+A\cdot 1$$
36	34 35	mp3an3	$$⊢\left(A\in ℂ\wedge k\in ℂ\right)\to A\left(k+1\right)=Ak+A\cdot 1$$
37		mulrid	$$⊢A\in ℂ\to A\cdot 1=A$$
38	37	adantr	$$⊢\left(A\in ℂ\wedge k\in ℂ\right)\to A\cdot 1=A$$
39	38	oveq2d	$$⊢\left(A\in ℂ\wedge k\in ℂ\right)\to Ak+A\cdot 1=Ak+A$$
40	36 39	eqtrd	$$⊢\left(A\in ℂ\wedge k\in ℂ\right)\to A\left(k+1\right)=Ak+A$$
41	33 40	sylan2	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A\left(k+1\right)=Ak+A$$
42	41	fveq2d	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{e}}^{A\left(k+1\right)}={\mathrm{e}}^{Ak+A}$$
43		mulcl	$$⊢\left(A\in ℂ\wedge k\in ℂ\right)\to Ak\in ℂ$$
44	33 43	sylan2	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to Ak\in ℂ$$
45		simpl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A\in ℂ$$
46		efadd	$$⊢\left(Ak\in ℂ\wedge A\in ℂ\right)\to {\mathrm{e}}^{Ak+A}={\mathrm{e}}^{Ak}{\mathrm{e}}^A$$
47	44 45 46	syl2anc	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{e}}^{Ak+A}={\mathrm{e}}^{Ak}{\mathrm{e}}^A$$
48	42 47	eqtrd	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{e}}^{A\left(k+1\right)}={\mathrm{e}}^{Ak}{\mathrm{e}}^A$$
49	48	adantr	$$⊢\left(\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\wedge {\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\right)\to {\mathrm{e}}^{A\left(k+1\right)}={\mathrm{e}}^{Ak}{\mathrm{e}}^A$$
50		expp1	$$⊢\left({\mathrm{e}}^A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {{\mathrm{e}}^A}^{k+1}={{\mathrm{e}}^A}^k{\mathrm{e}}^A$$
51	28 50	sylan	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {{\mathrm{e}}^A}^{k+1}={{\mathrm{e}}^A}^k{\mathrm{e}}^A$$
52	51	adantr	$$⊢\left(\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\wedge {\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\right)\to {{\mathrm{e}}^A}^{k+1}={{\mathrm{e}}^A}^k{\mathrm{e}}^A$$
53	32 49 52	3eqtr4d	$$⊢\left(\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\wedge {\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\right)\to {\mathrm{e}}^{A\left(k+1\right)}={{\mathrm{e}}^A}^{k+1}$$
54	53	exp31	$$⊢A\in ℂ\to \left(k\in {\mathbb{N}}_0\to \left({\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\to {\mathrm{e}}^{A\left(k+1\right)}={{\mathrm{e}}^A}^{k+1}\right)\right)$$
55		oveq2	$$⊢{\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\to \frac{1}{{\mathrm{e}}^{Ak}}=\frac{1}{{{\mathrm{e}}^A}^k}$$
56		nncn	$$⊢k\in \mathbb{N}\to k\in ℂ$$
57		mulneg2	$$⊢\left(A\in ℂ\wedge k\in ℂ\right)\to A\left(-k\right)=-Ak$$
58	56 57	sylan2	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to A\left(-k\right)=-Ak$$
59	58	fveq2d	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to {\mathrm{e}}^{A\left(-k\right)}={\mathrm{e}}^{-Ak}$$
60	56 43	sylan2	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to Ak\in ℂ$$
61		efneg	$$⊢Ak\in ℂ\to {\mathrm{e}}^{-Ak}=\frac{1}{{\mathrm{e}}^{Ak}}$$
62	60 61	syl	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to {\mathrm{e}}^{-Ak}=\frac{1}{{\mathrm{e}}^{Ak}}$$
63	59 62	eqtrd	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to {\mathrm{e}}^{A\left(-k\right)}=\frac{1}{{\mathrm{e}}^{Ak}}$$
64		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
65		expneg	$$⊢\left({\mathrm{e}}^A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {{\mathrm{e}}^A}^{-k}=\frac{1}{{{\mathrm{e}}^A}^k}$$
66	28 64 65	syl2an	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to {{\mathrm{e}}^A}^{-k}=\frac{1}{{{\mathrm{e}}^A}^k}$$
67	63 66	eqeq12d	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to \left({\mathrm{e}}^{A\left(-k\right)}={{\mathrm{e}}^A}^{-k}\leftrightarrow \frac{1}{{\mathrm{e}}^{Ak}}=\frac{1}{{{\mathrm{e}}^A}^k}\right)$$
68	55 67	imbitrrid	$$⊢\left(A\in ℂ\wedge k\in \mathbb{N}\right)\to \left({\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\to {\mathrm{e}}^{A\left(-k\right)}={{\mathrm{e}}^A}^{-k}\right)$$
69	68	ex	$$⊢A\in ℂ\to \left(k\in \mathbb{N}\to \left({\mathrm{e}}^{Ak}={{\mathrm{e}}^A}^k\to {\mathrm{e}}^{A\left(-k\right)}={{\mathrm{e}}^A}^{-k}\right)\right)$$
70	8 12 16 20 24 30 54 69	zindd	$$⊢A\in ℂ\to \left(N\in \mathbb{Z}\to {\mathrm{e}}^{A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={{\mathrm{e}}^A}^N\right)$$
71	70	imp	$$⊢\left(A\in ℂ\wedge N\in \mathbb{Z}\right)\to {\mathrm{e}}^{A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={{\mathrm{e}}^A}^N$$
72	4 71	eqtr3d	$$⊢\left(A\in ℂ\wedge N\in \mathbb{Z}\right)\to {\mathrm{e}}^{NA}={{\mathrm{e}}^A}^N$$