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 ∈ ℕ ⟼ 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
lgsfcl2.z ⊢ Z = x ∈ ℤ | x ≤ 1
Assertion lgsfcl2 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ Z

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 lgsfcl2.z ⊢ Z = x ∈ ℤ | x ≤ 1
3 0z ⊢ 0 ∈ ℤ
4 0le1 ⊢ 0 ≤ 1
5 fveq2 ⊢ x = 0 → x = 0
6 abs0 ⊢ 0 = 0
7 5 6 eqtrdi ⊢ x = 0 → x = 0
8 7 breq1d ⊢ x = 0 → x ≤ 1 ↔ 0 ≤ 1
9 8 2 elrab2 ⊢ 0 ∈ Z ↔ 0 ∈ ℤ ∧ 0 ≤ 1
10 3 4 9 mpbir2an ⊢ 0 ∈ Z
11 1z ⊢ 1 ∈ ℤ
12 1le1 ⊢ 1 ≤ 1
13 fveq2 ⊢ x = 1 → x = 1
14 abs1 ⊢ 1 = 1
15 13 14 eqtrdi ⊢ x = 1 → x = 1
16 15 breq1d ⊢ x = 1 → x ≤ 1 ↔ 1 ≤ 1
17 16 2 elrab2 ⊢ 1 ∈ Z ↔ 1 ∈ ℤ ∧ 1 ≤ 1
18 11 12 17 mpbir2an ⊢ 1 ∈ Z
19 neg1z ⊢ − 1 ∈ ℤ
20 fveq2 ⊢ x = − 1 → x = − 1
21 ax-1cn ⊢ 1 ∈ ℂ
22 21 absnegi ⊢ − 1 = 1
23 22 14 eqtri ⊢ − 1 = 1
24 20 23 eqtrdi ⊢ x = − 1 → x = 1
25 24 breq1d ⊢ x = − 1 → x ≤ 1 ↔ 1 ≤ 1
26 25 2 elrab2 ⊢ − 1 ∈ Z ↔ − 1 ∈ ℤ ∧ 1 ≤ 1
27 19 12 26 mpbir2an ⊢ − 1 ∈ Z
28 18 27 ifcli ⊢ if A mod 8 ∈ 1 7 1 − 1 ∈ Z
29 10 28 ifcli ⊢ if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ∈ Z
30 29 a1i ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ ∧ n = 2 → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ∈ Z
31 simpl1 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ → A ∈ ℤ
32 31 ad2antrr ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ ∧ ¬ n = 2 → A ∈ ℤ
33 simplr ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ ∧ ¬ n = 2 → n ∈ ℙ
34 simpr ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ ∧ ¬ n = 2 → ¬ n = 2
35 34 neqned ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ ∧ ¬ n = 2 → n ≠ 2
36 eldifsn ⊢ n ∈ ℙ ∖ 2 ↔ n ∈ ℙ ∧ n ≠ 2
37 33 35 36 sylanbrc ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ ∧ ¬ n = 2 → n ∈ ℙ ∖ 2
38 2 lgslem4 ⊢ A ∈ ℤ ∧ n ∈ ℙ ∖ 2 → A n − 1 2 + 1 mod n − 1 ∈ Z
39 32 37 38 syl2anc ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ ∧ ¬ n = 2 → A n − 1 2 + 1 mod n − 1 ∈ Z
40 30 39 ifclda ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ → if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 ∈ Z
41 simpr ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ → n ∈ ℙ
42 simpll2 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ → N ∈ ℤ
43 simpll3 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ → N ≠ 0
44 pczcl ⊢ n ∈ ℙ ∧ N ∈ ℤ ∧ N ≠ 0 → n pCnt N ∈ ℕ 0
45 41 42 43 44 syl12anc ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ n ∈ ℙ → n pCnt N ∈ ℕ 0
46 2 ssrab3 ⊢ Z ⊆ ℤ
47 zsscn ⊢ ℤ ⊆ ℂ
48 46 47 sstri ⊢ Z ⊆ ℂ
49 2 lgslem3 ⊢ a ∈ Z ∧ b ∈ Z → a ⁢ b ∈ Z
50 48 49 18 expcllem ⊢ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 ∈ Z ∧ n pCnt N ∈ ℕ 0 → 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 ∈ Z
51 40 45 50 syl2anc ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ 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 ∈ Z
52 18 a1i ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℕ ∧ ¬ n ∈ ℙ → 1 ∈ Z
53 51 52 ifclda ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ 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 ∈ Z
54 53 1 fmptd ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ Z