Metamath Proof Explorer

Theorem absprodnn

Description: The absolute value of the product of the elements of a finite subset of the integers not containing 0 is a poitive integer. (Contributed by AV, 21-Aug-2020)

		Ref	Expression
	Hypotheses	absproddvds.s	$⊢ φ \to Z \subseteq ℤ$
		absproddvds.f	$⊢ φ \to Z \in Fin$
		absproddvds.p	$⊢ P = \|\prod_{z \in Z} z\|$
		absprodnn.z	$⊢ φ \to 0 \notin Z$
	Assertion	absprodnn	$⊢ φ \to P \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		absproddvds.s	$⊢ φ \to Z \subseteq ℤ$
2		absproddvds.f	$⊢ φ \to Z \in Fin$
3		absproddvds.p	$⊢ P = \|\prod_{z \in Z} z\|$
4		absprodnn.z	$⊢ φ \to 0 \notin Z$
5	1	sselda	$⊢ (φ \land z \in Z) \to z \in ℤ$
6	2 5	fprodzcl	$⊢ φ \to \prod_{z \in Z} z \in ℤ$
7	5	zcnd	$⊢ (φ \land z \in Z) \to z \in ℂ$
8		elnelne2	$⊢ (z \in Z \land 0 \notin Z) \to z \neq 0$
9	8	expcom	$⊢ 0 \notin Z \to (z \in Z \to z \neq 0)$
10	4 9	syl	$⊢ φ \to (z \in Z \to z \neq 0)$
11	10	imp	$⊢ (φ \land z \in Z) \to z \neq 0$
12	2 7 11	fprodn0	$⊢ φ \to \prod_{z \in Z} z \neq 0$
13		nnabscl	$⊢ (\prod_{z \in Z} z \in ℤ \land \prod_{z \in Z} z \neq 0) \to \|\prod_{z \in Z} z\| \in ℕ$
14	6 12 13	syl2anc	$⊢ φ \to \|\prod_{z \in Z} z\| \in ℕ$
15	3 14	eqeltrid	$⊢ φ \to P \in ℕ$