Metamath Proof Explorer


Theorem lcm1

Description: The lcm of an integer and 1 is the absolute value of the integer. (Contributed by AV, 23-Aug-2020)

Ref Expression
Assertion lcm1 ( ๐‘€ โˆˆ โ„ค โ†’ ( ๐‘€ lcm 1 ) = ( abs โ€˜ ๐‘€ ) )

Proof

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 โ€˜ ๐‘€ ) )