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

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

Metamath Proof Explorer

Theorem lgsfcl2

Proof