Metamath Proof Explorer

Theorem rprpwr

Description: If A and B are relatively prime, then so are A and B ^ N . Originally a subproof of rppwr . (Contributed by SN, 21-Aug-2024)

Ref Expression
Assertion rprpwr 
|- ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( A gcd ( B ^ N ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 rplpwr 
 |-  ( ( B e. NN /\ A e. NN /\ N e. NN ) -> ( ( B gcd A ) = 1 -> ( ( B ^ N ) gcd A ) = 1 ) )
2 1 3com12 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( B gcd A ) = 1 -> ( ( B ^ N ) gcd A ) = 1 ) )
3 nnz 
 |-  ( A e. NN -> A e. ZZ )
4 nnz 
 |-  ( B e. NN -> B e. ZZ )
5 gcdcom 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
6 3 4 5 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) = ( B gcd A ) )
7 6 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A gcd B ) = ( B gcd A ) )
8 7 eqeq1d 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 <-> ( B gcd A ) = 1 ) )
9 simp1 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> A e. NN )
10 9 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> A e. ZZ )
11 simp2 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> B e. NN )
12 simp3 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> N e. NN )
13 12 nnnn0d 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> N e. NN0 )
14 11 13 nnexpcld 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( B ^ N ) e. NN )
15 14 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( B ^ N ) e. ZZ )
16 10 15 gcdcomd 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A gcd ( B ^ N ) ) = ( ( B ^ N ) gcd A ) )
17 16 eqeq1d 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd ( B ^ N ) ) = 1 <-> ( ( B ^ N ) gcd A ) = 1 ) )
18 2 8 17 3imtr4d 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( A gcd ( B ^ N ) ) = 1 ) )