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	|- ( ph -> Z C_ ZZ )
	absproddvds.f	|- ( ph -> Z e. Fin )
	absproddvds.p	|- P = ( abs ` prod_ z e. Z z )
	absprodnn.z	|- ( ph -> 0 e/ Z )
Assertion	absprodnn	|- ( ph -> P e. NN )

Proof

Step	Hyp	Ref	Expression
1		absproddvds.s	|- ( ph -> Z C_ ZZ )
2		absproddvds.f	|- ( ph -> Z e. Fin )
3		absproddvds.p	|- P = ( abs ` prod_ z e. Z z )
4		absprodnn.z	|- ( ph -> 0 e/ Z )
5	1	sselda	|- ( ( ph /\ z e. Z ) -> z e. ZZ )
6	2 5	fprodzcl	|- ( ph -> prod_ z e. Z z e. ZZ )
7	5	zcnd	|- ( ( ph /\ z e. Z ) -> z e. CC )
8		elnelne2	|- ( ( z e. Z /\ 0 e/ Z ) -> z =/= 0 )
9	8	expcom	|- ( 0 e/ Z -> ( z e. Z -> z =/= 0 ) )
10	4 9	syl	|- ( ph -> ( z e. Z -> z =/= 0 ) )
11	10	imp	|- ( ( ph /\ z e. Z ) -> z =/= 0 )
12	2 7 11	fprodn0	|- ( ph -> prod_ z e. Z z =/= 0 )
13		nnabscl	|- ( ( prod_ z e. Z z e. ZZ /\ prod_ z e. Z z =/= 0 ) -> ( abs ` prod_ z e. Z z ) e. NN )
14	6 12 13	syl2anc	|- ( ph -> ( abs ` prod_ z e. Z z ) e. NN )
15	3 14	eqeltrid	|- ( ph -> P e. NN )