Metamath Proof Explorer

Theorem rpexp12i

Description: Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014)

Ref Expression
Assertion rpexp12i 
|- ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd ( B ^ N ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 rpexp1i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )
2 1 3adant3r 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )
3 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> B e. ZZ )
4 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> A e. ZZ )
5 simp3l 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> M e. NN0 )
6 zexpcl 
 |-  ( ( A e. ZZ /\ M e. NN0 ) -> ( A ^ M ) e. ZZ )
7 4 5 6 syl2anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( A ^ M ) e. ZZ )
8 simp3r 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> N e. NN0 )
9 rpexp1i 
 |-  ( ( B e. ZZ /\ ( A ^ M ) e. ZZ /\ N e. NN0 ) -> ( ( B gcd ( A ^ M ) ) = 1 -> ( ( B ^ N ) gcd ( A ^ M ) ) = 1 ) )
10 3 7 8 9 syl3anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( B gcd ( A ^ M ) ) = 1 -> ( ( B ^ N ) gcd ( A ^ M ) ) = 1 ) )
11 7 3 gcdcomd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( A ^ M ) gcd B ) = ( B gcd ( A ^ M ) ) )
12 11 eqeq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( ( A ^ M ) gcd B ) = 1 <-> ( B gcd ( A ^ M ) ) = 1 ) )
13 zexpcl 
 |-  ( ( B e. ZZ /\ N e. NN0 ) -> ( B ^ N ) e. ZZ )
14 3 8 13 syl2anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( B ^ N ) e. ZZ )
15 7 14 gcdcomd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( A ^ M ) gcd ( B ^ N ) ) = ( ( B ^ N ) gcd ( A ^ M ) ) )
16 15 eqeq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( ( A ^ M ) gcd ( B ^ N ) ) = 1 <-> ( ( B ^ N ) gcd ( A ^ M ) ) = 1 ) )
17 10 12 16 3imtr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( ( A ^ M ) gcd B ) = 1 -> ( ( A ^ M ) gcd ( B ^ N ) ) = 1 ) )
18 2 17 syld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd ( B ^ N ) ) = 1 ) )