Theorem odzcl

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

	Ref	Expression
Assertion	odzcl	$$⊢\left(N\in \mathbb{N}\wedge A\in \mathbb{Z}\wedge A\gcd N=1\right)\to {\mathrm{od}}_{\mathbb{Z}}\left(N\right)\left(A\right)\in \mathbb{N}$$

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