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 ) )