lcmdvdsb

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

		Ref	Expression
	Assertion	lcmdvdsb	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M ∥ K \land N ∥ K) \leftrightarrow (M lcm N) ∥ K)$

Proof

Step	Hyp	Ref	Expression
1		lcmdvds	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M ∥ K \land N ∥ K) \to (M lcm N) ∥ K)$
2		dvdslcm	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ (M lcm N) \land N ∥ (M lcm N))$
3	2	simpld	$⊢ (M \in ℤ \land N \in ℤ) \to M ∥ (M lcm N)$
4	3	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M ∥ (M lcm N)$
5		simp2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \in ℤ$
6		lcmcl	$⊢ (M \in ℤ \land N \in ℤ) \to M lcm N \in ℕ_{0}$
7	6	nn0zd	$⊢ (M \in ℤ \land N \in ℤ) \to M lcm N \in ℤ$
8	7	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M lcm N \in ℤ$
9		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
10		dvdstr	$⊢ (M \in ℤ \land M lcm N \in ℤ \land K \in ℤ) \to ((M ∥ (M lcm N) \land (M lcm N) ∥ K) \to M ∥ K)$
11	5 8 9 10	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M ∥ (M lcm N) \land (M lcm N) ∥ K) \to M ∥ K)$
12	4 11	mpand	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M lcm N) ∥ K \to M ∥ K)$
13	2	simprd	$⊢ (M \in ℤ \land N \in ℤ) \to N ∥ (M lcm N)$
14	13	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to N ∥ (M lcm N)$
15		dvdstr	$⊢ (N \in ℤ \land M lcm N \in ℤ \land K \in ℤ) \to ((N ∥ (M lcm N) \land (M lcm N) ∥ K) \to N ∥ K)$
16	15	3com13	$⊢ (K \in ℤ \land M lcm N \in ℤ \land N \in ℤ) \to ((N ∥ (M lcm N) \land (M lcm N) ∥ K) \to N ∥ K)$
17	8 16	syld3an2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((N ∥ (M lcm N) \land (M lcm N) ∥ K) \to N ∥ K)$
18	14 17	mpand	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M lcm N) ∥ K \to N ∥ K)$
19	12 18	jcad	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M lcm N) ∥ K \to (M ∥ K \land N ∥ K))$
20	1 19	impbid	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M ∥ K \land N ∥ K) \leftrightarrow (M lcm N) ∥ K)$

Metamath Proof Explorer

Theorem lcmdvdsb

Proof