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	⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
	absproddvds.f	⊢ ( 𝜑 → 𝑍 ∈ Fin )
	absproddvds.p	⊢ 𝑃 = ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 )
	absprodnn.z	⊢ ( 𝜑 → 0 ∉ 𝑍 )
Assertion	absprodnn	⊢ ( 𝜑 → 𝑃 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		absproddvds.s	⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
2		absproddvds.f	⊢ ( 𝜑 → 𝑍 ∈ Fin )
3		absproddvds.p	⊢ 𝑃 = ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 )
4		absprodnn.z	⊢ ( 𝜑 → 0 ∉ 𝑍 )
5	1	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → 𝑧 ∈ ℤ )
6	2 5	fprodzcl	⊢ ( 𝜑 → ∏ 𝑧 ∈ 𝑍 𝑧 ∈ ℤ )
7	5	zcnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → 𝑧 ∈ ℂ )
8		elnelne2	⊢ ( ( 𝑧 ∈ 𝑍 ∧ 0 ∉ 𝑍 ) → 𝑧 ≠ 0 )
9	8	expcom	⊢ ( 0 ∉ 𝑍 → ( 𝑧 ∈ 𝑍 → 𝑧 ≠ 0 ) )
10	4 9	syl	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑍 → 𝑧 ≠ 0 ) )
11	10	imp	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → 𝑧 ≠ 0 )
12	2 7 11	fprodn0	⊢ ( 𝜑 → ∏ 𝑧 ∈ 𝑍 𝑧 ≠ 0 )
13		nnabscl	⊢ ( ( ∏ 𝑧 ∈ 𝑍 𝑧 ∈ ℤ ∧ ∏ 𝑧 ∈ 𝑍 𝑧 ≠ 0 ) → ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) ∈ ℕ )
14	6 12 13	syl2anc	⊢ ( 𝜑 → ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) ∈ ℕ )
15	3 14	eqeltrid	⊢ ( 𝜑 → 𝑃 ∈ ℕ )