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 42 44 gcdcomd 
 |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( A gcd B ) = ( B gcd A ) )
46 45 eqeq1d 
 |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( ( A gcd B ) = 1 <-> ( B gcd A ) = 1 ) )
47 46 biimpa 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( B gcd A ) = 1 )
48 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 ) ) )
49 39 24 40 47 48 syl31anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( B gcd ( A x. ( A ^ n ) ) ) = ( B gcd ( A ^ n ) ) )
50 38 49 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( B gcd ( A ^ ( n + 1 ) ) ) = ( B gcd ( A ^ n ) ) )
51 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
52 51 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ n e. NN ) -> ( n + 1 ) e. NN )
53 52 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( n + 1 ) e. NN )
54 53 nnnn0d 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( n + 1 ) e. NN0 )
55 24 54 nnexpcld 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ ( n + 1 ) ) e. NN )
56 55 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( A ^ ( n + 1 ) ) e. ZZ )
57 44 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> B e. ZZ )
58 56 57 gcdcomd 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ ( n + 1 ) ) gcd B ) = ( B gcd ( A ^ ( n + 1 ) ) ) )
59 34 57 gcdcomd 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ n ) gcd B ) = ( B gcd ( A ^ n ) ) )
60 50 58 59 3eqtr4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ n e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ ( n + 1 ) ) gcd B ) = ( ( A ^ n ) gcd B ) )
61 60 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 ) )
62 61 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 ) )
63 23 62 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 ) )
64 63 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 ) )
65 64 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 ) ) )
66 65 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 ) ) )
67 4 8 12 16 22 66 nnind 
 |-  ( N e. NN -> ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( ( A ^ N ) gcd B ) = 1 ) )
68 67 expd 
 |-  ( N e. NN -> ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd B ) = 1 ) ) )
69 68 com12 
 |-  ( ( A e. NN /\ B e. NN ) -> ( N e. NN -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd B ) = 1 ) ) )
70 69 3impia 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd B ) = 1 ) )