This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑁 ) ∥ 𝑁 ) )