Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
โข ( ( ๐ โ โ โง ( ๐ถ gcd ๐ ) = 1 ) โ ๐ โ โ ) |
2 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
3 |
2
|
div1d |
โข ( ๐ โ โ โ ( ๐ / 1 ) = ๐ ) |
4 |
|
oveq2 |
โข ( ( ๐ถ gcd ๐ ) = 1 โ ( ๐ / ( ๐ถ gcd ๐ ) ) = ( ๐ / 1 ) ) |
5 |
4
|
eqcomd |
โข ( ( ๐ถ gcd ๐ ) = 1 โ ( ๐ / 1 ) = ( ๐ / ( ๐ถ gcd ๐ ) ) ) |
6 |
3 5
|
sylan9req |
โข ( ( ๐ โ โ โง ( ๐ถ gcd ๐ ) = 1 ) โ ๐ = ( ๐ / ( ๐ถ gcd ๐ ) ) ) |
7 |
1 6
|
jca |
โข ( ( ๐ โ โ โง ( ๐ถ gcd ๐ ) = 1 ) โ ( ๐ โ โ โง ๐ = ( ๐ / ( ๐ถ gcd ๐ ) ) ) ) |
8 |
|
cncongr |
โข ( ( ( ๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค ) โง ( ๐ โ โ โง ๐ = ( ๐ / ( ๐ถ gcd ๐ ) ) ) ) โ ( ( ( ๐ด ยท ๐ถ ) mod ๐ ) = ( ( ๐ต ยท ๐ถ ) mod ๐ ) โ ( ๐ด mod ๐ ) = ( ๐ต mod ๐ ) ) ) |
9 |
7 8
|
sylan2 |
โข ( ( ( ๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค ) โง ( ๐ โ โ โง ( ๐ถ gcd ๐ ) = 1 ) ) โ ( ( ( ๐ด ยท ๐ถ ) mod ๐ ) = ( ( ๐ต ยท ๐ถ ) mod ๐ ) โ ( ๐ด mod ๐ ) = ( ๐ต mod ๐ ) ) ) |