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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( exp ‘ ( 𝑁 · 𝐴 ) ) = ( ( exp ‘ 𝐴 ) ↑ 𝑁 ) )

Proof

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