Step |
Hyp |
Ref |
Expression |
1 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
2 |
1
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ๐ โ โ ) |
3 |
|
zcn |
โข ( ๐ โ โค โ ๐ โ โ ) |
4 |
3
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ๐ โ โ ) |
5 |
2 4
|
mulcomd |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) |
6 |
5
|
oveq2d |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ( ๐ gcd ( ๐ ยท ๐ ) ) = ( ๐ gcd ( ๐ ยท ๐ ) ) ) |
7 |
|
nnnn0 |
โข ( ๐ โ โ โ ๐ โ โ0 ) |
8 |
7
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ๐ โ โ0 ) |
9 |
|
simpr |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ๐ โ โค ) |
10 |
8 9
|
gcdmultipled |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ( ๐ gcd ( ๐ ยท ๐ ) ) = ๐ ) |
11 |
6 10
|
eqtrd |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ( ๐ gcd ( ๐ ยท ๐ ) ) = ๐ ) |