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 B N A gcd B = 1 A gcd B N = 1

Proof

Step Hyp Ref Expression
1 rplpwr B A N B gcd A = 1 B N gcd A = 1
2 1 3com12 A B N B gcd A = 1 B N gcd A = 1
3 nnz A A
4 nnz B B
5 gcdcom A B A gcd B = B gcd A
6 3 4 5 syl2an A B A gcd B = B gcd A
7 6 3adant3 A B N A gcd B = B gcd A
8 7 eqeq1d A B N A gcd B = 1 B gcd A = 1
9 simp1 A B N A
10 9 nnzd A B N A
11 simp2 A B N B
12 simp3 A B N N
13 12 nnnn0d A B N N 0
14 11 13 nnexpcld A B N B N
15 14 nnzd A B N B N
16 10 15 gcdcomd A B N A gcd B N = B N gcd A
17 16 eqeq1d A B N A gcd B N = 1 B N gcd A = 1
18 2 8 17 3imtr4d A B N A gcd B = 1 A gcd B N = 1