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 \in ℕ ⟼ if (n \in ℙ, {if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1)}^{n pCnt N}, 1))$
	lgsfcl2.z	$⊢ Z = \{x \in ℤ \| \|x\| \leq 1\}$
Assertion	lgsfcl2	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to F : ℕ ⟶ Z$

Proof

Step	Hyp	Ref	Expression
1		lgsval.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, {if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1)}^{n pCnt N}, 1))$
2		lgsfcl2.z	$⊢ Z = \{x \in ℤ \| \|x\| \leq 1\}$
3		0z	$⊢ 0 \in ℤ$
4		0le1	$⊢ 0 \leq 1$
5		fveq2	$⊢ x = 0 \to \|x\| = \|0\|$
6		abs0	$⊢ \|0\| = 0$
7	5 6	eqtrdi	$⊢ x = 0 \to \|x\| = 0$
8	7	breq1d	$⊢ x = 0 \to (\|x\| \leq 1 \leftrightarrow 0 \leq 1)$
9	8 2	elrab2	$⊢ 0 \in Z \leftrightarrow (0 \in ℤ \land 0 \leq 1)$
10	3 4 9	mpbir2an	$⊢ 0 \in Z$
11		1z	$⊢ 1 \in ℤ$
12		1le1	$⊢ 1 \leq 1$
13		fveq2	$⊢ x = 1 \to \|x\| = \|1\|$
14		abs1	$⊢ \|1\| = 1$
15	13 14	eqtrdi	$⊢ x = 1 \to \|x\| = 1$
16	15	breq1d	$⊢ x = 1 \to (\|x\| \leq 1 \leftrightarrow 1 \leq 1)$
17	16 2	elrab2	$⊢ 1 \in Z \leftrightarrow (1 \in ℤ \land 1 \leq 1)$
18	11 12 17	mpbir2an	$⊢ 1 \in Z$
19		neg1z	$⊢ - 1 \in ℤ$
20		fveq2	$⊢ x = - 1 \to \|x\| = \|- 1\|$
21		ax-1cn	$⊢ 1 \in ℂ$
22	21	absnegi	$⊢ \|- 1\| = \|1\|$
23	22 14	eqtri	$⊢ \|- 1\| = 1$
24	20 23	eqtrdi	$⊢ x = - 1 \to \|x\| = 1$
25	24	breq1d	$⊢ x = - 1 \to (\|x\| \leq 1 \leftrightarrow 1 \leq 1)$
26	25 2	elrab2	$⊢ - 1 \in Z \leftrightarrow (- 1 \in ℤ \land 1 \leq 1)$
27	19 12 26	mpbir2an	$⊢ - 1 \in Z$
28	18 27	ifcli	$⊢ if (A \mod 8 \in \{1, 7\}, 1, - 1) \in Z$
29	10 28	ifcli	$⊢ if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)) \in Z$
30	29	a1i	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \land n = 2) \to if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)) \in Z$
31		simpl1	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \to A \in ℤ$
32	31	ad2antrr	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \land \neg n = 2) \to A \in ℤ$
33		simplr	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \land \neg n = 2) \to n \in ℙ$
34		simpr	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \land \neg n = 2) \to \neg n = 2$
35	34	neqned	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \land \neg n = 2) \to n \neq 2$
36		eldifsn	$⊢ n \in (ℙ ∖ \{2\}) \leftrightarrow (n \in ℙ \land n \neq 2)$
37	33 35 36	sylanbrc	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \land \neg n = 2) \to n \in (ℙ ∖ \{2\})$
38	2	lgslem4	$⊢ (A \in ℤ \land n \in (ℙ ∖ \{2\})) \to ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1 \in Z$
39	32 37 38	syl2anc	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \land \neg n = 2) \to ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1 \in Z$
40	30 39	ifclda	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \to if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1) \in Z$
41		simpr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \to n \in ℙ$
42		simpll2	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \to N \in ℤ$
43		simpll3	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \to N \neq 0$
44		pczcl	$⊢ (n \in ℙ \land (N \in ℤ \land N \neq 0)) \to n pCnt N \in ℕ_{0}$
45	41 42 43 44	syl12anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \to n pCnt N \in ℕ_{0}$
46	2	ssrab3	$⊢ Z \subseteq ℤ$
47		zsscn	$⊢ ℤ \subseteq ℂ$
48	46 47	sstri	$⊢ Z \subseteq ℂ$
49	2	lgslem3	$⊢ (a \in Z \land b \in Z) \to a b \in Z$
50	48 49 18	expcllem	$⊢ (if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1) \in Z \land n pCnt N \in ℕ_{0}) \to {if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1)}^{n pCnt N} \in Z$
51	40 45 50	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land n \in ℙ) \to {if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1)}^{n pCnt N} \in Z$
52	18	a1i	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \land \neg n \in ℙ) \to 1 \in Z$
53	51 52	ifclda	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land n \in ℕ) \to if (n \in ℙ, {if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1)}^{n pCnt N}, 1) \in Z$
54	53 1	fmptd	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to F : ℕ ⟶ Z$

Metamath Proof Explorer

Theorem lgsfcl2

Proof