Metamath Proof Explorer

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 ( 𝐵 ↑ 𝑁 ) ) )