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	$⊢ (A \in ℂ \land N \in ℤ) \to e^{N A} = {e^{A}}^{N}$

Proof

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

Metamath Proof Explorer

Theorem efexp

Proof