Theorem expgcd

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

	Ref	Expression
Assertion	expgcd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gcdnncl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
3		simp3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
4	2 3	nnexpcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∈ ℕ )
5	4	nncnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∈ ℂ )
6	5	mulridd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) · 1 ) = ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) )
7		nnexpcl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
8	7	3adant2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
9	8	nnzd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
10		nnexpcl	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℕ )
11	10	3adant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℕ )
12	11	nnzd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℤ )
13		simpl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℕ )
14	13	nnzd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℤ )
15		simpr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℕ )
16	15	nnzd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℤ )
17		gcddvds	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
18	14 16 17	syl2anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
19	18	3adant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
20	19	simpld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
21	2	nnzd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
22		simp1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℕ )
23	22	nnzd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
24		dvdsexpim	⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) )
25	21 23 3 24	syl3anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ) )
26	20 25	mpd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) )
27	19	simprd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
28		simp2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ∈ ℕ )
29	28	nnzd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ∈ ℤ )
30		dvdsexpim	⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
31	21 29 3 30	syl3anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
32	27 31	mpd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) )
33		gcddiv	⊢ ( ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℤ ∧ ( 𝐵 ↑ 𝑁 ) ∈ ℤ ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∈ ℕ ) ∧ ( ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∥ ( 𝐴 ↑ 𝑁 ) ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) = ( ( ( 𝐴 ↑ 𝑁 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) gcd ( ( 𝐵 ↑ 𝑁 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) ) )
34	9 12 4 26 32 33	syl32anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) = ( ( ( 𝐴 ↑ 𝑁 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) gcd ( ( 𝐵 ↑ 𝑁 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) ) )
35		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
36	35	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
37	2	nncnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 gcd 𝐵 ) ∈ ℂ )
38	2	nnne0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 gcd 𝐵 ) ≠ 0 )
39	36 37 38 3	expdivd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) )
40		nncn	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
41	40	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
42	41 37 38 3	expdivd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) = ( ( 𝐵 ↑ 𝑁 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) )
43	39 42	oveq12d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) gcd ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) ) = ( ( ( 𝐴 ↑ 𝑁 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) gcd ( ( 𝐵 ↑ 𝑁 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) ) )
44		gcddiv	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ∈ ℕ ) ∧ ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
45	23 29 2 19 44	syl31anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
46	37 38	dividd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = 1 )
47	45 46	eqtr3d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 1 )
48		divgcdnn	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
49	22 29 48	syl2anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
50	49	nnnn0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ0 )
51		divgcdnnr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℤ ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
52	28 23 51	syl2anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
53	52	nnnn0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ0 )
54		nn0rppwr	⊢ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ0 ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 1 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) gcd ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) ) = 1 ) )
55	50 53 3 54	syl3anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 1 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) gcd ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) ) = 1 ) )
56	47 55	mpd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) gcd ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) ) = 1 )
57	34 43 56	3eqtr2d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) = 1 )
58		gcdnncl	⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℕ ∧ ( 𝐵 ↑ 𝑁 ) ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ∈ ℕ )
59	58	nncnd	⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℕ ∧ ( 𝐵 ↑ 𝑁 ) ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ∈ ℂ )
60	8 11 59	syl2anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ∈ ℂ )
61	4	nnne0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ≠ 0 )
62		ax-1cn	⊢ 1 ∈ ℂ
63		divmul	⊢ ( ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∈ ℂ ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ≠ 0 ) ) → ( ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) = 1 ↔ ( ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) · 1 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
64	62 63	mp3an2	⊢ ( ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ∈ ℂ ∧ ( ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ∈ ℂ ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ≠ 0 ) ) → ( ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) = 1 ↔ ( ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) · 1 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
65	60 5 61 64	syl12anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) ) = 1 ↔ ( ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) · 1 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
66	57 65	mpbid	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) · 1 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
67	6 66	eqtr3d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )