Metamath Proof Explorer

Theorem dvdsexp

Description: A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion dvdsexp 
|- ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) || ( A ^ N ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> A e. ZZ )
2 uznn0sub 
 |-  ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )
3 2 3ad2ant3 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( N - M ) e. NN0 )
4 zexpcl 
 |-  ( ( A e. ZZ /\ ( N - M ) e. NN0 ) -> ( A ^ ( N - M ) ) e. ZZ )
5 1 3 4 syl2anc 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( A ^ ( N - M ) ) e. ZZ )
6 zexpcl 
 |-  ( ( A e. ZZ /\ M e. NN0 ) -> ( A ^ M ) e. ZZ )
7 6 3adant3 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) e. ZZ )
8 dvdsmul2 
 |-  ( ( ( A ^ ( N - M ) ) e. ZZ /\ ( A ^ M ) e. ZZ ) -> ( A ^ M ) || ( ( A ^ ( N - M ) ) x. ( A ^ M ) ) )
9 5 7 8 syl2anc 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) || ( ( A ^ ( N - M ) ) x. ( A ^ M ) ) )
10 1 zcnd 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> A e. CC )
11 simp2 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> M e. NN0 )
12 10 11 3 expaddd 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( A ^ ( ( N - M ) + M ) ) = ( ( A ^ ( N - M ) ) x. ( A ^ M ) ) )
13 eluzelcn 
 |-  ( N e. ( ZZ>= ` M ) -> N e. CC )
14 13 3ad2ant3 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> N e. CC )
15 11 nn0cnd 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> M e. CC )
16 14 15 npcand 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( ( N - M ) + M ) = N )
17 16 oveq2d 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( A ^ ( ( N - M ) + M ) ) = ( A ^ N ) )
18 12 17 eqtr3d 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( ( A ^ ( N - M ) ) x. ( A ^ M ) ) = ( A ^ N ) )
19 9 18 breqtrd 
 |-  ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) || ( A ^ N ) )