Metamath Proof Explorer

Theorem phicl2

Description: Bounds and closure for the value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion phicl2 
|- ( N e. NN -> ( phi ` N ) e. ( 1 ... N ) )

Proof

Step Hyp Ref Expression
1 phival 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
2 fzfi 
 |-  ( 1 ... N ) e. Fin
3 ssrab2 
 |-  { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... N )
4 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 )
5 2 3 4 mp2an 
 |-  { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. Fin
6 hashcl 
 |-  ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. Fin -> ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. NN0 )
7 5 6 ax-mp 
 |-  ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. NN0
8 7 nn0zi 
 |-  ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. ZZ
9 8 a1i 
 |-  ( N e. NN -> ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. ZZ )
10 1z 
 |-  1 e. ZZ
11 hashsng 
 |-  ( 1 e. ZZ -> ( # ` { 1 } ) = 1 )
12 10 11 ax-mp 
 |-  ( # ` { 1 } ) = 1
13 ovex 
 |-  ( 1 ... N ) e. _V
14 13 rabex 
 |-  { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. _V
15 oveq1 
 |-  ( x = 1 -> ( x gcd N ) = ( 1 gcd N ) )
16 15 eqeq1d 
 |-  ( x = 1 -> ( ( x gcd N ) = 1 <-> ( 1 gcd N ) = 1 ) )
17 eluzfz1 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
18 nnuz 
 |-  NN = ( ZZ>= ` 1 )
19 17 18 eleq2s 
 |-  ( N e. NN -> 1 e. ( 1 ... N ) )
20 nnz 
 |-  ( N e. NN -> N e. ZZ )
21 1gcd 
 |-  ( N e. ZZ -> ( 1 gcd N ) = 1 )
22 20 21 syl 
 |-  ( N e. NN -> ( 1 gcd N ) = 1 )
23 16 19 22 elrabd 
 |-  ( N e. NN -> 1 e. { x e. ( 1 ... N ) | ( x gcd N ) = 1 } )
24 23 snssd 
 |-  ( N e. NN -> { 1 } C_ { x e. ( 1 ... N ) | ( x gcd N ) = 1 } )
25 ssdomg 
 |-  ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. _V -> ( { 1 } C_ { x e. ( 1 ... N ) | ( x gcd N ) = 1 } -> { 1 } ~<_ { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
26 14 24 25 mpsyl 
 |-  ( N e. NN -> { 1 } ~<_ { x e. ( 1 ... N ) | ( x gcd N ) = 1 } )
27 snfi 
 |-  { 1 } e. Fin
28 hashdom 
 |-  ( ( { 1 } e. Fin /\ { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. Fin ) -> ( ( # ` { 1 } ) <_ ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <-> { 1 } ~<_ { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
29 27 5 28 mp2an 
 |-  ( ( # ` { 1 } ) <_ ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <-> { 1 } ~<_ { x e. ( 1 ... N ) | ( x gcd N ) = 1 } )
30 26 29 sylibr 
 |-  ( N e. NN -> ( # ` { 1 } ) <_ ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
31 12 30 eqbrtrrid 
 |-  ( N e. NN -> 1 <_ ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
32 ssdomg 
 |-  ( ( 1 ... N ) e. _V -> ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... N ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ~<_ ( 1 ... N ) ) )
33 13 3 32 mp2 
 |-  { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ~<_ ( 1 ... N )
34 hashdom 
 |-  ( ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ ( # ` ( 1 ... N ) ) <-> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ~<_ ( 1 ... N ) ) )
35 5 2 34 mp2an 
 |-  ( ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ ( # ` ( 1 ... N ) ) <-> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ~<_ ( 1 ... N ) )
36 33 35 mpbir 
 |-  ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ ( # ` ( 1 ... N ) )
37 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
38 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
39 37 38 syl 
 |-  ( N e. NN -> ( # ` ( 1 ... N ) ) = N )
40 36 39 breqtrid 
 |-  ( N e. NN -> ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ N )
41 elfz1 
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. ( 1 ... N ) <-> ( ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. ZZ /\ 1 <_ ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) /\ ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ N ) ) )
42 10 20 41 sylancr 
 |-  ( N e. NN -> ( ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. ( 1 ... N ) <-> ( ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. ZZ /\ 1 <_ ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) /\ ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) <_ N ) ) )
43 9 31 40 42 mpbir3and 
 |-  ( N e. NN -> ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. ( 1 ... N ) )
44 1 43 eqeltrd 
 |-  ( N e. NN -> ( phi ` N ) e. ( 1 ... N ) )