Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
โข ( ๐ โ โค โ ๐ โ โ ) |
2 |
|
zcn |
โข ( ๐ โ โค โ ๐ โ โ ) |
3 |
|
mulcom |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) |
4 |
1 2 3
|
syl2anr |
โข ( ( ๐ โ โค โง ๐ โ โค ) โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) |
5 |
|
zmulcl |
โข ( ( ๐ โ โค โง ๐ โ โค ) โ ( ๐ ยท ๐ ) โ โค ) |
6 |
|
dvds0lem |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ( ๐ ยท ๐ ) โ โค ) โง ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) โ ๐ โฅ ( ๐ ยท ๐ ) ) |
7 |
6
|
ex |
โข ( ( ๐ โ โค โง ๐ โ โค โง ( ๐ ยท ๐ ) โ โค ) โ ( ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) โ ๐ โฅ ( ๐ ยท ๐ ) ) ) |
8 |
7
|
3com12 |
โข ( ( ๐ โ โค โง ๐ โ โค โง ( ๐ ยท ๐ ) โ โค ) โ ( ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) โ ๐ โฅ ( ๐ ยท ๐ ) ) ) |
9 |
5 8
|
mpd3an3 |
โข ( ( ๐ โ โค โง ๐ โ โค ) โ ( ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) โ ๐ โฅ ( ๐ ยท ๐ ) ) ) |
10 |
4 9
|
mpd |
โข ( ( ๐ โ โค โง ๐ โ โค ) โ ๐ โฅ ( ๐ ยท ๐ ) ) |