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 ) )
20 19 adantr
 |-  ( ( 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 )
31 30 3ad2ant3
 |-  ( ( 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 )
34 33 adantr
 |-  ( ( ( 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 )
40 32 adantr
 |-  ( ( ( 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 )
42 41 3ad2ant1
 |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> A e. ZZ )
43 nnz
 |-  ( B e. NN -> B e. ZZ )
44 43 3ad2ant2
 |-  ( ( 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 )
53 52 3ad2ant3
 |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( n + 1 ) e. NN )
54 53 adantr
 |-  ( ( ( 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 )
58 44 adantr
 |-  ( ( ( 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 ) )