Metamath Proof Explorer

Theorem dvdsexpim

Description: If two numbers are divisible, so are their nonnegative exponents. Similar to dvdssqim for nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023)

Ref Expression
Assertion dvdsexpim 
|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( A || B -> ( A ^ N ) || ( B ^ N ) ) )

Proof

Step Hyp Ref Expression
1 divides 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> E. k e. ZZ ( k x. A ) = B ) )
2 1 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( A || B <-> E. k e. ZZ ( k x. A ) = B ) )
3 zexpcl 
 |-  ( ( k e. ZZ /\ N e. NN0 ) -> ( k ^ N ) e. ZZ )
4 3 ancoms 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( k ^ N ) e. ZZ )
5 4 adantll 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> ( k ^ N ) e. ZZ )
6 zexpcl 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A ^ N ) e. ZZ )
7 6 adantr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> ( A ^ N ) e. ZZ )
8 dvdsmul2 
 |-  ( ( ( k ^ N ) e. ZZ /\ ( A ^ N ) e. ZZ ) -> ( A ^ N ) || ( ( k ^ N ) x. ( A ^ N ) ) )
9 5 7 8 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> ( A ^ N ) || ( ( k ^ N ) x. ( A ^ N ) ) )
10 zcn 
 |-  ( k e. ZZ -> k e. CC )
11 10 adantl 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> k e. CC )
12 zcn 
 |-  ( A e. ZZ -> A e. CC )
13 12 ad2antrr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> A e. CC )
14 simplr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> N e. NN0 )
15 11 13 14 mulexpd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> ( ( k x. A ) ^ N ) = ( ( k ^ N ) x. ( A ^ N ) ) )
16 9 15 breqtrrd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> ( A ^ N ) || ( ( k x. A ) ^ N ) )
17 oveq1 
 |-  ( ( k x. A ) = B -> ( ( k x. A ) ^ N ) = ( B ^ N ) )
18 17 breq2d 
 |-  ( ( k x. A ) = B -> ( ( A ^ N ) || ( ( k x. A ) ^ N ) <-> ( A ^ N ) || ( B ^ N ) ) )
19 16 18 syl5ibcom 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ k e. ZZ ) -> ( ( k x. A ) = B -> ( A ^ N ) || ( B ^ N ) ) )
20 19 rexlimdva 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( E. k e. ZZ ( k x. A ) = B -> ( A ^ N ) || ( B ^ N ) ) )
21 20 3adant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( E. k e. ZZ ( k x. A ) = B -> ( A ^ N ) || ( B ^ N ) ) )
22 2 21 sylbid 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( A || B -> ( A ^ N ) || ( B ^ N ) ) )