odzphi

Description: The order of any group element is a divisor of the Euler phi function. (Contributed by Mario Carneiro, 28-Feb-2014)

		Ref	Expression
	Assertion	odzphi	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to {od}_{ℤ} (N) (A) ∥ ϕ (N)$

Step	Hyp	Ref	Expression
1		eulerth	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A^{ϕ (N)} \mod N = 1 \mod N$
2		simp1	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to N \in ℕ$
3		simp2	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A \in ℤ$
4	2	phicld	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to ϕ (N) \in ℕ$
5	4	nnnn0d	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to ϕ (N) \in ℕ_{0}$
6		zexpcl	$⊢ (A \in ℤ \land ϕ (N) \in ℕ_{0}) \to A^{ϕ (N)} \in ℤ$
7	3 5 6	syl2anc	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A^{ϕ (N)} \in ℤ$
8		1zzd	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to 1 \in ℤ$
9		moddvds	$⊢ (N \in ℕ \land A^{ϕ (N)} \in ℤ \land 1 \in ℤ) \to (A^{ϕ (N)} \mod N = 1 \mod N \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
10	2 7 8 9	syl3anc	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to (A^{ϕ (N)} \mod N = 1 \mod N \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
11	1 10	mpbid	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to N ∥ (A^{ϕ (N)} - 1)$
12		odzdvds	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land ϕ (N) \in ℕ_{0}) \to (N ∥ (A^{ϕ (N)} - 1) \leftrightarrow {od}_{ℤ} (N) (A) ∥ ϕ (N))$
13	5 12	mpdan	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to (N ∥ (A^{ϕ (N)} - 1) \leftrightarrow {od}_{ℤ} (N) (A) ∥ ϕ (N))$
14	11 13	mpbid	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to {od}_{ℤ} (N) (A) ∥ ϕ (N)$

Metamath Proof Explorer