This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
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 ⊢ ( 𝜑 → 𝑃 ∈ ℕ )