Metamath Proof Explorer

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 ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
Assertion lgsfle1 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ M ∈ ℕ → F ⁡ M ≤ 1

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
2 eqid ⊢ x ∈ ℤ | x ≤ 1 = x ∈ ℤ | x ≤ 1
3 1 2 lgsfcl2 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ x ∈ ℤ | x ≤ 1
4 3 ffvelrnda ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ M ∈ ℕ → F ⁡ M ∈ x ∈ ℤ | x ≤ 1
5 fveq2 ⊢ x = F ⁡ M → x = F ⁡ M
6 5 breq1d ⊢ x = F ⁡ M → x ≤ 1 ↔ F ⁡ M ≤ 1
7 6 elrab ⊢ F ⁡ M ∈ x ∈ ℤ | x ≤ 1 ↔ F ⁡ M ∈ ℤ ∧ F ⁡ M ≤ 1
8 7 simprbi ⊢ F ⁡ M ∈ x ∈ ℤ | x ≤ 1 → F ⁡ M ≤ 1
9 4 8 syl ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ M ∈ ℕ → F ⁡ M ≤ 1