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