lcmfdvdsb

Description: Biconditional form of lcmfdvds . (Contributed by AV, 26-Aug-2020)

		Ref	Expression
	Assertion	lcmfdvdsb	$⊢ (K \in ℤ \land Z \subseteq ℤ \land Z \in Fin) \to (\forall m \in Z m ∥ K \leftrightarrow \underline{lcm} (Z) ∥ K)$

Proof

Step	Hyp	Ref	Expression
1		lcmfdvds	$⊢ (K \in ℤ \land Z \subseteq ℤ \land Z \in Fin) \to (\forall m \in Z m ∥ K \to \underline{lcm} (Z) ∥ K)$
2		dvdslcmf	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to \forall x \in Z x ∥ \underline{lcm} (Z)$
3		breq1	$⊢ x = m \to (x ∥ \underline{lcm} (Z) \leftrightarrow m ∥ \underline{lcm} (Z))$
4	3	rspcv	$⊢ m \in Z \to (\forall x \in Z x ∥ \underline{lcm} (Z) \to m ∥ \underline{lcm} (Z))$
5		ssel	$⊢ Z \subseteq ℤ \to (m \in Z \to m \in ℤ)$
6	5	adantr	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to (m \in Z \to m \in ℤ)$
7	6	com12	$⊢ m \in Z \to ((Z \subseteq ℤ \land Z \in Fin) \to m \in ℤ)$
8	7	adantr	$⊢ (m \in Z \land K \in ℤ) \to ((Z \subseteq ℤ \land Z \in Fin) \to m \in ℤ)$
9	8	imp	$⊢ ((m \in Z \land K \in ℤ) \land (Z \subseteq ℤ \land Z \in Fin)) \to m \in ℤ$
10		lcmfcl	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to \underline{lcm} (Z) \in ℕ_{0}$
11	10	nn0zd	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to \underline{lcm} (Z) \in ℤ$
12	11	adantl	$⊢ ((m \in Z \land K \in ℤ) \land (Z \subseteq ℤ \land Z \in Fin)) \to \underline{lcm} (Z) \in ℤ$
13		simplr	$⊢ ((m \in Z \land K \in ℤ) \land (Z \subseteq ℤ \land Z \in Fin)) \to K \in ℤ$
14		dvdstr	$⊢ (m \in ℤ \land \underline{lcm} (Z) \in ℤ \land K \in ℤ) \to ((m ∥ \underline{lcm} (Z) \land \underline{lcm} (Z) ∥ K) \to m ∥ K)$
15	9 12 13 14	syl3anc	$⊢ ((m \in Z \land K \in ℤ) \land (Z \subseteq ℤ \land Z \in Fin)) \to ((m ∥ \underline{lcm} (Z) \land \underline{lcm} (Z) ∥ K) \to m ∥ K)$
16	15	expd	$⊢ ((m \in Z \land K \in ℤ) \land (Z \subseteq ℤ \land Z \in Fin)) \to (m ∥ \underline{lcm} (Z) \to (\underline{lcm} (Z) ∥ K \to m ∥ K))$
17	16	exp31	$⊢ m \in Z \to (K \in ℤ \to ((Z \subseteq ℤ \land Z \in Fin) \to (m ∥ \underline{lcm} (Z) \to (\underline{lcm} (Z) ∥ K \to m ∥ K))))$
18	17	com23	$⊢ m \in Z \to ((Z \subseteq ℤ \land Z \in Fin) \to (K \in ℤ \to (m ∥ \underline{lcm} (Z) \to (\underline{lcm} (Z) ∥ K \to m ∥ K))))$
19	18	com24	$⊢ m \in Z \to (m ∥ \underline{lcm} (Z) \to (K \in ℤ \to ((Z \subseteq ℤ \land Z \in Fin) \to (\underline{lcm} (Z) ∥ K \to m ∥ K))))$
20	19	com45	$⊢ m \in Z \to (m ∥ \underline{lcm} (Z) \to (K \in ℤ \to (\underline{lcm} (Z) ∥ K \to ((Z \subseteq ℤ \land Z \in Fin) \to m ∥ K))))$
21	4 20	syld	$⊢ m \in Z \to (\forall x \in Z x ∥ \underline{lcm} (Z) \to (K \in ℤ \to (\underline{lcm} (Z) ∥ K \to ((Z \subseteq ℤ \land Z \in Fin) \to m ∥ K))))$
22	21	com15	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to (\forall x \in Z x ∥ \underline{lcm} (Z) \to (K \in ℤ \to (\underline{lcm} (Z) ∥ K \to (m \in Z \to m ∥ K))))$
23	2 22	mpd	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to (K \in ℤ \to (\underline{lcm} (Z) ∥ K \to (m \in Z \to m ∥ K)))$
24	23	com12	$⊢ K \in ℤ \to ((Z \subseteq ℤ \land Z \in Fin) \to (\underline{lcm} (Z) ∥ K \to (m \in Z \to m ∥ K)))$
25	24	3impib	$⊢ (K \in ℤ \land Z \subseteq ℤ \land Z \in Fin) \to (\underline{lcm} (Z) ∥ K \to (m \in Z \to m ∥ K))$
26	25	ralrimdv	$⊢ (K \in ℤ \land Z \subseteq ℤ \land Z \in Fin) \to (\underline{lcm} (Z) ∥ K \to \forall m \in Z m ∥ K)$
27	1 26	impbid	$⊢ (K \in ℤ \land Z \subseteq ℤ \land Z \in Fin) \to (\forall m \in Z m ∥ K \leftrightarrow \underline{lcm} (Z) ∥ K)$

Metamath Proof Explorer

Theorem lcmfdvdsb

Proof