expgcd

Description: Exponentiation distributes over GCD. sqgcd extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023)

		Ref	Expression
	Assertion	expgcd	$⊢ (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		gcdnncl	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℕ$
2	1	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A \gcd B \in ℕ$
3		simp3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
4	2 3	nnexpcld	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} \in ℕ$
5	4	nncnd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} \in ℂ$
6	5	mulid1d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} \cdot 1 = {(A \gcd B)}^{N}$
7		nnexpcl	$⊢ (A \in ℕ \land N \in ℕ_{0}) \to A^{N} \in ℕ$
8	7	3adant2	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A^{N} \in ℕ$
9	8	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A^{N} \in ℤ$
10		nnexpcl	$⊢ (B \in ℕ \land N \in ℕ_{0}) \to B^{N} \in ℕ$
11	10	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to B^{N} \in ℕ$
12	11	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to B^{N} \in ℤ$
13		simpl	$⊢ (A \in ℕ \land B \in ℕ) \to A \in ℕ$
14	13	nnzd	$⊢ (A \in ℕ \land B \in ℕ) \to A \in ℤ$
15		simpr	$⊢ (A \in ℕ \land B \in ℕ) \to B \in ℕ$
16	15	nnzd	$⊢ (A \in ℕ \land B \in ℕ) \to B \in ℤ$
17		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
18	14 16 17	syl2anc	$⊢ (A \in ℕ \land B \in ℕ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
19	18	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
20	19	simpld	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to (A \gcd B) ∥ A$
21	2	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A \gcd B \in ℤ$
22		simp1	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A \in ℕ$
23	22	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A \in ℤ$
24		dvdsexpim	$⊢ (A \gcd B \in ℤ \land A \in ℤ \land N \in ℕ_{0}) \to ((A \gcd B) ∥ A \to {(A \gcd B)}^{N} ∥ A^{N})$
25	21 23 3 24	syl3anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to ((A \gcd B) ∥ A \to {(A \gcd B)}^{N} ∥ A^{N})$
26	20 25	mpd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} ∥ A^{N}$
27	19	simprd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to (A \gcd B) ∥ B$
28		simp2	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to B \in ℕ$
29	28	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to B \in ℤ$
30		dvdsexpim	$⊢ (A \gcd B \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to ((A \gcd B) ∥ B \to {(A \gcd B)}^{N} ∥ B^{N})$
31	21 29 3 30	syl3anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to ((A \gcd B) ∥ B \to {(A \gcd B)}^{N} ∥ B^{N})$
32	27 31	mpd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} ∥ B^{N}$
33		gcddiv	$⊢ ((A^{N} \in ℤ \land B^{N} \in ℤ \land {(A \gcd B)}^{N} \in ℕ) \land ({(A \gcd B)}^{N} ∥ A^{N} \land {(A \gcd B)}^{N} ∥ B^{N})) \to \frac{A^{N} \gcd B^{N}}{{(A \gcd B)}^{N}} = (\frac{A^{N}}{{(A \gcd B)}^{N}}) \gcd (\frac{B^{N}}{{(A \gcd B)}^{N}})$
34	9 12 4 26 32 33	syl32anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to \frac{A^{N} \gcd B^{N}}{{(A \gcd B)}^{N}} = (\frac{A^{N}}{{(A \gcd B)}^{N}}) \gcd (\frac{B^{N}}{{(A \gcd B)}^{N}})$
35		nncn	$⊢ A \in ℕ \to A \in ℂ$
36	35	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A \in ℂ$
37	2	nncnd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A \gcd B \in ℂ$
38	2	nnne0d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A \gcd B \neq 0$
39	36 37 38 3	expdivd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(\frac{A}{A \gcd B})}^{N} = \frac{A^{N}}{{(A \gcd B)}^{N}}$
40		nncn	$⊢ B \in ℕ \to B \in ℂ$
41	40	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to B \in ℂ$
42	41 37 38 3	expdivd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(\frac{B}{A \gcd B})}^{N} = \frac{B^{N}}{{(A \gcd B)}^{N}}$
43	39 42	oveq12d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(\frac{A}{A \gcd B})}^{N} \gcd {(\frac{B}{A \gcd B})}^{N} = (\frac{A^{N}}{{(A \gcd B)}^{N}}) \gcd (\frac{B^{N}}{{(A \gcd B)}^{N}})$
44		gcddiv	$⊢ ((A \in ℤ \land B \in ℤ \land A \gcd B \in ℕ) \land ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)) \to \frac{A \gcd B}{A \gcd B} = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
45	23 29 2 19 44	syl31anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to \frac{A \gcd B}{A \gcd B} = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
46	37 38	dividd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to \frac{A \gcd B}{A \gcd B} = 1$
47	45 46	eqtr3d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1$
48		divgcdnn	$⊢ (A \in ℕ \land B \in ℤ) \to \frac{A}{A \gcd B} \in ℕ$
49	22 29 48	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to \frac{A}{A \gcd B} \in ℕ$
50	49	nnnn0d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to \frac{A}{A \gcd B} \in ℕ_{0}$
51		divgcdnnr	$⊢ (B \in ℕ \land A \in ℤ) \to \frac{B}{A \gcd B} \in ℕ$
52	28 23 51	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to \frac{B}{A \gcd B} \in ℕ$
53	52	nnnn0d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to \frac{B}{A \gcd B} \in ℕ_{0}$
54		nn0rppwr	$⊢ (\frac{A}{A \gcd B} \in ℕ_{0} \land \frac{B}{A \gcd B} \in ℕ_{0} \land N \in ℕ_{0}) \to ((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1 \to {(\frac{A}{A \gcd B})}^{N} \gcd {(\frac{B}{A \gcd B})}^{N} = 1)$
55	50 53 3 54	syl3anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to ((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1 \to {(\frac{A}{A \gcd B})}^{N} \gcd {(\frac{B}{A \gcd B})}^{N} = 1)$
56	47 55	mpd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(\frac{A}{A \gcd B})}^{N} \gcd {(\frac{B}{A \gcd B})}^{N} = 1$
57	34 43 56	3eqtr2d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to \frac{A^{N} \gcd B^{N}}{{(A \gcd B)}^{N}} = 1$
58		gcdnncl	$⊢ (A^{N} \in ℕ \land B^{N} \in ℕ) \to A^{N} \gcd B^{N} \in ℕ$
59	58	nncnd	$⊢ (A^{N} \in ℕ \land B^{N} \in ℕ) \to A^{N} \gcd B^{N} \in ℂ$
60	8 11 59	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to A^{N} \gcd B^{N} \in ℂ$
61	4	nnne0d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} \neq 0$
62		ax-1cn	$⊢ 1 \in ℂ$
63		divmul	$⊢ (A^{N} \gcd B^{N} \in ℂ \land 1 \in ℂ \land ({(A \gcd B)}^{N} \in ℂ \land {(A \gcd B)}^{N} \neq 0)) \to (\frac{A^{N} \gcd B^{N}}{{(A \gcd B)}^{N}} = 1 \leftrightarrow {(A \gcd B)}^{N} \cdot 1 = A^{N} \gcd B^{N})$
64	62 63	mp3an2	$⊢ (A^{N} \gcd B^{N} \in ℂ \land ({(A \gcd B)}^{N} \in ℂ \land {(A \gcd B)}^{N} \neq 0)) \to (\frac{A^{N} \gcd B^{N}}{{(A \gcd B)}^{N}} = 1 \leftrightarrow {(A \gcd B)}^{N} \cdot 1 = A^{N} \gcd B^{N})$
65	60 5 61 64	syl12anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to (\frac{A^{N} \gcd B^{N}}{{(A \gcd B)}^{N}} = 1 \leftrightarrow {(A \gcd B)}^{N} \cdot 1 = A^{N} \gcd B^{N})$
66	57 65	mpbid	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} \cdot 1 = A^{N} \gcd B^{N}$
67	6 66	eqtr3d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$

Metamath Proof Explorer

Theorem expgcd

Proof