Step |
Hyp |
Ref |
Expression |
1 |
|
gcd1 |
โข ( ๐ โ โค โ ( ๐ gcd 1 ) = 1 ) |
2 |
1
|
oveq2d |
โข ( ๐ โ โค โ ( ( ๐ lcm 1 ) ยท ( ๐ gcd 1 ) ) = ( ( ๐ lcm 1 ) ยท 1 ) ) |
3 |
|
1z |
โข 1 โ โค |
4 |
|
lcmcl |
โข ( ( ๐ โ โค โง 1 โ โค ) โ ( ๐ lcm 1 ) โ โ0 ) |
5 |
3 4
|
mpan2 |
โข ( ๐ โ โค โ ( ๐ lcm 1 ) โ โ0 ) |
6 |
5
|
nn0cnd |
โข ( ๐ โ โค โ ( ๐ lcm 1 ) โ โ ) |
7 |
6
|
mulid1d |
โข ( ๐ โ โค โ ( ( ๐ lcm 1 ) ยท 1 ) = ( ๐ lcm 1 ) ) |
8 |
2 7
|
eqtr2d |
โข ( ๐ โ โค โ ( ๐ lcm 1 ) = ( ( ๐ lcm 1 ) ยท ( ๐ gcd 1 ) ) ) |
9 |
|
lcmgcd |
โข ( ( ๐ โ โค โง 1 โ โค ) โ ( ( ๐ lcm 1 ) ยท ( ๐ gcd 1 ) ) = ( abs โ ( ๐ ยท 1 ) ) ) |
10 |
3 9
|
mpan2 |
โข ( ๐ โ โค โ ( ( ๐ lcm 1 ) ยท ( ๐ gcd 1 ) ) = ( abs โ ( ๐ ยท 1 ) ) ) |
11 |
|
zcn |
โข ( ๐ โ โค โ ๐ โ โ ) |
12 |
11
|
mulid1d |
โข ( ๐ โ โค โ ( ๐ ยท 1 ) = ๐ ) |
13 |
12
|
fveq2d |
โข ( ๐ โ โค โ ( abs โ ( ๐ ยท 1 ) ) = ( abs โ ๐ ) ) |
14 |
8 10 13
|
3eqtrd |
โข ( ๐ โ โค โ ( ๐ lcm 1 ) = ( abs โ ๐ ) ) |