Metamath Proof Explorer


Theorem rppwr

Description: If A and B are relatively prime, then so are A ^ N and B ^ N . (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 simpl1
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> A e. NN )
2 simpl2
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> B e. NN )
3 simpl3
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> N e. NN )
4 3 nnnn0d
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> N e. NN0 )
5 2 4 nnexpcld
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( B ^ N ) e. NN )
6 1 5 3 3jca
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( A e. NN /\ ( B ^ N ) e. NN /\ N e. NN ) )
7 1 nnzd
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> A e. ZZ )
8 5 nnzd
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( B ^ N ) e. ZZ )
9 gcdcom
 |-  ( ( A e. ZZ /\ ( B ^ N ) e. ZZ ) -> ( A gcd ( B ^ N ) ) = ( ( B ^ N ) gcd A ) )
10 7 8 9 syl2anc
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( A gcd ( B ^ N ) ) = ( ( B ^ N ) gcd A ) )
11 2 1 3 3jca
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( B e. NN /\ A e. NN /\ N e. NN ) )
12 nnz
 |-  ( A e. NN -> A e. ZZ )
13 12 3ad2ant1
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> A e. ZZ )
14 nnz
 |-  ( B e. NN -> B e. ZZ )
15 14 3ad2ant2
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> B e. ZZ )
16 gcdcom
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
17 13 15 16 syl2anc
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A gcd B ) = ( B gcd A ) )
18 17 eqeq1d
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 <-> ( B gcd A ) = 1 ) )
19 18 biimpa
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( B gcd A ) = 1 )
20 rplpwr
 |-  ( ( B e. NN /\ A e. NN /\ N e. NN ) -> ( ( B gcd A ) = 1 -> ( ( B ^ N ) gcd A ) = 1 ) )
21 11 19 20 sylc
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( B ^ N ) gcd A ) = 1 )
22 10 21 eqtrd
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( A gcd ( B ^ N ) ) = 1 )
23 rplpwr
 |-  ( ( A e. NN /\ ( B ^ N ) e. NN /\ N e. NN ) -> ( ( A gcd ( B ^ N ) ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )
24 6 22 23 sylc
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 )
25 24 ex
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )