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 
|- ( N e. ( ZZ>= ` 2 ) -> ( phi ` N ) <_ ( N - 1 ) )

Proof

Step Hyp Ref Expression
1 fzfi 
 |-  ( 1 ... ( N - 1 ) ) e. Fin
2 phibndlem 
 |-  ( N e. ( ZZ>= ` 2 ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... ( N - 1 ) ) )
3 ssdomg 
 |-  ( ( 1 ... ( N - 1 ) ) e. Fin -> ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... ( N - 1 ) ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ~<_ ( 1 ... ( N - 1 ) ) ) )
4 1 2 3 mpsyl 
 |-  ( N e. ( ZZ>= ` 2 ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ~<_ ( 1 ... ( N - 1 ) ) )
5 fzfi 
 |-  ( 1 ... N ) e. Fin
6 ssrab2 
 |-  { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... N )
7 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... N ) ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. Fin )
8 5 6 7 mp2an 
 |-  { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. Fin
9 hashdom 
 |-  ( ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. Fin /\ ( 1 ... ( N - 1 ) ) e. Fin ) -> ( ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ ( # ` ( 1 ... ( N - 1 ) ) ) <-> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ~<_ ( 1 ... ( N - 1 ) ) ) )
10 8 1 9 mp2an 
 |-  ( ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ ( # ` ( 1 ... ( N - 1 ) ) ) <-> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ~<_ ( 1 ... ( N - 1 ) ) )
11 4 10 sylibr 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ ( # ` ( 1 ... ( N - 1 ) ) ) )
12 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
13 phival 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
14 12 13 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( phi ` N ) = ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
15 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
16 hashfz1 
 |-  ( ( N - 1 ) e. NN0 -> ( # ` ( 1 ... ( N - 1 ) ) ) = ( N - 1 ) )
17 12 15 16 3syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( # ` ( 1 ... ( N - 1 ) ) ) = ( N - 1 ) )
18 17 eqcomd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) = ( # ` ( 1 ... ( N - 1 ) ) ) )
19 11 14 18 3brtr4d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( phi ` N ) <_ ( N - 1 ) )