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

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 simp1 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> A e. NN )
2 simp3 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> N e. NN )
3 2 nnnn0d 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> N e. NN0 )
4 1 3 nnexpcld 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A ^ N ) e. NN )
5 simp2 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> B e. NN )
6 4 5 2 3jca 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A ^ N ) e. NN /\ B e. NN /\ N e. NN ) )
7 rplpwr 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd B ) = 1 ) )
8 rprpwr 
 |-  ( ( ( A ^ N ) e. NN /\ B e. NN /\ N e. NN ) -> ( ( ( A ^ N ) gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )
9 6 7 8 sylsyld 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )