zexpgcd

Description: Exponentiation distributes over gcd. zgcdsq extended to nonnegative exponents. nn0expgcd extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023)

		Ref	Expression
	Assertion	zexpgcd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$

Proof

Step	Hyp	Ref	Expression
1		gcdabs	$⊢ (A \in ℤ \land B \in ℤ) \to \|A\| \gcd \|B\| = A \gcd B$
2	1	3adant3	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to \|A\| \gcd \|B\| = A \gcd B$
3	2	eqcomd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to A \gcd B = \|A\| \gcd \|B\|$
4	3	oveq1d	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} = {(\|A\| \gcd \|B\|)}^{N}$
5		nn0abscl	$⊢ A \in ℤ \to \|A\| \in ℕ_{0}$
6		nn0abscl	$⊢ B \in ℤ \to \|B\| \in ℕ_{0}$
7		id	$⊢ N \in ℕ_{0} \to N \in ℕ_{0}$
8		nn0expgcd	$⊢ (\|A\| \in ℕ_{0} \land \|B\| \in ℕ_{0} \land N \in ℕ_{0}) \to {(\|A\| \gcd \|B\|)}^{N} = {\|A\|}^{N} \gcd {\|B\|}^{N}$
9	5 6 7 8	syl3an	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to {(\|A\| \gcd \|B\|)}^{N} = {\|A\|}^{N} \gcd {\|B\|}^{N}$
10		zcn	$⊢ A \in ℤ \to A \in ℂ$
11	10	3ad2ant1	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to A \in ℂ$
12		simp3	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
13	11 12	absexpd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to \|A^{N}\| = {\|A\|}^{N}$
14	13	eqcomd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to {\|A\|}^{N} = \|A^{N}\|$
15		zcn	$⊢ B \in ℤ \to B \in ℂ$
16	15	3ad2ant2	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to B \in ℂ$
17	16 12	absexpd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to \|B^{N}\| = {\|B\|}^{N}$
18	17	eqcomd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to {\|B\|}^{N} = \|B^{N}\|$
19	14 18	oveq12d	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to {\|A\|}^{N} \gcd {\|B\|}^{N} = \|A^{N}\| \gcd \|B^{N}\|$
20		zexpcl	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A^{N} \in ℤ$
21	20	3adant2	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to A^{N} \in ℤ$
22		zexpcl	$⊢ (B \in ℤ \land N \in ℕ_{0}) \to B^{N} \in ℤ$
23	22	3adant1	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to B^{N} \in ℤ$
24		gcdabs	$⊢ (A^{N} \in ℤ \land B^{N} \in ℤ) \to \|A^{N}\| \gcd \|B^{N}\| = A^{N} \gcd B^{N}$
25	21 23 24	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to \|A^{N}\| \gcd \|B^{N}\| = A^{N} \gcd B^{N}$
26	19 25	eqtrd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to {\|A\|}^{N} \gcd {\|B\|}^{N} = A^{N} \gcd B^{N}$
27	4 9 26	3eqtrd	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$

Metamath Proof Explorer

Theorem zexpgcd

Proof