Theorem absexp

Description: Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006)

	Ref	Expression
Assertion	absexp	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left|A^N\right|={\left|A\right|}^N$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢j=0\to A^j=A^0$$
2	1	fveq2d	$$⊢j=0\to \left|A^j\right|=\left|A^0\right|$$
3		oveq2	$$⊢j=0\to {\left|A\right|}^j={\left|A\right|}^0$$
4	2 3	eqeq12d	$$⊢j=0\to \left(\left|A^j\right|={\left|A\right|}^j\leftrightarrow \left|A^0\right|={\left|A\right|}^0\right)$$
5		oveq2	$$⊢j=k\to A^j=A^k$$
6	5	fveq2d	$$⊢j=k\to \left|A^j\right|=\left|A^k\right|$$
7		oveq2	$$⊢j=k\to {\left|A\right|}^j={\left|A\right|}^k$$
8	6 7	eqeq12d	$$⊢j=k\to \left(\left|A^j\right|={\left|A\right|}^j\leftrightarrow \left|A^k\right|={\left|A\right|}^k\right)$$
9		oveq2	$$⊢j=k+1\to A^j=A^{k+1}$$
10	9	fveq2d	$$⊢j=k+1\to \left|A^j\right|=\left|A^{k+1}\right|$$
11		oveq2	$$⊢j=k+1\to {\left|A\right|}^j={\left|A\right|}^{k+1}$$
12	10 11	eqeq12d	$$⊢j=k+1\to \left(\left|A^j\right|={\left|A\right|}^j\leftrightarrow \left|A^{k+1}\right|={\left|A\right|}^{k+1}\right)$$
13		oveq2	$$⊢j=N\to A^j=A^N$$
14	13	fveq2d	$$⊢j=N\to \left|A^j\right|=\left|A^N\right|$$
15		oveq2	$$⊢j=N\to {\left|A\right|}^j={\left|A\right|}^N$$
16	14 15	eqeq12d	$$⊢j=N\to \left(\left|A^j\right|={\left|A\right|}^j\leftrightarrow \left|A^N\right|={\left|A\right|}^N\right)$$
17		abs1	$$⊢\left|1\right|=1$$
18		exp0	$$⊢A\in ℂ\to A^0=1$$
19	18	fveq2d	$$⊢A\in ℂ\to \left|A^0\right|=\left|1\right|$$
20		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
21	20	recnd	$$⊢A\in ℂ\to \left|A\right|\in ℂ$$
22	21	exp0d	$$⊢A\in ℂ\to {\left|A\right|}^0=1$$
23	17 19 22	3eqtr4a	$$⊢A\in ℂ\to \left|A^0\right|={\left|A\right|}^0$$
24		oveq1	$$⊢\left|A^k\right|={\left|A\right|}^k\to \left|A^k\right|\left|A\right|={\left|A\right|}^k\left|A\right|$$
25	24	adantl	$$⊢\left(\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\wedge \left|A^k\right|={\left|A\right|}^k\right)\to \left|A^k\right|\left|A\right|={\left|A\right|}^k\left|A\right|$$
26		expp1	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^{k+1}=A^{k}A$$
27	26	fveq2d	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left|A^{k+1}\right|=\left|A^{k}A\right|$$
28		expcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
29		simpl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A\in ℂ$$
30		absmul	$$⊢\left(A^k\in ℂ\wedge A\in ℂ\right)\to \left|A^{k}A\right|=\left|A^k\right|\left|A\right|$$
31	28 29 30	syl2anc	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left|A^{k}A\right|=\left|A^k\right|\left|A\right|$$
32	27 31	eqtrd	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left|A^{k+1}\right|=\left|A^k\right|\left|A\right|$$
33	32	adantr	$$⊢\left(\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\wedge \left|A^k\right|={\left|A\right|}^k\right)\to \left|A^{k+1}\right|=\left|A^k\right|\left|A\right|$$
34		expp1	$$⊢\left(\left|A\right|\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\left|A\right|}^{k+1}={\left|A\right|}^k\left|A\right|$$
35	21 34	sylan	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\left|A\right|}^{k+1}={\left|A\right|}^k\left|A\right|$$
36	35	adantr	$$⊢\left(\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\wedge \left|A^k\right|={\left|A\right|}^k\right)\to {\left|A\right|}^{k+1}={\left|A\right|}^k\left|A\right|$$
37	25 33 36	3eqtr4d	$$⊢\left(\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\wedge \left|A^k\right|={\left|A\right|}^k\right)\to \left|A^{k+1}\right|={\left|A\right|}^{k+1}$$
38	4 8 12 16 23 37	nn0indd	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left|A^N\right|={\left|A\right|}^N$$