Metamath Proof Explorer


Theorem gcdmultiplez

Description: The GCD of a multiple of an integer is the integer itself. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by AV, 12-Jan-2023)

Ref Expression
Assertion gcdmultiplez ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘€ gcd ( ๐‘€ ยท ๐‘ ) ) = ๐‘€ )

Proof

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 ( ๐‘€ ยท ๐‘ ) ) = ๐‘€ )