Theorem dvdsgcdb

Description: Biconditional form of dvdsgcd . (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	dvdsgcdb	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ↔ 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsgcd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) )
2		gcddvds	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
3	2	simpld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∥ 𝑀 )
4	3	3adant1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∥ 𝑀 )
5		simp1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
6		gcdcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
7	6	nn0zd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℤ )
8	7	3adant1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℤ )
9		simp2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
10		dvdstr	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ) → 𝐾 ∥ 𝑀 ) )
11	5 8 9 10	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ) → 𝐾 ∥ 𝑀 ) )
12	4 11	mpan2d	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑀 gcd 𝑁 ) → 𝐾 ∥ 𝑀 ) )
13	2	simprd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∥ 𝑁 )
14	13	3adant1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∥ 𝑁 )
15		dvdstr	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) → 𝐾 ∥ 𝑁 ) )
16	8 15	syld3an2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) → 𝐾 ∥ 𝑁 ) )
17	14 16	mpan2d	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑀 gcd 𝑁 ) → 𝐾 ∥ 𝑁 ) )
18	12 17	jcad	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑀 gcd 𝑁 ) → ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) )
19	1 18	impbid	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ↔ 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) )