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

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 ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ϕ ‘ 𝑁 ) ≤ ( 𝑁 − 1 ) )

Proof

Step Hyp Ref Expression
1 fzfi ⊢ ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin
2 phibndlem ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ... ( 𝑁 − 1 ) ) )
3 ssdomg ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin → ( { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ... ( 𝑁 − 1 ) ) → { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ≼ ( 1 ... ( 𝑁 − 1 ) ) ) )
4 1 2 3 mpsyl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ≼ ( 1 ... ( 𝑁 − 1 ) ) )
5 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
6 ssrab2 ⊢ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ... 𝑁 )
7 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ... 𝑁 ) ) → { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∈ Fin )
8 5 6 7 mp2an ⊢ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∈ Fin
9 hashdom ⊢ ( ( { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∈ Fin ∧ ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) ≤ ( ♯ ‘ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ≼ ( 1 ... ( 𝑁 − 1 ) ) ) )
10 8 1 9 mp2an ⊢ ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) ≤ ( ♯ ‘ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ≼ ( 1 ... ( 𝑁 − 1 ) ) )
11 4 10 sylibr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) ≤ ( ♯ ‘ ( 1 ... ( 𝑁 − 1 ) ) ) )
12 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
13 phival ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
14 12 13 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
15 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
16 hashfz1 ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑁 − 1 ) ) ) = ( 𝑁 − 1 ) )
17 12 15 16 3syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ♯ ‘ ( 1 ... ( 𝑁 − 1 ) ) ) = ( 𝑁 − 1 ) )
18 17 eqcomd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) = ( ♯ ‘ ( 1 ... ( 𝑁 − 1 ) ) ) )
19 11 14 18 3brtr4d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ϕ ‘ 𝑁 ) ≤ ( 𝑁 − 1 ) )