Theorem mulgnn0cld

Description: Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl . (Contributed by SN, 1-Feb-2025)

	Ref	Expression
Hypotheses	mulgnn0cld.b	|- B = ( Base ` G )
	mulgnn0cld.t	|- .x. = ( .g ` G )
	mulgnn0cld.m	|- ( ph -> G e. Mnd )
	mulgnn0cld.n	|- ( ph -> N e. NN0 )
	mulgnn0cld.x	|- ( ph -> X e. B )
Assertion	mulgnn0cld	|- ( ph -> ( N .x. X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		mulgnn0cld.b	|- B = ( Base ` G )
2		mulgnn0cld.t	|- .x. = ( .g ` G )
3		mulgnn0cld.m	|- ( ph -> G e. Mnd )
4		mulgnn0cld.n	|- ( ph -> N e. NN0 )
5		mulgnn0cld.x	|- ( ph -> X e. B )
6	1 2	mulgnn0cl	|- ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .x. X ) e. B )
7	3 4 5 6	syl3anc	|- ( ph -> ( N .x. X ) e. B )