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	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
Assertion	lgsfle1	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑀 ∈ ℕ ) → ( abs ‘ ( 𝐹 ‘ 𝑀 ) ) ≤ 1 )

Proof

Step	Hyp	Ref	Expression
1		lgsval.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
2		eqid	⊢ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
3	1 2	lgsfcl2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝐹 : ℕ ⟶ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
4	3	ffvelrnda	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑀 ∈ ℕ ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
5		fveq2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑀 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑀 ) ) )
6	5	breq1d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑀 ) → ( ( abs ‘ 𝑥 ) ≤ 1 ↔ ( abs ‘ ( 𝐹 ‘ 𝑀 ) ) ≤ 1 ) )
7	6	elrab	⊢ ( ( 𝐹 ‘ 𝑀 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } ↔ ( ( 𝐹 ‘ 𝑀 ) ∈ ℤ ∧ ( abs ‘ ( 𝐹 ‘ 𝑀 ) ) ≤ 1 ) )
8	7	simprbi	⊢ ( ( 𝐹 ‘ 𝑀 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } → ( abs ‘ ( 𝐹 ‘ 𝑀 ) ) ≤ 1 )
9	4 8	syl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑀 ∈ ℕ ) → ( abs ‘ ( 𝐹 ‘ 𝑀 ) ) ≤ 1 )