Metamath Proof Explorer

Theorem fissn0dvds

Description: For each finite subset of the integers not containing 0 there is a positive integer which is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020)

		Ref	Expression
	Assertion	fissn0dvds	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \exists n \in ℕ \forall m \in Z m ∥ n$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to Z \subseteq ℤ$
2		simp2	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to Z \in Fin$
3		eqid	$⊢ \|\prod_{k \in Z} k\| = \|\prod_{k \in Z} k\|$
4		simp3	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to 0 \notin Z$
5	1 2 3 4	absprodnn	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \|\prod_{k \in Z} k\| \in ℕ$
6		breq2	$⊢ n = \|\prod_{k \in Z} k\| \to (m ∥ n \leftrightarrow m ∥ \|\prod_{k \in Z} k\|)$
7	6	ralbidv	$⊢ n = \|\prod_{k \in Z} k\| \to (\forall m \in Z m ∥ n \leftrightarrow \forall m \in Z m ∥ \|\prod_{k \in Z} k\|)$
8	7	adantl	$⊢ ((Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \land n = \|\prod_{k \in Z} k\|) \to (\forall m \in Z m ∥ n \leftrightarrow \forall m \in Z m ∥ \|\prod_{k \in Z} k\|)$
9	1 2 3	absproddvds	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \forall m \in Z m ∥ \|\prod_{k \in Z} k\|$
10	5 8 9	rspcedvd	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \exists n \in ℕ \forall m \in Z m ∥ n$