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 ) )