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 ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ A gcd N = 1 → odℤ ⁡ N ⁡ A ∥ ϕ ⁡ N

Proof

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