Metamath Proof Explorer

Theorem odzcl

Description: The order of a group element is an integer. (Contributed by Mario Carneiro, 28-Feb-2014)

		Ref	Expression
	Assertion	odzcl	\|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) e. NN )

Step	Hyp	Ref	Expression
1		odzcllem	\|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( ( odZ ` N ) ` A ) e. NN /\ N \|\| ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) )
2	1	simpld	\|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) e. NN )

Step

Hyp

Ref

Expression

 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( ( odZ ` N ) ` A ) e. NN /\ N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) )

 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) e. NN )