Metamath Proof Explorer

Theorem lgsfcl2

Description: The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 } , see zabsle1 ). (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypotheses lgsval.1 
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )
lgsfcl2.z 
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }
Assertion lgsfcl2 
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> Z )

Proof

Step Hyp Ref Expression
1 lgsval.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )
2 lgsfcl2.z 
 |-  Z = { x e. ZZ | ( abs ` x ) <_ 1 }
3 0z 
 |-  0 e. ZZ
4 0le1 
 |-  0 <_ 1
5 fveq2 
 |-  ( x = 0 -> ( abs ` x ) = ( abs ` 0 ) )
6 abs0 
 |-  ( abs ` 0 ) = 0
7 5 6 eqtrdi 
 |-  ( x = 0 -> ( abs ` x ) = 0 )
8 7 breq1d 
 |-  ( x = 0 -> ( ( abs ` x ) <_ 1 <-> 0 <_ 1 ) )
9 8 2 elrab2 
 |-  ( 0 e. Z <-> ( 0 e. ZZ /\ 0 <_ 1 ) )
10 3 4 9 mpbir2an 
 |-  0 e. Z
11 1z 
 |-  1 e. ZZ
12 1le1 
 |-  1 <_ 1
13 fveq2 
 |-  ( x = 1 -> ( abs ` x ) = ( abs ` 1 ) )
14 abs1 
 |-  ( abs ` 1 ) = 1
15 13 14 eqtrdi 
 |-  ( x = 1 -> ( abs ` x ) = 1 )
16 15 breq1d 
 |-  ( x = 1 -> ( ( abs ` x ) <_ 1 <-> 1 <_ 1 ) )
17 16 2 elrab2 
 |-  ( 1 e. Z <-> ( 1 e. ZZ /\ 1 <_ 1 ) )
18 11 12 17 mpbir2an 
 |-  1 e. Z
19 neg1z 
 |-  -u 1 e. ZZ
20 fveq2 
 |-  ( x = -u 1 -> ( abs ` x ) = ( abs ` -u 1 ) )
21 ax-1cn 
 |-  1 e. CC
22 21 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
23 22 14 eqtri 
 |-  ( abs ` -u 1 ) = 1
24 20 23 eqtrdi 
 |-  ( x = -u 1 -> ( abs ` x ) = 1 )
25 24 breq1d 
 |-  ( x = -u 1 -> ( ( abs ` x ) <_ 1 <-> 1 <_ 1 ) )
26 25 2 elrab2 
 |-  ( -u 1 e. Z <-> ( -u 1 e. ZZ /\ 1 <_ 1 ) )
27 19 12 26 mpbir2an 
 |-  -u 1 e. Z
28 18 27 ifcli 
 |-  if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) e. Z
29 10 28 ifcli 
 |-  if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) e. Z
30 29 a1i 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) /\ n = 2 ) -> if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) e. Z )
31 simpl1 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) -> A e. ZZ )
32 31 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) /\ -. n = 2 ) -> A e. ZZ )
33 simplr 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) /\ -. n = 2 ) -> n e. Prime )
34 simpr 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) /\ -. n = 2 ) -> -. n = 2 )
35 34 neqned 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) /\ -. n = 2 ) -> n =/= 2 )
36 eldifsn 
 |-  ( n e. ( Prime \ { 2 } ) <-> ( n e. Prime /\ n =/= 2 ) )
37 33 35 36 sylanbrc 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) /\ -. n = 2 ) -> n e. ( Prime \ { 2 } ) )
38 2 lgslem4 
 |-  ( ( A e. ZZ /\ n e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) e. Z )
39 32 37 38 syl2anc 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) /\ -. n = 2 ) -> ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) e. Z )
40 30 39 ifclda 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) -> if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) e. Z )
41 simpr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) -> n e. Prime )
42 simpll2 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) -> N e. ZZ )
43 simpll3 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) -> N =/= 0 )
44 pczcl 
 |-  ( ( n e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( n pCnt N ) e. NN0 )
45 41 42 43 44 syl12anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) -> ( n pCnt N ) e. NN0 )
46 2 ssrab3 
 |-  Z C_ ZZ
47 zsscn 
 |-  ZZ C_ CC
48 46 47 sstri 
 |-  Z C_ CC
49 2 lgslem3 
 |-  ( ( a e. Z /\ b e. Z ) -> ( a x. b ) e. Z )
50 48 49 18 expcllem 
 |-  ( ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) e. Z /\ ( n pCnt N ) e. NN0 ) -> ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) e. Z )
51 40 45 50 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ n e. Prime ) -> ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) e. Z )
52 18 a1i 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) /\ -. n e. Prime ) -> 1 e. Z )
53 51 52 ifclda 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. NN ) -> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) e. Z )
54 53 1 fmptd 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> Z )