Metamath Proof Explorer

Theorem phibnd

Description: A slightly tighter bound on the value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion phibnd ⊢ N ∈ ℤ ≥ 2 → ϕ ⁡ N ≤ N − 1

Proof

Step Hyp Ref Expression
1 fzfi ⊢ 1 … N − 1 ∈ Fin
2 phibndlem ⊢ N ∈ ℤ ≥ 2 → x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N − 1
3 ssdomg ⊢ 1 … N − 1 ∈ Fin → x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N − 1 → x ∈ 1 … N | x gcd N = 1 ≼ 1 … N − 1
4 1 2 3 mpsyl ⊢ N ∈ ℤ ≥ 2 → x ∈ 1 … N | x gcd N = 1 ≼ 1 … N − 1
5 fzfi ⊢ 1 … N ∈ Fin
6 ssrab2 ⊢ x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N
7 ssfi ⊢ 1 … N ∈ Fin ∧ x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N → x ∈ 1 … N | x gcd N = 1 ∈ Fin
8 5 6 7 mp2an ⊢ x ∈ 1 … N | x gcd N = 1 ∈ Fin
9 hashdom ⊢ x ∈ 1 … N | x gcd N = 1 ∈ Fin ∧ 1 … N − 1 ∈ Fin → x ∈ 1 … N | x gcd N = 1 ≤ 1 … N − 1 ↔ x ∈ 1 … N | x gcd N = 1 ≼ 1 … N − 1
10 8 1 9 mp2an ⊢ x ∈ 1 … N | x gcd N = 1 ≤ 1 … N − 1 ↔ x ∈ 1 … N | x gcd N = 1 ≼ 1 … N − 1
11 4 10 sylibr ⊢ N ∈ ℤ ≥ 2 → x ∈ 1 … N | x gcd N = 1 ≤ 1 … N − 1
12 eluz2nn ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ
13 phival ⊢ N ∈ ℕ → ϕ ⁡ N = x ∈ 1 … N | x gcd N = 1
14 12 13 syl ⊢ N ∈ ℤ ≥ 2 → ϕ ⁡ N = x ∈ 1 … N | x gcd N = 1
15 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
16 hashfz1 ⊢ N − 1 ∈ ℕ 0 → 1 … N − 1 = N − 1
17 12 15 16 3syl ⊢ N ∈ ℤ ≥ 2 → 1 … N − 1 = N − 1
18 17 eqcomd ⊢ N ∈ ℤ ≥ 2 → N − 1 = 1 … N − 1
19 11 14 18 3brtr4d ⊢ N ∈ ℤ ≥ 2 → ϕ ⁡ N ≤ N − 1