Metamath Proof Explorer


Theorem gcddvds

Description: The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcddvds ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 0z 0 ∈ ℤ
2 dvds0 ( 0 ∈ ℤ → 0 ∥ 0 )
3 1 2 ax-mp 0 ∥ 0
4 breq2 ( 𝑀 = 0 → ( 0 ∥ 𝑀 ↔ 0 ∥ 0 ) )
5 breq2 ( 𝑁 = 0 → ( 0 ∥ 𝑁 ↔ 0 ∥ 0 ) )
6 4 5 bi2anan9 ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 0 ∥ 𝑀 ∧ 0 ∥ 𝑁 ) ↔ ( 0 ∥ 0 ∧ 0 ∥ 0 ) ) )
7 anidm ( ( 0 ∥ 0 ∧ 0 ∥ 0 ) ↔ 0 ∥ 0 )
8 6 7 bitrdi ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 0 ∥ 𝑀 ∧ 0 ∥ 𝑁 ) ↔ 0 ∥ 0 ) )
9 3 8 mpbiri ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 0 ∥ 𝑀 ∧ 0 ∥ 𝑁 ) )
10 oveq12 ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = ( 0 gcd 0 ) )
11 gcd0val ( 0 gcd 0 ) = 0
12 10 11 eqtrdi ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = 0 )
13 12 breq1d ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ↔ 0 ∥ 𝑀 ) )
14 12 breq1d ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ↔ 0 ∥ 𝑁 ) )
15 13 14 anbi12d ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ↔ ( 0 ∥ 𝑀 ∧ 0 ∥ 𝑁 ) ) )
16 9 15 mpbird ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
17 16 adantl ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
18 eqid { 𝑛 ∈ ℤ ∣ ∀ 𝑧 ∈ { 𝑀 , 𝑁 } 𝑛𝑧 } = { 𝑛 ∈ ℤ ∣ ∀ 𝑧 ∈ { 𝑀 , 𝑁 } 𝑛𝑧 }
19 eqid { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } = { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) }
20 18 19 gcdcllem3 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∈ ℕ ∧ ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∥ 𝑀 ∧ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∥ 𝑁 ) ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐾𝑀𝐾𝑁 ) → 𝐾 ≤ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ) ) )
21 20 simp2d ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∥ 𝑀 ∧ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∥ 𝑁 ) )
22 gcdn0val ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) )
23 22 breq1d ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ↔ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∥ 𝑀 ) )
24 22 breq1d ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ↔ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∥ 𝑁 ) )
25 23 24 anbi12d ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ↔ ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∥ 𝑀 ∧ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛𝑀𝑛𝑁 ) } , ℝ , < ) ∥ 𝑁 ) ) )
26 21 25 mpbird ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
27 17 26 pm2.61dan ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )