lgsval2lem

		Ref	Expression
	Hypothesis	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))$
	Assertion	lgsval2lem	$⊢ (A \in ℤ \land N \in ℙ) \to A /_{L} N = 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)$

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		prmz	$⊢ N \in ℙ \to N \in ℤ$
3	1	lgsval	$⊢ (A \in ℤ \land N \in ℤ) \to A /_{L} N = if (N = 0, if (A^{2} = 1, 1, 0), if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|))$
4	2 3	sylan2	$⊢ (A \in ℤ \land N \in ℙ) \to A /_{L} N = if (N = 0, if (A^{2} = 1, 1, 0), if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|))$
5		prmnn	$⊢ N \in ℙ \to N \in ℕ$
6	5	adantl	$⊢ (A \in ℤ \land N \in ℙ) \to N \in ℕ$
7	6	nnne0d	$⊢ (A \in ℤ \land N \in ℙ) \to N \neq 0$
8	7	neneqd	$⊢ (A \in ℤ \land N \in ℙ) \to \neg N = 0$
9	8	iffalsed	$⊢ (A \in ℤ \land N \in ℙ) \to if (N = 0, if (A^{2} = 1, 1, 0), if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|)) = if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|)$
10	6	nnnn0d	$⊢ (A \in ℤ \land N \in ℙ) \to N \in ℕ_{0}$
11	10	nn0ge0d	$⊢ (A \in ℤ \land N \in ℙ) \to 0 \leq N$
12		0re	$⊢ 0 \in ℝ$
13	6	nnred	$⊢ (A \in ℤ \land N \in ℙ) \to N \in ℝ$
14		lenlt	$⊢ (0 \in ℝ \land N \in ℝ) \to (0 \leq N \leftrightarrow \neg N < 0)$
15	12 13 14	sylancr	$⊢ (A \in ℤ \land N \in ℙ) \to (0 \leq N \leftrightarrow \neg N < 0)$
16	11 15	mpbid	$⊢ (A \in ℤ \land N \in ℙ) \to \neg N < 0$
17	16	intnanrd	$⊢ (A \in ℤ \land N \in ℙ) \to \neg (N < 0 \land A < 0)$
18	17	iffalsed	$⊢ (A \in ℤ \land N \in ℙ) \to if ((N < 0 \land A < 0), - 1, 1) = 1$
19	13 11	absidd	$⊢ (A \in ℤ \land N \in ℙ) \to \|N\| = N$
20	19	fveq2d	$⊢ (A \in ℤ \land N \in ℙ) \to seq 1 (\times F) (\|N\|) = seq 1 (\times F) (N)$
21		1z	$⊢ 1 \in ℤ$
22		prmuz2	$⊢ N \in ℙ \to N \in ℤ_{\geq 2}$
23	22	adantl	$⊢ (A \in ℤ \land N \in ℙ) \to N \in ℤ_{\geq 2}$
24		df-2	$⊢ 2 = 1 + 1$
25	24	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
26	23 25	eleqtrdi	$⊢ (A \in ℤ \land N \in ℙ) \to N \in ℤ_{\geq (1 + 1)}$
27		seqm1	$⊢ (1 \in ℤ \land N \in ℤ_{\geq (1 + 1)}) \to seq 1 (\times F) (N) = seq 1 (\times F) (N - 1) F (N)$
28	21 26 27	sylancr	$⊢ (A \in ℤ \land N \in ℙ) \to seq 1 (\times F) (N) = seq 1 (\times F) (N - 1) F (N)$
29		1t1e1	$⊢ 1 \cdot 1 = 1$
30	29	a1i	$⊢ (A \in ℤ \land N \in ℙ) \to 1 \cdot 1 = 1$
31		uz2m1nn	$⊢ N \in ℤ_{\geq 2} \to N - 1 \in ℕ$
32	23 31	syl	$⊢ (A \in ℤ \land N \in ℙ) \to N - 1 \in ℕ$
33		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
34	32 33	eleqtrdi	$⊢ (A \in ℤ \land N \in ℙ) \to N - 1 \in ℤ_{\geq 1}$
35		elfznn	$⊢ x \in (1 \dots N - 1) \to x \in ℕ$
36	35	adantl	$⊢ ((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \to x \in ℕ$
37	1	lgsfval	$⊢ x \in ℕ \to F (x) = if (x \in ℙ, {if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1)}^{x pCnt N}, 1)$
38	36 37	syl	$⊢ ((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \to F (x) = if (x \in ℙ, {if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1)}^{x pCnt N}, 1)$
39		elfzelz	$⊢ N \in (1 \dots N - 1) \to N \in ℤ$
40	39	zred	$⊢ N \in (1 \dots N - 1) \to N \in ℝ$
41	40	ltm1d	$⊢ N \in (1 \dots N - 1) \to N - 1 < N$
42		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
43	40 42	syl	$⊢ N \in (1 \dots N - 1) \to N - 1 \in ℝ$
44		elfzle2	$⊢ N \in (1 \dots N - 1) \to N \leq N - 1$
45	40 43 44	lensymd	$⊢ N \in (1 \dots N - 1) \to \neg N - 1 < N$
46	41 45	pm2.65i	$⊢ \neg N \in (1 \dots N - 1)$
47		eleq1	$⊢ x = N \to (x \in (1 \dots N - 1) \leftrightarrow N \in (1 \dots N - 1))$
48	46 47	mtbiri	$⊢ x = N \to \neg x \in (1 \dots N - 1)$
49	48	con2i	$⊢ x \in (1 \dots N - 1) \to \neg x = N$
50	49	ad2antlr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to \neg x = N$
51		prmuz2	$⊢ x \in ℙ \to x \in ℤ_{\geq 2}$
52		simpllr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to N \in ℙ$
53		dvdsprm	$⊢ (x \in ℤ_{\geq 2} \land N \in ℙ) \to (x ∥ N \leftrightarrow x = N)$
54	51 52 53	syl2an2	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to (x ∥ N \leftrightarrow x = N)$
55	50 54	mtbird	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to \neg x ∥ N$
56		simpr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to x \in ℙ$
57	6	ad2antrr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to N \in ℕ$
58		pceq0	$⊢ (x \in ℙ \land N \in ℕ) \to (x pCnt N = 0 \leftrightarrow \neg x ∥ N)$
59	56 57 58	syl2anc	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to (x pCnt N = 0 \leftrightarrow \neg x ∥ N)$
60	55 59	mpbird	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to x pCnt N = 0$
61	60	oveq2d	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to {if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1)}^{x pCnt N} = {if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1)}^{0}$
62		0z	$⊢ 0 \in ℤ$
63		neg1z	$⊢ - 1 \in ℤ$
64	21 63	ifcli	$⊢ if (A \mod 8 \in \{1, 7\}, 1, - 1) \in ℤ$
65	62 64	ifcli	$⊢ if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)) \in ℤ$
66	65	a1i	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land x = 2) \to if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)) \in ℤ$
67		simpl	$⊢ (A \in ℤ \land N \in ℙ) \to A \in ℤ$
68	67	ad2antrr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to A \in ℤ$
69		simplr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to x \in ℙ$
70		simpr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to \neg x = 2$
71	70	neqned	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to x \neq 2$
72		eldifsn	$⊢ x \in (ℙ ∖ \{2\}) \leftrightarrow (x \in ℙ \land x \neq 2)$
73	69 71 72	sylanbrc	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to x \in (ℙ ∖ \{2\})$
74		oddprm	$⊢ x \in (ℙ ∖ \{2\}) \to \frac{x - 1}{2} \in ℕ$
75	73 74	syl	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to \frac{x - 1}{2} \in ℕ$
76	75	nnnn0d	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to \frac{x - 1}{2} \in ℕ_{0}$
77		zexpcl	$⊢ (A \in ℤ \land \frac{x - 1}{2} \in ℕ_{0}) \to A^{\frac{x - 1}{2}} \in ℤ$
78	68 76 77	syl2anc	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to A^{\frac{x - 1}{2}} \in ℤ$
79	78	peano2zd	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to A^{\frac{x - 1}{2}} + 1 \in ℤ$
80		prmnn	$⊢ x \in ℙ \to x \in ℕ$
81	80	ad2antlr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to x \in ℕ$
82	79 81	zmodcld	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to (A^{\frac{x - 1}{2}} + 1) \mod x \in ℕ_{0}$
83	82	nn0zd	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to (A^{\frac{x - 1}{2}} + 1) \mod x \in ℤ$
84		peano2zm	$⊢ (A^{\frac{x - 1}{2}} + 1) \mod x \in ℤ \to ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1 \in ℤ$
85	83 84	syl	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in ℙ) \land \neg x = 2) \to ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1 \in ℤ$
86	66 85	ifclda	$⊢ ((A \in ℤ \land N \in ℙ) \land x \in ℙ) \to if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1) \in ℤ$
87	86	zcnd	$⊢ ((A \in ℤ \land N \in ℙ) \land x \in ℙ) \to if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1) \in ℂ$
88	87	adantlr	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1) \in ℂ$
89	88	exp0d	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to {if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1)}^{0} = 1$
90	61 89	eqtrd	$⊢ (((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \land x \in ℙ) \to {if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1)}^{x pCnt N} = 1$
91	90	ifeq1da	$⊢ ((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \to if (x \in ℙ, {if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1)}^{x pCnt N}, 1) = if (x \in ℙ, 1, 1)$
92		ifid	$⊢ if (x \in ℙ, 1, 1) = 1$
93	91 92	eqtrdi	$⊢ ((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \to if (x \in ℙ, {if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1)}^{x pCnt N}, 1) = 1$
94	38 93	eqtrd	$⊢ ((A \in ℤ \land N \in ℙ) \land x \in (1 \dots N - 1)) \to F (x) = 1$
95	30 34 94	seqid3	$⊢ (A \in ℤ \land N \in ℙ) \to seq 1 (\times F) (N - 1) = 1$
96	95	oveq1d	$⊢ (A \in ℤ \land N \in ℙ) \to seq 1 (\times F) (N - 1) F (N) = 1 F (N)$
97	2	adantl	$⊢ (A \in ℤ \land N \in ℙ) \to N \in ℤ$
98	1	lgsfcl	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to F : ℕ ⟶ ℤ$
99	67 97 7 98	syl3anc	$⊢ (A \in ℤ \land N \in ℙ) \to F : ℕ ⟶ ℤ$
100	99 6	ffvelcdmd	$⊢ (A \in ℤ \land N \in ℙ) \to F (N) \in ℤ$
101	100	zcnd	$⊢ (A \in ℤ \land N \in ℙ) \to F (N) \in ℂ$
102	101	mullidd	$⊢ (A \in ℤ \land N \in ℙ) \to 1 F (N) = F (N)$
103	28 96 102	3eqtrd	$⊢ (A \in ℤ \land N \in ℙ) \to seq 1 (\times F) (N) = F (N)$
104	20 103	eqtrd	$⊢ (A \in ℤ \land N \in ℙ) \to seq 1 (\times F) (\|N\|) = F (N)$
105	18 104	oveq12d	$⊢ (A \in ℤ \land N \in ℙ) \to if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|) = 1 F (N)$
106	1	lgsfval	$⊢ N \in ℕ \to F (N) = 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)$
107	6 106	syl	$⊢ (A \in ℤ \land N \in ℙ) \to F (N) = 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)$
108		iftrue	$⊢ 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) = {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}$
109	108	adantl	$⊢ (A \in ℤ \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) = {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}$
110	6	nncnd	$⊢ (A \in ℤ \land N \in ℙ) \to N \in ℂ$
111	110	exp1d	$⊢ (A \in ℤ \land N \in ℙ) \to N^{1} = N$
112	111	oveq2d	$⊢ (A \in ℤ \land N \in ℙ) \to N pCnt N^{1} = N pCnt N$
113		simpr	$⊢ (A \in ℤ \land N \in ℙ) \to N \in ℙ$
114		pcid	$⊢ (N \in ℙ \land 1 \in ℤ) \to N pCnt N^{1} = 1$
115	113 21 114	sylancl	$⊢ (A \in ℤ \land N \in ℙ) \to N pCnt N^{1} = 1$
116	112 115	eqtr3d	$⊢ (A \in ℤ \land N \in ℙ) \to N pCnt N = 1$
117	116	oveq2d	$⊢ (A \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} = {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)}^{1}$
118		eqeq1	$⊢ x = N \to (x = 2 \leftrightarrow N = 2)$
119		oveq1	$⊢ x = N \to x - 1 = N - 1$
120	119	oveq1d	$⊢ x = N \to \frac{x - 1}{2} = \frac{N - 1}{2}$
121	120	oveq2d	$⊢ x = N \to A^{\frac{x - 1}{2}} = A^{\frac{N - 1}{2}}$
122	121	oveq1d	$⊢ x = N \to A^{\frac{x - 1}{2}} + 1 = A^{\frac{N - 1}{2}} + 1$
123		id	$⊢ x = N \to x = N$
124	122 123	oveq12d	$⊢ x = N \to (A^{\frac{x - 1}{2}} + 1) \mod x = (A^{\frac{N - 1}{2}} + 1) \mod N$
125	124	oveq1d	$⊢ x = N \to ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1 = ((A^{\frac{N - 1}{2}} + 1) \mod N) - 1$
126	118 125	ifbieq2d	$⊢ x = N \to if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1) = 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)$
127	126	eleq1d	$⊢ x = N \to (if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1) \in ℂ \leftrightarrow 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 ℂ)$
128	87	ralrimiva	$⊢ (A \in ℤ \land N \in ℙ) \to \forall x \in ℙ if (x = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{x - 1}{2}} + 1) \mod x) - 1) \in ℂ$
129	127 128 113	rspcdva	$⊢ (A \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 ℂ$
130	129	exp1d	$⊢ (A \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)}^{1} = 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)$
131	117 130	eqtrd	$⊢ (A \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} = 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)$
132	107 109 131	3eqtrd	$⊢ (A \in ℤ \land N \in ℙ) \to F (N) = 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)$
133	105 102 132	3eqtrd	$⊢ (A \in ℤ \land N \in ℙ) \to if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|) = 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)$
134	4 9 133	3eqtrd	$⊢ (A \in ℤ \land N \in ℙ) \to A /_{L} N = 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)$

Metamath Proof Explorer

Theorem lgsval2lem

Proof