Theorem lcmdvdsb

Description: Biconditional form of lcmdvds . (Contributed by Steve Rodriguez, 20-Jan-2020)

	Ref	Expression
Assertion	lcmdvdsb	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ↔ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) )

Proof

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