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 
|- ( ( A e. NN /\ B e. NN /\ N e. NN0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )

Proof

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