# Metamath Proof Explorer

## Theorem rplpwr

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

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

### Proof

Step Hyp Ref Expression
1 oveq2
` |-  ( k = 1 -> ( A ^ k ) = ( A ^ 1 ) )`
2 1 oveq1d
` |-  ( k = 1 -> ( ( A ^ k ) gcd B ) = ( ( A ^ 1 ) gcd B ) )`
3 2 eqeq1d
` |-  ( k = 1 -> ( ( ( A ^ k ) gcd B ) = 1 <-> ( ( A ^ 1 ) gcd B ) = 1 ) )`
4 3 imbi2d
` |-  ( k = 1 -> ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ k ) gcd B ) = 1 ) <-> ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ 1 ) gcd B ) = 1 ) ) )`
5 oveq2
` |-  ( k = n -> ( A ^ k ) = ( A ^ n ) )`
6 5 oveq1d
` |-  ( k = n -> ( ( A ^ k ) gcd B ) = ( ( A ^ n ) gcd B ) )`
7 6 eqeq1d
` |-  ( k = n -> ( ( ( A ^ k ) gcd B ) = 1 <-> ( ( A ^ n ) gcd B ) = 1 ) )`
8 7 imbi2d
` |-  ( k = n -> ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ k ) gcd B ) = 1 ) <-> ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ n ) gcd B ) = 1 ) ) )`
9 oveq2
` |-  ( k = ( n + 1 ) -> ( A ^ k ) = ( A ^ ( n + 1 ) ) )`
10 9 oveq1d
` |-  ( k = ( n + 1 ) -> ( ( A ^ k ) gcd B ) = ( ( A ^ ( n + 1 ) ) gcd B ) )`
11 10 eqeq1d
` |-  ( k = ( n + 1 ) -> ( ( ( A ^ k ) gcd B ) = 1 <-> ( ( A ^ ( n + 1 ) ) gcd B ) = 1 ) )`
12 11 imbi2d
` |-  ( k = ( n + 1 ) -> ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ k ) gcd B ) = 1 ) <-> ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ ( n + 1 ) ) gcd B ) = 1 ) ) )`
13 oveq2
` |-  ( k = N -> ( A ^ k ) = ( A ^ N ) )`
14 13 oveq1d
` |-  ( k = N -> ( ( A ^ k ) gcd B ) = ( ( A ^ N ) gcd B ) )`
15 14 eqeq1d
` |-  ( k = N -> ( ( ( A ^ k ) gcd B ) = 1 <-> ( ( A ^ N ) gcd B ) = 1 ) )`
16 15 imbi2d
` |-  ( k = N -> ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ k ) gcd B ) = 1 ) <-> ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ N ) gcd B ) = 1 ) ) )`
17 nncn
` |-  ( A e. NN -> A e. CC )`
18 17 exp1d
` |-  ( A e. NN -> ( A ^ 1 ) = A )`
19 18 oveq1d
` |-  ( A e. NN -> ( ( A ^ 1 ) gcd B ) = ( A gcd B ) )`
` |-  ( ( A e. NN /\ B e. NN ) -> ( ( A ^ 1 ) gcd B ) = ( A gcd B ) )`
21 20 eqeq1d
` |-  ( ( A e. NN /\ B e. NN ) -> ( ( ( A ^ 1 ) gcd B ) = 1 <-> ( A gcd B ) = 1 ) )`
22 21 biimpar
` |-  ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ 1 ) gcd B ) = 1 )`
23 df-3an
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) <-> ( ( A e. NN /\ B e. NN ) /\ n e. NN ) )`
24 simpl1
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> A e. NN )`
25 24 nncnd
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> A e. CC )`
26 simpl3
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> n e. NN )`
27 26 nnnn0d
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> n e. NN0 )`
28 25 27 expp1d
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ ( n + 1 ) ) = ( ( A ^ n ) x. A ) )`
29 simp1
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> A e. NN )`
30 nnnn0
` |-  ( n e. NN -> n e. NN0 )`
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> n e. NN0 )`
32 29 31 nnexpcld
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( A ^ n ) e. NN )`
33 32 nnzd
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( A ^ n ) e. ZZ )`
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ n ) e. ZZ )`
35 34 zcnd
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ n ) e. CC )`
36 35 25 mulcomd
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ n ) x. A ) = ( A x. ( A ^ n ) ) )`
37 28 36 eqtrd
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ ( n + 1 ) ) = ( A x. ( A ^ n ) ) )`
38 37 oveq2d
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( B gcd ( A ^ ( n + 1 ) ) ) = ( B gcd ( A x. ( A ^ n ) ) ) )`
39 simpl2
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> B e. NN )`
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ n ) e. NN )`
41 nnz
` |-  ( A e. NN -> A e. ZZ )`
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> A e. ZZ )`
43 nnz
` |-  ( B e. NN -> B e. ZZ )`
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> B e. ZZ )`
45 gcdcom
` |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )`
46 42 44 45 syl2anc
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( A gcd B ) = ( B gcd A ) )`
47 46 eqeq1d
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( ( A gcd B ) = 1 <-> ( B gcd A ) = 1 ) )`
48 47 biimpa
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( B gcd A ) = 1 )`
49 rpmulgcd
` |-  ( ( ( B e. NN /\ A e. NN /\ ( A ^ n ) e. NN ) /\ ( B gcd A ) = 1 ) -> ( B gcd ( A x. ( A ^ n ) ) ) = ( B gcd ( A ^ n ) ) )`
50 39 24 40 48 49 syl31anc
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( B gcd ( A x. ( A ^ n ) ) ) = ( B gcd ( A ^ n ) ) )`
51 38 50 eqtrd
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( B gcd ( A ^ ( n + 1 ) ) ) = ( B gcd ( A ^ n ) ) )`
52 peano2nn
` |-  ( n e. NN -> ( n + 1 ) e. NN )`
` |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( n + 1 ) e. NN )`
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( n + 1 ) e. NN )`
55 54 nnnn0d
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( n + 1 ) e. NN0 )`
56 24 55 nnexpcld
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ ( n + 1 ) ) e. NN )`
57 56 nnzd
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ ( n + 1 ) ) e. ZZ )`
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> B e. ZZ )`
59 gcdcom
` |-  ( ( ( A ^ ( n + 1 ) ) e. ZZ /\ B e. ZZ ) -> ( ( A ^ ( n + 1 ) ) gcd B ) = ( B gcd ( A ^ ( n + 1 ) ) ) )`
60 57 58 59 syl2anc
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ ( n + 1 ) ) gcd B ) = ( B gcd ( A ^ ( n + 1 ) ) ) )`
61 gcdcom
` |-  ( ( ( A ^ n ) e. ZZ /\ B e. ZZ ) -> ( ( A ^ n ) gcd B ) = ( B gcd ( A ^ n ) ) )`
62 34 58 61 syl2anc
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ n ) gcd B ) = ( B gcd ( A ^ n ) ) )`
63 51 60 62 3eqtr4d
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ ( n + 1 ) ) gcd B ) = ( ( A ^ n ) gcd B ) )`
64 63 eqeq1d
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( ( A ^ ( n + 1 ) ) gcd B ) = 1 <-> ( ( A ^ n ) gcd B ) = 1 ) )`
65 64 biimprd
` |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( ( A ^ n ) gcd B ) = 1 -> ( ( A ^ ( n + 1 ) ) gcd B ) = 1 ) )`
66 23 65 sylanbr
` |-  ( ( ( ( A e. NN /\ B e. NN ) /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( ( A ^ n ) gcd B ) = 1 -> ( ( A ^ ( n + 1 ) ) gcd B ) = 1 ) )`
67 66 an32s
` |-  ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) /\ n e. NN ) -> ( ( ( A ^ n ) gcd B ) = 1 -> ( ( A ^ ( n + 1 ) ) gcd B ) = 1 ) )`
68 67 expcom
` |-  ( n e. NN -> ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( ( A ^ n ) gcd B ) = 1 -> ( ( A ^ ( n + 1 ) ) gcd B ) = 1 ) ) )`
69 68 a2d
` |-  ( n e. NN -> ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ n ) gcd B ) = 1 ) -> ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ ( n + 1 ) ) gcd B ) = 1 ) ) )`
70 4 8 12 16 22 69 nnind
` |-  ( N e. NN -> ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ N ) gcd B ) = 1 ) )`
71 70 expd
` |-  ( N e. NN -> ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd B ) = 1 ) ) )`
72 71 com12
` |-  ( ( A e. NN /\ B e. NN ) -> ( N e. NN -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd B ) = 1 ) ) )`
73 72 3impia
` |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd B ) = 1 ) )`