Metamath Proof Explorer

Theorem lcmid

Description: The lcm of an integer and itself is its absolute value. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmid 
|- ( M e. ZZ -> ( M lcm M ) = ( abs ` M ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( M = 0 -> ( M lcm M ) = ( M lcm 0 ) )
2 fveq2 
 |-  ( M = 0 -> ( abs ` M ) = ( abs ` 0 ) )
3 abs0 
 |-  ( abs ` 0 ) = 0
4 2 3 eqtrdi 
 |-  ( M = 0 -> ( abs ` M ) = 0 )
5 1 4 eqeq12d 
 |-  ( M = 0 -> ( ( M lcm M ) = ( abs ` M ) <-> ( M lcm 0 ) = 0 ) )
6 lcmcl 
 |-  ( ( M e. ZZ /\ M e. ZZ ) -> ( M lcm M ) e. NN0 )
7 6 nn0cnd 
 |-  ( ( M e. ZZ /\ M e. ZZ ) -> ( M lcm M ) e. CC )
8 7 anidms 
 |-  ( M e. ZZ -> ( M lcm M ) e. CC )
9 8 adantr 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( M lcm M ) e. CC )
10 zabscl 
 |-  ( M e. ZZ -> ( abs ` M ) e. ZZ )
11 10 zcnd 
 |-  ( M e. ZZ -> ( abs ` M ) e. CC )
12 11 adantr 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( abs ` M ) e. CC )
13 zcn 
 |-  ( M e. ZZ -> M e. CC )
14 13 adantr 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> M e. CC )
15 simpr 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> M =/= 0 )
16 14 15 absne0d 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( abs ` M ) =/= 0 )
17 lcmgcd 
 |-  ( ( M e. ZZ /\ M e. ZZ ) -> ( ( M lcm M ) x. ( M gcd M ) ) = ( abs ` ( M x. M ) ) )
18 17 anidms 
 |-  ( M e. ZZ -> ( ( M lcm M ) x. ( M gcd M ) ) = ( abs ` ( M x. M ) ) )
19 gcdid 
 |-  ( M e. ZZ -> ( M gcd M ) = ( abs ` M ) )
20 19 oveq2d 
 |-  ( M e. ZZ -> ( ( M lcm M ) x. ( M gcd M ) ) = ( ( M lcm M ) x. ( abs ` M ) ) )
21 13 13 absmuld 
 |-  ( M e. ZZ -> ( abs ` ( M x. M ) ) = ( ( abs ` M ) x. ( abs ` M ) ) )
22 18 20 21 3eqtr3d 
 |-  ( M e. ZZ -> ( ( M lcm M ) x. ( abs ` M ) ) = ( ( abs ` M ) x. ( abs ` M ) ) )
23 22 adantr 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( ( M lcm M ) x. ( abs ` M ) ) = ( ( abs ` M ) x. ( abs ` M ) ) )
24 9 12 12 16 23 mulcan2ad 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( M lcm M ) = ( abs ` M ) )
25 lcm0val 
 |-  ( M e. ZZ -> ( M lcm 0 ) = 0 )
26 5 24 25 pm2.61ne 
 |-  ( M e. ZZ -> ( M lcm M ) = ( abs ` M ) )