Theorem lgsfle1

Description: The function F has magnitude less or equal to 1 . (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	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 ) )
Assertion	lgsfle1	|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ M e. NN ) -> ( abs ` ( F ` M ) ) <_ 1 )

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		eqid	|- { x e. ZZ | ( abs ` x ) <_ 1 } = { x e. ZZ | ( abs ` x ) <_ 1 }
3	1 2	lgsfcl2	|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> { x e. ZZ | ( abs ` x ) <_ 1 } )
4	3	ffvelrnda	|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ M e. NN ) -> ( F ` M ) e. { x e. ZZ | ( abs ` x ) <_ 1 } )
5		fveq2	|- ( x = ( F ` M ) -> ( abs ` x ) = ( abs ` ( F ` M ) ) )
6	5	breq1d	|- ( x = ( F ` M ) -> ( ( abs ` x ) <_ 1 <-> ( abs ` ( F ` M ) ) <_ 1 ) )
7	6	elrab	|- ( ( F ` M ) e. { x e. ZZ | ( abs ` x ) <_ 1 } <-> ( ( F ` M ) e. ZZ /\ ( abs ` ( F ` M ) ) <_ 1 ) )
8	7	simprbi	|- ( ( F ` M ) e. { x e. ZZ | ( abs ` x ) <_ 1 } -> ( abs ` ( F ` M ) ) <_ 1 )
9	4 8	syl	|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ M e. NN ) -> ( abs ` ( F ` M ) ) <_ 1 )