Step |
Hyp |
Ref |
Expression |
1 |
|
divides |
โข ( ( ๐ โ โค โง ๐พ โ โค ) โ ( ๐ โฅ ๐พ โ โ ๐ฅ โ โค ( ๐ฅ ยท ๐ ) = ๐พ ) ) |
2 |
1
|
3adant1 |
โข ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โ ( ๐ โฅ ๐พ โ โ ๐ฅ โ โค ( ๐ฅ ยท ๐ ) = ๐พ ) ) |
3 |
2
|
adantr |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ๐ gcd ๐ ) = 1 ) โ ( ๐ โฅ ๐พ โ โ ๐ฅ โ โค ( ๐ฅ ยท ๐ ) = ๐พ ) ) |
4 |
|
simprr |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ๐ฅ โ โค ) |
5 |
|
simpl2 |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ๐ โ โค ) |
6 |
|
zcn |
โข ( ๐ฅ โ โค โ ๐ฅ โ โ ) |
7 |
|
zcn |
โข ( ๐ โ โค โ ๐ โ โ ) |
8 |
|
mulcom |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ ( ๐ฅ ยท ๐ ) = ( ๐ ยท ๐ฅ ) ) |
9 |
6 7 8
|
syl2an |
โข ( ( ๐ฅ โ โค โง ๐ โ โค ) โ ( ๐ฅ ยท ๐ ) = ( ๐ ยท ๐ฅ ) ) |
10 |
4 5 9
|
syl2anc |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ๐ฅ ยท ๐ ) = ( ๐ ยท ๐ฅ ) ) |
11 |
10
|
breq2d |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ๐ โฅ ( ๐ฅ ยท ๐ ) โ ๐ โฅ ( ๐ ยท ๐ฅ ) ) ) |
12 |
|
simprl |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ๐ gcd ๐ ) = 1 ) |
13 |
|
simpl1 |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ๐ โ โค ) |
14 |
|
coprmdvds |
โข ( ( ๐ โ โค โง ๐ โ โค โง ๐ฅ โ โค ) โ ( ( ๐ โฅ ( ๐ ยท ๐ฅ ) โง ( ๐ gcd ๐ ) = 1 ) โ ๐ โฅ ๐ฅ ) ) |
15 |
13 5 4 14
|
syl3anc |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ( ๐ โฅ ( ๐ ยท ๐ฅ ) โง ( ๐ gcd ๐ ) = 1 ) โ ๐ โฅ ๐ฅ ) ) |
16 |
12 15
|
mpan2d |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ๐ โฅ ( ๐ ยท ๐ฅ ) โ ๐ โฅ ๐ฅ ) ) |
17 |
11 16
|
sylbid |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ๐ โฅ ( ๐ฅ ยท ๐ ) โ ๐ โฅ ๐ฅ ) ) |
18 |
|
dvdsmulc |
โข ( ( ๐ โ โค โง ๐ฅ โ โค โง ๐ โ โค ) โ ( ๐ โฅ ๐ฅ โ ( ๐ ยท ๐ ) โฅ ( ๐ฅ ยท ๐ ) ) ) |
19 |
13 4 5 18
|
syl3anc |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ๐ โฅ ๐ฅ โ ( ๐ ยท ๐ ) โฅ ( ๐ฅ ยท ๐ ) ) ) |
20 |
17 19
|
syld |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ๐ โฅ ( ๐ฅ ยท ๐ ) โ ( ๐ ยท ๐ ) โฅ ( ๐ฅ ยท ๐ ) ) ) |
21 |
|
breq2 |
โข ( ( ๐ฅ ยท ๐ ) = ๐พ โ ( ๐ โฅ ( ๐ฅ ยท ๐ ) โ ๐ โฅ ๐พ ) ) |
22 |
|
breq2 |
โข ( ( ๐ฅ ยท ๐ ) = ๐พ โ ( ( ๐ ยท ๐ ) โฅ ( ๐ฅ ยท ๐ ) โ ( ๐ ยท ๐ ) โฅ ๐พ ) ) |
23 |
21 22
|
imbi12d |
โข ( ( ๐ฅ ยท ๐ ) = ๐พ โ ( ( ๐ โฅ ( ๐ฅ ยท ๐ ) โ ( ๐ ยท ๐ ) โฅ ( ๐ฅ ยท ๐ ) ) โ ( ๐ โฅ ๐พ โ ( ๐ ยท ๐ ) โฅ ๐พ ) ) ) |
24 |
20 23
|
syl5ibcom |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ( ๐ gcd ๐ ) = 1 โง ๐ฅ โ โค ) ) โ ( ( ๐ฅ ยท ๐ ) = ๐พ โ ( ๐ โฅ ๐พ โ ( ๐ ยท ๐ ) โฅ ๐พ ) ) ) |
25 |
24
|
anassrs |
โข ( ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ๐ gcd ๐ ) = 1 ) โง ๐ฅ โ โค ) โ ( ( ๐ฅ ยท ๐ ) = ๐พ โ ( ๐ โฅ ๐พ โ ( ๐ ยท ๐ ) โฅ ๐พ ) ) ) |
26 |
25
|
rexlimdva |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ๐ gcd ๐ ) = 1 ) โ ( โ ๐ฅ โ โค ( ๐ฅ ยท ๐ ) = ๐พ โ ( ๐ โฅ ๐พ โ ( ๐ ยท ๐ ) โฅ ๐พ ) ) ) |
27 |
3 26
|
sylbid |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ๐ gcd ๐ ) = 1 ) โ ( ๐ โฅ ๐พ โ ( ๐ โฅ ๐พ โ ( ๐ ยท ๐ ) โฅ ๐พ ) ) ) |
28 |
27
|
impcomd |
โข ( ( ( ๐ โ โค โง ๐ โ โค โง ๐พ โ โค ) โง ( ๐ gcd ๐ ) = 1 ) โ ( ( ๐ โฅ ๐พ โง ๐ โฅ ๐พ ) โ ( ๐ ยท ๐ ) โฅ ๐พ ) ) |