Metamath Proof Explorer

Theorem rpexp1i

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

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

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
2 rpexp 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> ( ( ( A ^ M ) gcd B ) = 1 <-> ( A gcd B ) = 1 ) )
3 2 biimprd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )
4 3 3expa 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )
5 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> M = 0 )
6 5 oveq2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> ( A ^ M ) = ( A ^ 0 ) )
7 zcn 
 |-  ( A e. ZZ -> A e. CC )
8 7 ad2antrr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> A e. CC )
9 8 exp0d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> ( A ^ 0 ) = 1 )
10 6 9 eqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> ( A ^ M ) = 1 )
11 10 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> ( ( A ^ M ) gcd B ) = ( 1 gcd B ) )
12 1gcd 
 |-  ( B e. ZZ -> ( 1 gcd B ) = 1 )
13 12 ad2antlr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> ( 1 gcd B ) = 1 )
14 11 13 eqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> ( ( A ^ M ) gcd B ) = 1 )
15 14 a1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M = 0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )
16 4 15 jaodan 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( M e. NN \/ M = 0 ) ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )
17 1 16 sylan2b 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ M e. NN0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )
18 17 3impa 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )