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 ‘ 𝑀 ) ) |