Metamath Proof Explorer

Theorem odzid

Description: Any element raised to the power of its order is 1 . (Contributed by Mario Carneiro, 28-Feb-2014)

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

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	simprd	\|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N \|\| ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) )

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 ) -> N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) )