This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℤ ‘ 𝑁 ) ‘ 𝐴 ) ∥ ( ϕ ‘ 𝑁 ) )