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 ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ๐ด โ†‘ ๐‘€ ) โˆฅ ( ๐ด โ†‘ ๐‘ ) )

Proof

Step Hyp Ref Expression
1 simp1 โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ๐ด โˆˆ โ„ค )
2 uznn0sub โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) โ†’ ( ๐‘ โˆ’ ๐‘€ ) โˆˆ โ„•0 )
3 2 3ad2ant3 โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ๐‘ โˆ’ ๐‘€ ) โˆˆ โ„•0 )
4 zexpcl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ( ๐‘ โˆ’ ๐‘€ ) โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ( ๐‘ โˆ’ ๐‘€ ) ) โˆˆ โ„ค )
5 1 3 4 syl2anc โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ๐ด โ†‘ ( ๐‘ โˆ’ ๐‘€ ) ) โˆˆ โ„ค )
6 zexpcl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ๐‘€ ) โˆˆ โ„ค )
7 6 3adant3 โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ๐ด โ†‘ ๐‘€ ) โˆˆ โ„ค )
8 dvdsmul2 โŠข ( ( ( ๐ด โ†‘ ( ๐‘ โˆ’ ๐‘€ ) ) โˆˆ โ„ค โˆง ( ๐ด โ†‘ ๐‘€ ) โˆˆ โ„ค ) โ†’ ( ๐ด โ†‘ ๐‘€ ) โˆฅ ( ( ๐ด โ†‘ ( ๐‘ โˆ’ ๐‘€ ) ) ยท ( ๐ด โ†‘ ๐‘€ ) ) )
9 5 7 8 syl2anc โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ๐ด โ†‘ ๐‘€ ) โˆฅ ( ( ๐ด โ†‘ ( ๐‘ โˆ’ ๐‘€ ) ) ยท ( ๐ด โ†‘ ๐‘€ ) ) )
10 1 zcnd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ๐ด โˆˆ โ„‚ )
11 simp2 โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ๐‘€ โˆˆ โ„•0 )
12 10 11 3 expaddd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ๐ด โ†‘ ( ( ๐‘ โˆ’ ๐‘€ ) + ๐‘€ ) ) = ( ( ๐ด โ†‘ ( ๐‘ โˆ’ ๐‘€ ) ) ยท ( ๐ด โ†‘ ๐‘€ ) ) )
13 eluzelcn โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) โ†’ ๐‘ โˆˆ โ„‚ )
14 13 3ad2ant3 โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ๐‘ โˆˆ โ„‚ )
15 11 nn0cnd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ๐‘€ โˆˆ โ„‚ )
16 14 15 npcand โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ( ๐‘ โˆ’ ๐‘€ ) + ๐‘€ ) = ๐‘ )
17 16 oveq2d โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ๐ด โ†‘ ( ( ๐‘ โˆ’ ๐‘€ ) + ๐‘€ ) ) = ( ๐ด โ†‘ ๐‘ ) )
18 12 17 eqtr3d โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ( ๐ด โ†‘ ( ๐‘ โˆ’ ๐‘€ ) ) ยท ( ๐ด โ†‘ ๐‘€ ) ) = ( ๐ด โ†‘ ๐‘ ) )
19 9 18 breqtrd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ( ๐ด โ†‘ ๐‘€ ) โˆฅ ( ๐ด โ†‘ ๐‘ ) )