This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 gcdabs 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( abs ` A ) gcd ( abs ` B ) ) = ( A gcd B ) )
2 1 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( abs ` A ) gcd ( abs ` B ) ) = ( A gcd B ) )
3 2 eqcomd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( A gcd B ) = ( ( abs ` A ) gcd ( abs ` B ) ) )
4 3 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( A gcd B ) ^ N ) = ( ( ( abs ` A ) gcd ( abs ` B ) ) ^ N ) )
5 nn0abscl 
 |-  ( A e. ZZ -> ( abs ` A ) e. NN0 )
6 nn0abscl 
 |-  ( B e. ZZ -> ( abs ` B ) e. NN0 )
7 id 
 |-  ( N e. NN0 -> N e. NN0 )
8 nn0expgcd 
 |-  ( ( ( abs ` A ) e. NN0 /\ ( abs ` B ) e. NN0 /\ N e. NN0 ) -> ( ( ( abs ` A ) gcd ( abs ` B ) ) ^ N ) = ( ( ( abs ` A ) ^ N ) gcd ( ( abs ` B ) ^ N ) ) )
9 5 6 7 8 syl3an 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( ( abs ` A ) gcd ( abs ` B ) ) ^ N ) = ( ( ( abs ` A ) ^ N ) gcd ( ( abs ` B ) ^ N ) ) )
10 zcn 
 |-  ( A e. ZZ -> A e. CC )
11 10 3ad2ant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> A e. CC )
12 simp3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> N e. NN0 )
13 11 12 absexpd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )
14 13 eqcomd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( abs ` A ) ^ N ) = ( abs ` ( A ^ N ) ) )
15 zcn 
 |-  ( B e. ZZ -> B e. CC )
16 15 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> B e. CC )
17 16 12 absexpd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( abs ` ( B ^ N ) ) = ( ( abs ` B ) ^ N ) )
18 17 eqcomd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( abs ` B ) ^ N ) = ( abs ` ( B ^ N ) ) )
19 14 18 oveq12d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( ( abs ` A ) ^ N ) gcd ( ( abs ` B ) ^ N ) ) = ( ( abs ` ( A ^ N ) ) gcd ( abs ` ( B ^ N ) ) ) )
20 zexpcl 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A ^ N ) e. ZZ )
21 20 3adant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( A ^ N ) e. ZZ )
22 zexpcl 
 |-  ( ( B e. ZZ /\ N e. NN0 ) -> ( B ^ N ) e. ZZ )
23 22 3adant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( B ^ N ) e. ZZ )
24 gcdabs 
 |-  ( ( ( A ^ N ) e. ZZ /\ ( B ^ N ) e. ZZ ) -> ( ( abs ` ( A ^ N ) ) gcd ( abs ` ( B ^ N ) ) ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
25 21 23 24 syl2anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( abs ` ( A ^ N ) ) gcd ( abs ` ( B ^ N ) ) ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
26 19 25 eqtrd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( ( abs ` A ) ^ N ) gcd ( ( abs ` B ) ^ N ) ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
27 4 9 26 3eqtrd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )