Step |
Hyp |
Ref |
Expression |
1 |
|
coprm |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ( ยฌ ๐ โฅ ๐ โ ( ๐ gcd ๐ ) = 1 ) ) |
2 |
1
|
3adant3 |
โข ( ( ๐ โ โ โง ๐ โ โค โง ๐ โ โค ) โ ( ยฌ ๐ โฅ ๐ โ ( ๐ gcd ๐ ) = 1 ) ) |
3 |
2
|
anbi2d |
โข ( ( ๐ โ โ โง ๐ โ โค โง ๐ โ โค ) โ ( ( ๐ โฅ ( ๐ ยท ๐ ) โง ยฌ ๐ โฅ ๐ ) โ ( ๐ โฅ ( ๐ ยท ๐ ) โง ( ๐ gcd ๐ ) = 1 ) ) ) |
4 |
|
prmz |
โข ( ๐ โ โ โ ๐ โ โค ) |
5 |
|
coprmdvds |
โข ( ( ๐ โ โค โง ๐ โ โค โง ๐ โ โค ) โ ( ( ๐ โฅ ( ๐ ยท ๐ ) โง ( ๐ gcd ๐ ) = 1 ) โ ๐ โฅ ๐ ) ) |
6 |
4 5
|
syl3an1 |
โข ( ( ๐ โ โ โง ๐ โ โค โง ๐ โ โค ) โ ( ( ๐ โฅ ( ๐ ยท ๐ ) โง ( ๐ gcd ๐ ) = 1 ) โ ๐ โฅ ๐ ) ) |
7 |
3 6
|
sylbid |
โข ( ( ๐ โ โ โง ๐ โ โค โง ๐ โ โค ) โ ( ( ๐ โฅ ( ๐ ยท ๐ ) โง ยฌ ๐ โฅ ๐ ) โ ๐ โฅ ๐ ) ) |
8 |
7
|
expd |
โข ( ( ๐ โ โ โง ๐ โ โค โง ๐ โ โค ) โ ( ๐ โฅ ( ๐ ยท ๐ ) โ ( ยฌ ๐ โฅ ๐ โ ๐ โฅ ๐ ) ) ) |
9 |
|
df-or |
โข ( ( ๐ โฅ ๐ โจ ๐ โฅ ๐ ) โ ( ยฌ ๐ โฅ ๐ โ ๐ โฅ ๐ ) ) |
10 |
8 9
|
imbitrrdi |
โข ( ( ๐ โ โ โง ๐ โ โค โง ๐ โ โค ) โ ( ๐ โฅ ( ๐ ยท ๐ ) โ ( ๐ โฅ ๐ โจ ๐ โฅ ๐ ) ) ) |
11 |
|
ordvdsmul |
โข ( ( ๐ โ โค โง ๐ โ โค โง ๐ โ โค ) โ ( ( ๐ โฅ ๐ โจ ๐ โฅ ๐ ) โ ๐ โฅ ( ๐ ยท ๐ ) ) ) |
12 |
4 11
|
syl3an1 |
โข ( ( ๐ โ โ โง ๐ โ โค โง ๐ โ โค ) โ ( ( ๐ โฅ ๐ โจ ๐ โฅ ๐ ) โ ๐ โฅ ( ๐ ยท ๐ ) ) ) |
13 |
10 12
|
impbid |
โข ( ( ๐ โ โ โง ๐ โ โค โง ๐ โ โค ) โ ( ๐ โฅ ( ๐ ยท ๐ ) โ ( ๐ โฅ ๐ โจ ๐ โฅ ๐ ) ) ) |