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	$$⊢\left(N\in \mathbb{N}\wedge A\in \mathbb{Z}\wedge A\gcd N=1\right)\to N\parallel \left(A^{{\mathrm{od}}_{\mathbb{Z}}\left(N\right)\left(A\right)}-1\right)$$

Proof

Step	Hyp	Ref	Expression
1		odzcllem	$$⊢\left(N\in \mathbb{N}\wedge A\in \mathbb{Z}\wedge A\gcd N=1\right)\to \left({\mathrm{od}}_{\mathbb{Z}}\left(N\right)\left(A\right)\in \mathbb{N}\wedge N\parallel \left(A^{{\mathrm{od}}_{\mathbb{Z}}\left(N\right)\left(A\right)}-1\right)\right)$$
2	1	simprd	$$⊢\left(N\in \mathbb{N}\wedge A\in \mathbb{Z}\wedge A\gcd N=1\right)\to N\parallel \left(A^{{\mathrm{od}}_{\mathbb{Z}}\left(N\right)\left(A\right)}-1\right)$$