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

Metamath Proof Explorer

Theorem phibndlem

Description: Lemma for phibnd . (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion phibndlem 
|- ( N e. ( ZZ>= ` 2 ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
2 fzm1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( x e. ( 1 ... N ) <-> ( x e. ( 1 ... ( N - 1 ) ) \/ x = N ) ) )
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 2 3 eleq2s 
 |-  ( N e. NN -> ( x e. ( 1 ... N ) <-> ( x e. ( 1 ... ( N - 1 ) ) \/ x = N ) ) )
5 4 biimpa 
 |-  ( ( N e. NN /\ x e. ( 1 ... N ) ) -> ( x e. ( 1 ... ( N - 1 ) ) \/ x = N ) )
6 5 ord 
 |-  ( ( N e. NN /\ x e. ( 1 ... N ) ) -> ( -. x e. ( 1 ... ( N - 1 ) ) -> x = N ) )
7 1 6 sylan 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 1 ... N ) ) -> ( -. x e. ( 1 ... ( N - 1 ) ) -> x = N ) )
8 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
9 gcdid 
 |-  ( N e. ZZ -> ( N gcd N ) = ( abs ` N ) )
10 8 9 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N gcd N ) = ( abs ` N ) )
11 nnre 
 |-  ( N e. NN -> N e. RR )
12 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
13 12 nn0ge0d 
 |-  ( N e. NN -> 0 <_ N )
14 11 13 absidd 
 |-  ( N e. NN -> ( abs ` N ) = N )
15 1 14 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( abs ` N ) = N )
16 10 15 eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N gcd N ) = N )
17 1re 
 |-  1 e. RR
18 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
19 ltne 
 |-  ( ( 1 e. RR /\ 1 < N ) -> N =/= 1 )
20 17 18 19 sylancr 
 |-  ( N e. ( ZZ>= ` 2 ) -> N =/= 1 )
21 16 20 eqnetrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N gcd N ) =/= 1 )
22 oveq1 
 |-  ( x = N -> ( x gcd N ) = ( N gcd N ) )
23 22 neeq1d 
 |-  ( x = N -> ( ( x gcd N ) =/= 1 <-> ( N gcd N ) =/= 1 ) )
24 21 23 syl5ibrcom 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( x = N -> ( x gcd N ) =/= 1 ) )
25 24 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 1 ... N ) ) -> ( x = N -> ( x gcd N ) =/= 1 ) )
26 7 25 syld 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 1 ... N ) ) -> ( -. x e. ( 1 ... ( N - 1 ) ) -> ( x gcd N ) =/= 1 ) )
27 26 necon4bd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 1 ... N ) ) -> ( ( x gcd N ) = 1 -> x e. ( 1 ... ( N - 1 ) ) ) )
28 27 ralrimiva 
 |-  ( N e. ( ZZ>= ` 2 ) -> A. x e. ( 1 ... N ) ( ( x gcd N ) = 1 -> x e. ( 1 ... ( N - 1 ) ) ) )
29 rabss 
 |-  ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... ( N - 1 ) ) <-> A. x e. ( 1 ... N ) ( ( x gcd N ) = 1 -> x e. ( 1 ... ( N - 1 ) ) ) )
30 28 29 sylibr 
 |-  ( N e. ( ZZ>= ` 2 ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... ( N - 1 ) ) )