absexpz

Description: Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015)

		Ref	Expression
	Assertion	absexpz	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to \|A^{N}\| = {\|A\|}^{N}$

Proof

Step	Hyp	Ref	Expression
1		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
2		absexp	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \|A^{N}\| = {\|A\|}^{N}$
3	2	ex	$⊢ A \in ℂ \to (N \in ℕ_{0} \to \|A^{N}\| = {\|A\|}^{N})$
4	3	adantr	$⊢ (A \in ℂ \land A \neq 0) \to (N \in ℕ_{0} \to \|A^{N}\| = {\|A\|}^{N})$
5		1cnd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to 1 \in ℂ$
6		simpll	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to A \in ℂ$
7		nnnn0	$⊢ - N \in ℕ \to - N \in ℕ_{0}$
8	7	ad2antll	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ_{0}$
9	6 8	expcld	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to A^{- N} \in ℂ$
10		simplr	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to A \neq 0$
11		nnz	$⊢ - N \in ℕ \to - N \in ℤ$
12	11	ad2antll	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℤ$
13	6 10 12	expne0d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to A^{- N} \neq 0$
14		absdiv	$⊢ (1 \in ℂ \land A^{- N} \in ℂ \land A^{- N} \neq 0) \to \|\frac{1}{A^{- N}}\| = \frac{\|1\|}{\|A^{- N}\|}$
15	5 9 13 14	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \|\frac{1}{A^{- N}}\| = \frac{\|1\|}{\|A^{- N}\|}$
16		abs1	$⊢ \|1\| = 1$
17	16	oveq1i	$⊢ \frac{\|1\|}{\|A^{- N}\|} = \frac{1}{\|A^{- N}\|}$
18		absexp	$⊢ (A \in ℂ \land - N \in ℕ_{0}) \to \|A^{- N}\| = {\|A\|}^{- N}$
19	6 8 18	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \|A^{- N}\| = {\|A\|}^{- N}$
20	19	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{\|A^{- N}\|} = \frac{1}{{\|A\|}^{- N}}$
21	17 20	syl5eq	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \frac{\|1\|}{\|A^{- N}\|} = \frac{1}{{\|A\|}^{- N}}$
22	15 21	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \|\frac{1}{A^{- N}}\| = \frac{1}{{\|A\|}^{- N}}$
23		simprl	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℝ$
24	23	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℂ$
25		expneg2	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to A^{N} = \frac{1}{A^{- N}}$
26	6 24 8 25	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to A^{N} = \frac{1}{A^{- N}}$
27	26	fveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \|A^{N}\| = \|\frac{1}{A^{- N}}\|$
28		abscl	$⊢ A \in ℂ \to \|A\| \in ℝ$
29	28	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \|A\| \in ℝ$
30	29	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \|A\| \in ℂ$
31		expneg2	$⊢ (\|A\| \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to {\|A\|}^{N} = \frac{1}{{\|A\|}^{- N}}$
32	30 24 8 31	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to {\|A\|}^{N} = \frac{1}{{\|A\|}^{- N}}$
33	22 27 32	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to \|A^{N}\| = {\|A\|}^{N}$
34	33	ex	$⊢ (A \in ℂ \land A \neq 0) \to ((N \in ℝ \land - N \in ℕ) \to \|A^{N}\| = {\|A\|}^{N})$
35	4 34	jaod	$⊢ (A \in ℂ \land A \neq 0) \to ((N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ)) \to \|A^{N}\| = {\|A\|}^{N})$
36	35	3impia	$⊢ (A \in ℂ \land A \neq 0 \land (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))) \to \|A^{N}\| = {\|A\|}^{N}$
37	1 36	syl3an3b	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to \|A^{N}\| = {\|A\|}^{N}$

Metamath Proof Explorer

Theorem absexpz

Proof