Theorem 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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∥ ( ϕ ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eulerth	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )
2		simp1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℕ )
3		simp2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝐴 ∈ ℤ )
4	2	phicld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ϕ ‘ 𝑁 ) ∈ ℕ )
5	4	nnnn0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
6		zexpcl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
7	3 5 6	syl2anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
8		1zzd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 1 ∈ ℤ )
9		moddvds	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
10	2 7 8 9	syl3anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
11	1 10	mpbid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
12		odzdvds	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) → ( 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∥ ( ϕ ‘ 𝑁 ) ) )
13	5 12	mpdan	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∥ ( ϕ ‘ 𝑁 ) ) )
14	11 13	mpbid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∥ ( ϕ ‘ 𝑁 ) )