lgsne0

Description: The Legendre symbol is nonzero (and hence equal to 1 or -u 1 ) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015)

		Ref	Expression
	Assertion	lgsne0	$⊢ (A \in ℤ \land N \in ℤ) \to (A /_{L} N \neq 0 \leftrightarrow A \gcd N = 1)$

Proof

Step	Hyp	Ref	Expression
1		iffalse	$⊢ \neg A^{2} = 1 \to if (A^{2} = 1, 1, 0) = 0$
2	1	necon1ai	$⊢ if (A^{2} = 1, 1, 0) \neq 0 \to A^{2} = 1$
3		iftrue	$⊢ A^{2} = 1 \to if (A^{2} = 1, 1, 0) = 1$
4		ax-1ne0	$⊢ 1 \neq 0$
5	4	a1i	$⊢ A^{2} = 1 \to 1 \neq 0$
6	3 5	eqnetrd	$⊢ A^{2} = 1 \to if (A^{2} = 1, 1, 0) \neq 0$
7	2 6	impbii	$⊢ if (A^{2} = 1, 1, 0) \neq 0 \leftrightarrow A^{2} = 1$
8		zre	$⊢ A \in ℤ \to A \in ℝ$
9	8	ad2antrr	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to A \in ℝ$
10		absresq	$⊢ A \in ℝ \to {\|A\|}^{2} = A^{2}$
11	9 10	syl	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to {\|A\|}^{2} = A^{2}$
12		sq1	$⊢ 1^{2} = 1$
13	12	a1i	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to 1^{2} = 1$
14	11 13	eqeq12d	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to ({\|A\|}^{2} = 1^{2} \leftrightarrow A^{2} = 1)$
15	9	recnd	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to A \in ℂ$
16	15	abscld	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to \|A\| \in ℝ$
17	15	absge0d	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to 0 \leq \|A\|$
18		1re	$⊢ 1 \in ℝ$
19		0le1	$⊢ 0 \leq 1$
20		sq11	$⊢ ((\|A\| \in ℝ \land 0 \leq \|A\|) \land (1 \in ℝ \land 0 \leq 1)) \to ({\|A\|}^{2} = 1^{2} \leftrightarrow \|A\| = 1)$
21	18 19 20	mpanr12	$⊢ (\|A\| \in ℝ \land 0 \leq \|A\|) \to ({\|A\|}^{2} = 1^{2} \leftrightarrow \|A\| = 1)$
22	16 17 21	syl2anc	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to ({\|A\|}^{2} = 1^{2} \leftrightarrow \|A\| = 1)$
23	14 22	bitr3d	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to (A^{2} = 1 \leftrightarrow \|A\| = 1)$
24	7 23	syl5bb	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to (if (A^{2} = 1, 1, 0) \neq 0 \leftrightarrow \|A\| = 1)$
25		oveq2	$⊢ N = 0 \to A /_{L} N = A /_{L} 0$
26		lgs0	$⊢ A \in ℤ \to A /_{L} 0 = if (A^{2} = 1, 1, 0)$
27	26	adantr	$⊢ (A \in ℤ \land N \in ℤ) \to A /_{L} 0 = if (A^{2} = 1, 1, 0)$
28	25 27	sylan9eqr	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to A /_{L} N = if (A^{2} = 1, 1, 0)$
29	28	neeq1d	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to (A /_{L} N \neq 0 \leftrightarrow if (A^{2} = 1, 1, 0) \neq 0)$
30		oveq2	$⊢ N = 0 \to A \gcd N = A \gcd 0$
31		gcdid0	$⊢ A \in ℤ \to A \gcd 0 = \|A\|$
32	31	adantr	$⊢ (A \in ℤ \land N \in ℤ) \to A \gcd 0 = \|A\|$
33	30 32	sylan9eqr	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to A \gcd N = \|A\|$
34	33	eqeq1d	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to (A \gcd N = 1 \leftrightarrow \|A\| = 1)$
35	24 29 34	3bitr4d	$⊢ ((A \in ℤ \land N \in ℤ) \land N = 0) \to (A /_{L} N \neq 0 \leftrightarrow A \gcd N = 1)$
36		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))$
37	36	lgsval4	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A /_{L} N = if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
38	37	neeq1d	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (A /_{L} N \neq 0 \leftrightarrow if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0)$
39		neeq1	$⊢ - 1 = if ((N < 0 \land A < 0), - 1, 1) \to (- 1 \neq 0 \leftrightarrow if ((N < 0 \land A < 0), - 1, 1) \neq 0)$
40		neeq1	$⊢ 1 = if ((N < 0 \land A < 0), - 1, 1) \to (1 \neq 0 \leftrightarrow if ((N < 0 \land A < 0), - 1, 1) \neq 0)$
41		neg1ne0	$⊢ - 1 \neq 0$
42	39 40 41 4	keephyp	$⊢ if ((N < 0 \land A < 0), - 1, 1) \neq 0$
43	42	biantrur	$⊢ seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0 \leftrightarrow (if ((N < 0 \land A < 0), - 1, 1) \neq 0 \land seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0)$
44		neg1cn	$⊢ - 1 \in ℂ$
45		ax-1cn	$⊢ 1 \in ℂ$
46	44 45	ifcli	$⊢ if ((N < 0 \land A < 0), - 1, 1) \in ℂ$
47	46	a1i	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to if ((N < 0 \land A < 0), - 1, 1) \in ℂ$
48		nnabscl	$⊢ (N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
49	48	3adant1	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
50		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
51	49 50	eleqtrdi	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to \|N\| \in ℤ_{\geq 1}$
52	36	lgsfcl3	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ$
53		elfznn	$⊢ k \in (1 \dots \|N\|) \to k \in ℕ$
54		ffvelrn	$⊢ ((n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ \land k \in ℕ) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℤ$
55	52 53 54	syl2an	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℤ$
56	55	zcnd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℂ$
57		mulcl	$⊢ (k \in ℂ \land x \in ℂ) \to k x \in ℂ$
58	57	adantl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
59	51 56 58	seqcl	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in ℂ$
60	47 59	mulne0bd	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to ((if ((N < 0 \land A < 0), - 1, 1) \neq 0 \land seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0) \leftrightarrow if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0)$
61	43 60	bitr2id	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0 \leftrightarrow seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0)$
62		gcd2n0cl	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A \gcd N \in ℕ$
63		eluz2b3	$⊢ A \gcd N \in ℤ_{\geq 2} \leftrightarrow (A \gcd N \in ℕ \land A \gcd N \neq 1)$
64		exprmfct	$⊢ A \gcd N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ (A \gcd N)$
65	63 64	sylbir	$⊢ (A \gcd N \in ℕ \land A \gcd N \neq 1) \to \exists p \in ℙ p ∥ (A \gcd N)$
66	57	adantl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
67	56	adantlr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℂ$
68		mul02	$⊢ k \in ℂ \to 0 \cdot k = 0$
69	68	adantl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land k \in ℂ) \to 0 \cdot k = 0$
70		mul01	$⊢ k \in ℂ \to k \cdot 0 = 0$
71	70	adantl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land k \in ℂ) \to k \cdot 0 = 0$
72		simprr	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p ∥ (A \gcd N)$
73		prmz	$⊢ p \in ℙ \to p \in ℤ$
74	73	ad2antrl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p \in ℤ$
75		simpl1	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to A \in ℤ$
76		simpl2	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to N \in ℤ$
77		dvdsgcdb	$⊢ (p \in ℤ \land A \in ℤ \land N \in ℤ) \to ((p ∥ A \land p ∥ N) \leftrightarrow p ∥ (A \gcd N))$
78	74 75 76 77	syl3anc	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to ((p ∥ A \land p ∥ N) \leftrightarrow p ∥ (A \gcd N))$
79	72 78	mpbird	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to (p ∥ A \land p ∥ N)$
80	79	simprd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p ∥ N$
81		dvdsabsb	$⊢ (p \in ℤ \land N \in ℤ) \to (p ∥ N \leftrightarrow p ∥ \|N\|)$
82	74 76 81	syl2anc	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to (p ∥ N \leftrightarrow p ∥ \|N\|)$
83	80 82	mpbid	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p ∥ \|N\|$
84	49	adantr	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to \|N\| \in ℕ$
85		dvdsle	$⊢ (p \in ℤ \land \|N\| \in ℕ) \to (p ∥ \|N\| \to p \leq \|N\|)$
86	74 84 85	syl2anc	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to (p ∥ \|N\| \to p \leq \|N\|)$
87	83 86	mpd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p \leq \|N\|$
88		prmnn	$⊢ p \in ℙ \to p \in ℕ$
89	88	ad2antrl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p \in ℕ$
90	89 50	eleqtrdi	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p \in ℤ_{\geq 1}$
91	84	nnzd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to \|N\| \in ℤ$
92		elfz5	$⊢ (p \in ℤ_{\geq 1} \land \|N\| \in ℤ) \to (p \in (1 \dots \|N\|) \leftrightarrow p \leq \|N\|)$
93	90 91 92	syl2anc	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to (p \in (1 \dots \|N\|) \leftrightarrow p \leq \|N\|)$
94	87 93	mpbird	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p \in (1 \dots \|N\|)$
95		eleq1w	$⊢ n = p \to (n \in ℙ \leftrightarrow p \in ℙ)$
96		oveq2	$⊢ n = p \to A /_{L} n = A /_{L} p$
97		oveq1	$⊢ n = p \to n pCnt N = p pCnt N$
98	96 97	oveq12d	$⊢ n = p \to {(A /_{L} n)}^{n pCnt N} = {(A /_{L} p)}^{p pCnt N}$
99	95 98	ifbieq1d	$⊢ n = p \to if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1) = if (p \in ℙ, {(A /_{L} p)}^{p pCnt N}, 1)$
100		ovex	$⊢ {(A /_{L} p)}^{p pCnt N} \in V$
101		1ex	$⊢ 1 \in V$
102	100 101	ifex	$⊢ if (p \in ℙ, {(A /_{L} p)}^{p pCnt N}, 1) \in V$
103	99 36 102	fvmpt	$⊢ p \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (p) = if (p \in ℙ, {(A /_{L} p)}^{p pCnt N}, 1)$
104	89 103	syl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (p) = if (p \in ℙ, {(A /_{L} p)}^{p pCnt N}, 1)$
105		iftrue	$⊢ p \in ℙ \to if (p \in ℙ, {(A /_{L} p)}^{p pCnt N}, 1) = {(A /_{L} p)}^{p pCnt N}$
106	105	ad2antrl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to if (p \in ℙ, {(A /_{L} p)}^{p pCnt N}, 1) = {(A /_{L} p)}^{p pCnt N}$
107		oveq2	$⊢ p = 2 \to A /_{L} p = A /_{L} 2$
108		lgs2	$⊢ A \in ℤ \to A /_{L} 2 = if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1))$
109	75 108	syl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to A /_{L} 2 = if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1))$
110	107 109	sylan9eqr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p = 2) \to A /_{L} p = if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1))$
111		simpr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p = 2) \to p = 2$
112	79	simpld	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p ∥ A$
113	112	adantr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p = 2) \to p ∥ A$
114	111 113	eqbrtrrd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p = 2) \to 2 ∥ A$
115	114	iftrued	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p = 2) \to if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)) = 0$
116	110 115	eqtrd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p = 2) \to A /_{L} p = 0$
117		simpll1	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A \in ℤ$
118		simprl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p \in ℙ$
119	118	adantr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to p \in ℙ$
120		simpr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to p \neq 2$
121		eldifsn	$⊢ p \in (ℙ ∖ \{2\}) \leftrightarrow (p \in ℙ \land p \neq 2)$
122	119 120 121	sylanbrc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to p \in (ℙ ∖ \{2\})$
123		lgsval3	$⊢ (A \in ℤ \land p \in (ℙ ∖ \{2\})) \to A /_{L} p = ((A^{\frac{p - 1}{2}} + 1) \mod p) - 1$
124	117 122 123	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A /_{L} p = ((A^{\frac{p - 1}{2}} + 1) \mod p) - 1$
125		oddprm	$⊢ p \in (ℙ ∖ \{2\}) \to \frac{p - 1}{2} \in ℕ$
126	122 125	syl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to \frac{p - 1}{2} \in ℕ$
127	126	nnnn0d	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to \frac{p - 1}{2} \in ℕ_{0}$
128		zexpcl	$⊢ (A \in ℤ \land \frac{p - 1}{2} \in ℕ_{0}) \to A^{\frac{p - 1}{2}} \in ℤ$
129	117 127 128	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A^{\frac{p - 1}{2}} \in ℤ$
130	129	zred	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A^{\frac{p - 1}{2}} \in ℝ$
131		0red	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to 0 \in ℝ$
132	18	a1i	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to 1 \in ℝ$
133	119 88	syl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to p \in ℕ$
134	133	nnrpd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to p \in ℝ^{+}$
135		0zd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to 0 \in ℤ$
136	112	adantr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to p ∥ A$
137		dvdsval3	$⊢ (p \in ℕ \land A \in ℤ) \to (p ∥ A \leftrightarrow A \mod p = 0)$
138	133 117 137	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to (p ∥ A \leftrightarrow A \mod p = 0)$
139	136 138	mpbid	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A \mod p = 0$
140		0mod	$⊢ p \in ℝ^{+} \to 0 \mod p = 0$
141	134 140	syl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to 0 \mod p = 0$
142	139 141	eqtr4d	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A \mod p = 0 \mod p$
143		modexp	$⊢ ((A \in ℤ \land 0 \in ℤ) \land (\frac{p - 1}{2} \in ℕ_{0} \land p \in ℝ^{+}) \land A \mod p = 0 \mod p) \to A^{\frac{p - 1}{2}} \mod p = 0^{\frac{p - 1}{2}} \mod p$
144	117 135 127 134 142 143	syl221anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A^{\frac{p - 1}{2}} \mod p = 0^{\frac{p - 1}{2}} \mod p$
145	126	0expd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to 0^{\frac{p - 1}{2}} = 0$
146	145	oveq1d	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to 0^{\frac{p - 1}{2}} \mod p = 0 \mod p$
147	144 146	eqtrd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A^{\frac{p - 1}{2}} \mod p = 0 \mod p$
148		modadd1	$⊢ ((A^{\frac{p - 1}{2}} \in ℝ \land 0 \in ℝ) \land (1 \in ℝ \land p \in ℝ^{+}) \land A^{\frac{p - 1}{2}} \mod p = 0 \mod p) \to (A^{\frac{p - 1}{2}} + 1) \mod p = (0 + 1) \mod p$
149	130 131 132 134 147 148	syl221anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to (A^{\frac{p - 1}{2}} + 1) \mod p = (0 + 1) \mod p$
150		0p1e1	$⊢ 0 + 1 = 1$
151	150	oveq1i	$⊢ (0 + 1) \mod p = 1 \mod p$
152	149 151	eqtrdi	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to (A^{\frac{p - 1}{2}} + 1) \mod p = 1 \mod p$
153	133	nnred	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to p \in ℝ$
154		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
155	119 154	syl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to p \in ℤ_{\geq 2}$
156		eluz2b2	$⊢ p \in ℤ_{\geq 2} \leftrightarrow (p \in ℕ \land 1 < p)$
157	155 156	sylib	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to (p \in ℕ \land 1 < p)$
158	157	simprd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to 1 < p$
159		1mod	$⊢ (p \in ℝ \land 1 < p) \to 1 \mod p = 1$
160	153 158 159	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to 1 \mod p = 1$
161	152 160	eqtrd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to (A^{\frac{p - 1}{2}} + 1) \mod p = 1$
162	161	oveq1d	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to ((A^{\frac{p - 1}{2}} + 1) \mod p) - 1 = 1 - 1$
163		1m1e0	$⊢ 1 - 1 = 0$
164	162 163	eqtrdi	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to ((A^{\frac{p - 1}{2}} + 1) \mod p) - 1 = 0$
165	124 164	eqtrd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \land p \neq 2) \to A /_{L} p = 0$
166	116 165	pm2.61dane	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to A /_{L} p = 0$
167	166	oveq1d	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to {(A /_{L} p)}^{p pCnt N} = 0^{p pCnt N}$
168		zq	$⊢ N \in ℤ \to N \in ℚ$
169	76 168	syl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to N \in ℚ$
170		pcabs	$⊢ (p \in ℙ \land N \in ℚ) \to p pCnt \|N\| = p pCnt N$
171	118 169 170	syl2anc	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p pCnt \|N\| = p pCnt N$
172		pcelnn	$⊢ (p \in ℙ \land \|N\| \in ℕ) \to (p pCnt \|N\| \in ℕ \leftrightarrow p ∥ \|N\|)$
173	118 84 172	syl2anc	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to (p pCnt \|N\| \in ℕ \leftrightarrow p ∥ \|N\|)$
174	83 173	mpbird	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p pCnt \|N\| \in ℕ$
175	171 174	eqeltrrd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to p pCnt N \in ℕ$
176	175	0expd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to 0^{p pCnt N} = 0$
177	167 176	eqtrd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to {(A /_{L} p)}^{p pCnt N} = 0$
178	104 106 177	3eqtrd	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (p) = 0$
179	66 67 69 71 94 84 178	seqz	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land (p \in ℙ \land p ∥ (A \gcd N))) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = 0$
180	179	rexlimdvaa	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (\exists p \in ℙ p ∥ (A \gcd N) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = 0)$
181	65 180	syl5	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to ((A \gcd N \in ℕ \land A \gcd N \neq 1) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = 0)$
182	62 181	mpand	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (A \gcd N \neq 1 \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = 0)$
183	182	necon1d	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0 \to A \gcd N = 1)$
184	51	adantr	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \to \|N\| \in ℤ_{\geq 1}$
185	53	adantl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in (1 \dots \|N\|)) \to k \in ℕ$
186		eleq1w	$⊢ n = k \to (n \in ℙ \leftrightarrow k \in ℙ)$
187		oveq2	$⊢ n = k \to A /_{L} n = A /_{L} k$
188		oveq1	$⊢ n = k \to n pCnt N = k pCnt N$
189	187 188	oveq12d	$⊢ n = k \to {(A /_{L} n)}^{n pCnt N} = {(A /_{L} k)}^{k pCnt N}$
190	186 189	ifbieq1d	$⊢ n = k \to if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
191		ovex	$⊢ {(A /_{L} k)}^{k pCnt N} \in V$
192	191 101	ifex	$⊢ if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) \in V$
193	190 36 192	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
194	185 193	syl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
195		simpll1	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to A \in ℤ$
196		prmz	$⊢ k \in ℙ \to k \in ℤ$
197	196	adantl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to k \in ℤ$
198		lgscl	$⊢ (A \in ℤ \land k \in ℤ) \to A /_{L} k \in ℤ$
199	195 197 198	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to A /_{L} k \in ℤ$
200	199	zcnd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to A /_{L} k \in ℂ$
201	200	adantr	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \to A /_{L} k \in ℂ$
202		oveq2	$⊢ k = 2 \to A /_{L} k = A /_{L} 2$
203	195	adantr	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \to A \in ℤ$
204	203 108	syl	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \to A /_{L} 2 = if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1))$
205	202 204	sylan9eqr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k = 2) \to A /_{L} k = if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1))$
206		nprmdvds1	$⊢ k \in ℙ \to \neg k ∥ 1$
207	206	adantl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to \neg k ∥ 1$
208		simpll2	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to N \in ℤ$
209		dvdsgcdb	$⊢ (k \in ℤ \land A \in ℤ \land N \in ℤ) \to ((k ∥ A \land k ∥ N) \leftrightarrow k ∥ (A \gcd N))$
210	197 195 208 209	syl3anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to ((k ∥ A \land k ∥ N) \leftrightarrow k ∥ (A \gcd N))$
211		simplr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to A \gcd N = 1$
212	211	breq2d	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to (k ∥ (A \gcd N) \leftrightarrow k ∥ 1)$
213	210 212	bitrd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to ((k ∥ A \land k ∥ N) \leftrightarrow k ∥ 1)$
214	207 213	mtbird	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to \neg (k ∥ A \land k ∥ N)$
215		imnan	$⊢ (k ∥ A \to \neg k ∥ N) \leftrightarrow \neg (k ∥ A \land k ∥ N)$
216	214 215	sylibr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to (k ∥ A \to \neg k ∥ N)$
217	216	con2d	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to (k ∥ N \to \neg k ∥ A)$
218	217	imp	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \to \neg k ∥ A$
219		breq1	$⊢ k = 2 \to (k ∥ A \leftrightarrow 2 ∥ A)$
220	219	notbid	$⊢ k = 2 \to (\neg k ∥ A \leftrightarrow \neg 2 ∥ A)$
221	218 220	syl5ibcom	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \to (k = 2 \to \neg 2 ∥ A)$
222	221	imp	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k = 2) \to \neg 2 ∥ A$
223	222	iffalsed	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k = 2) \to if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)) = if (A \mod 8 \in \{1, 7\}, 1, - 1)$
224	205 223	eqtrd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k = 2) \to A /_{L} k = if (A \mod 8 \in \{1, 7\}, 1, - 1)$
225		neeq1	$⊢ 1 = if (A \mod 8 \in \{1, 7\}, 1, - 1) \to (1 \neq 0 \leftrightarrow if (A \mod 8 \in \{1, 7\}, 1, - 1) \neq 0)$
226		neeq1	$⊢ - 1 = if (A \mod 8 \in \{1, 7\}, 1, - 1) \to (- 1 \neq 0 \leftrightarrow if (A \mod 8 \in \{1, 7\}, 1, - 1) \neq 0)$
227	225 226 4 41	keephyp	$⊢ if (A \mod 8 \in \{1, 7\}, 1, - 1) \neq 0$
228	227	a1i	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k = 2) \to if (A \mod 8 \in \{1, 7\}, 1, - 1) \neq 0$
229	224 228	eqnetrd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k = 2) \to A /_{L} k \neq 0$
230		simpr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to k \in ℙ$
231	230	ad2antrr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to k \in ℙ$
232	231 206	syl	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \neg k ∥ 1$
233		simplr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to k ∥ N$
234	231 196	syl	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to k \in ℤ$
235	203	adantr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to A \in ℤ$
236		simpr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to k \neq 2$
237		eldifsn	$⊢ k \in (ℙ ∖ \{2\}) \leftrightarrow (k \in ℙ \land k \neq 2)$
238	231 236 237	sylanbrc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to k \in (ℙ ∖ \{2\})$
239		oddprm	$⊢ k \in (ℙ ∖ \{2\}) \to \frac{k - 1}{2} \in ℕ$
240	238 239	syl	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \frac{k - 1}{2} \in ℕ$
241	240	nnnn0d	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \frac{k - 1}{2} \in ℕ_{0}$
242		zexpcl	$⊢ (A \in ℤ \land \frac{k - 1}{2} \in ℕ_{0}) \to A^{\frac{k - 1}{2}} \in ℤ$
243	235 241 242	syl2anc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to A^{\frac{k - 1}{2}} \in ℤ$
244	208	ad2antrr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to N \in ℤ$
245		dvdsgcd	$⊢ (k \in ℤ \land A^{\frac{k - 1}{2}} \in ℤ \land N \in ℤ) \to ((k ∥ A^{\frac{k - 1}{2}} \land k ∥ N) \to k ∥ (A^{\frac{k - 1}{2}} \gcd N))$
246	234 243 244 245	syl3anc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to ((k ∥ A^{\frac{k - 1}{2}} \land k ∥ N) \to k ∥ (A^{\frac{k - 1}{2}} \gcd N))$
247	233 246	mpan2d	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (k ∥ A^{\frac{k - 1}{2}} \to k ∥ (A^{\frac{k - 1}{2}} \gcd N))$
248	235	zcnd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to A \in ℂ$
249	248 241	absexpd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \|A^{\frac{k - 1}{2}}\| = {\|A\|}^{\frac{k - 1}{2}}$
250	249	oveq1d	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \|A^{\frac{k - 1}{2}}\| \gcd \|N\| = {\|A\|}^{\frac{k - 1}{2}} \gcd \|N\|$
251		gcdabs	$⊢ (A^{\frac{k - 1}{2}} \in ℤ \land N \in ℤ) \to \|A^{\frac{k - 1}{2}}\| \gcd \|N\| = A^{\frac{k - 1}{2}} \gcd N$
252	243 244 251	syl2anc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \|A^{\frac{k - 1}{2}}\| \gcd \|N\| = A^{\frac{k - 1}{2}} \gcd N$
253		gcdabs	$⊢ (A \in ℤ \land N \in ℤ) \to \|A\| \gcd \|N\| = A \gcd N$
254	235 244 253	syl2anc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \|A\| \gcd \|N\| = A \gcd N$
255	211	ad2antrr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to A \gcd N = 1$
256	254 255	eqtrd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \|A\| \gcd \|N\| = 1$
257	218	adantr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \neg k ∥ A$
258		dvds0	$⊢ k \in ℤ \to k ∥ 0$
259	234 258	syl	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to k ∥ 0$
260		breq2	$⊢ A = 0 \to (k ∥ A \leftrightarrow k ∥ 0)$
261	259 260	syl5ibrcom	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (A = 0 \to k ∥ A)$
262	261	necon3bd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (\neg k ∥ A \to A \neq 0)$
263	257 262	mpd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to A \neq 0$
264		nnabscl	$⊢ (A \in ℤ \land A \neq 0) \to \|A\| \in ℕ$
265	235 263 264	syl2anc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \|A\| \in ℕ$
266		simpll3	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to N \neq 0$
267	208 266 48	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to \|N\| \in ℕ$
268	267	ad2antrr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \|N\| \in ℕ$
269		rplpwr	$⊢ (\|A\| \in ℕ \land \|N\| \in ℕ \land \frac{k - 1}{2} \in ℕ) \to (\|A\| \gcd \|N\| = 1 \to {\|A\|}^{\frac{k - 1}{2}} \gcd \|N\| = 1)$
270	265 268 240 269	syl3anc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (\|A\| \gcd \|N\| = 1 \to {\|A\|}^{\frac{k - 1}{2}} \gcd \|N\| = 1)$
271	256 270	mpd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to {\|A\|}^{\frac{k - 1}{2}} \gcd \|N\| = 1$
272	250 252 271	3eqtr3d	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to A^{\frac{k - 1}{2}} \gcd N = 1$
273	272	breq2d	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (k ∥ (A^{\frac{k - 1}{2}} \gcd N) \leftrightarrow k ∥ 1)$
274	247 273	sylibd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (k ∥ A^{\frac{k - 1}{2}} \to k ∥ 1)$
275	232 274	mtod	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to \neg k ∥ A^{\frac{k - 1}{2}}$
276		prmnn	$⊢ k \in ℙ \to k \in ℕ$
277	276	adantl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to k \in ℕ$
278	277	ad2antrr	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to k \in ℕ$
279		dvdsval3	$⊢ (k \in ℕ \land A^{\frac{k - 1}{2}} \in ℤ) \to (k ∥ A^{\frac{k - 1}{2}} \leftrightarrow A^{\frac{k - 1}{2}} \mod k = 0)$
280	278 243 279	syl2anc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (k ∥ A^{\frac{k - 1}{2}} \leftrightarrow A^{\frac{k - 1}{2}} \mod k = 0)$
281	280	necon3bbid	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (\neg k ∥ A^{\frac{k - 1}{2}} \leftrightarrow A^{\frac{k - 1}{2}} \mod k \neq 0)$
282	275 281	mpbid	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to A^{\frac{k - 1}{2}} \mod k \neq 0$
283		lgsvalmod	$⊢ (A \in ℤ \land k \in (ℙ ∖ \{2\})) \to (A /_{L} k) \mod k = A^{\frac{k - 1}{2}} \mod k$
284	235 238 283	syl2anc	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (A /_{L} k) \mod k = A^{\frac{k - 1}{2}} \mod k$
285	278	nnrpd	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to k \in ℝ^{+}$
286		0mod	$⊢ k \in ℝ^{+} \to 0 \mod k = 0$
287	285 286	syl	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to 0 \mod k = 0$
288	282 284 287	3netr4d	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to (A /_{L} k) \mod k \neq 0 \mod k$
289		oveq1	$⊢ A /_{L} k = 0 \to (A /_{L} k) \mod k = 0 \mod k$
290	289	necon3i	$⊢ (A /_{L} k) \mod k \neq 0 \mod k \to A /_{L} k \neq 0$
291	288 290	syl	$⊢ (((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \land k \neq 2) \to A /_{L} k \neq 0$
292	229 291	pm2.61dane	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \to A /_{L} k \neq 0$
293		pczcl	$⊢ (k \in ℙ \land (N \in ℤ \land N \neq 0)) \to k pCnt N \in ℕ_{0}$
294	230 208 266 293	syl12anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to k pCnt N \in ℕ_{0}$
295	294	nn0zd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to k pCnt N \in ℤ$
296	295	adantr	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \to k pCnt N \in ℤ$
297		neeq1	$⊢ x = {(A /_{L} k)}^{k pCnt N} \to (x \neq 0 \leftrightarrow {(A /_{L} k)}^{k pCnt N} \neq 0)$
298		expclz	$⊢ (A /_{L} k \in ℂ \land A /_{L} k \neq 0 \land k pCnt N \in ℤ) \to {(A /_{L} k)}^{k pCnt N} \in ℂ$
299		expne0i	$⊢ (A /_{L} k \in ℂ \land A /_{L} k \neq 0 \land k pCnt N \in ℤ) \to {(A /_{L} k)}^{k pCnt N} \neq 0$
300	297 298 299	elrabd	$⊢ (A /_{L} k \in ℂ \land A /_{L} k \neq 0 \land k pCnt N \in ℤ) \to {(A /_{L} k)}^{k pCnt N} \in \{x \in ℂ \| x \neq 0\}$
301	201 292 296 300	syl3anc	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land k ∥ N) \to {(A /_{L} k)}^{k pCnt N} \in \{x \in ℂ \| x \neq 0\}$
302		dvdsabsb	$⊢ (k \in ℤ \land N \in ℤ) \to (k ∥ N \leftrightarrow k ∥ \|N\|)$
303	197 208 302	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to (k ∥ N \leftrightarrow k ∥ \|N\|)$
304	303	notbid	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to (\neg k ∥ N \leftrightarrow \neg k ∥ \|N\|)$
305		pceq0	$⊢ (k \in ℙ \land \|N\| \in ℕ) \to (k pCnt \|N\| = 0 \leftrightarrow \neg k ∥ \|N\|)$
306	230 267 305	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to (k pCnt \|N\| = 0 \leftrightarrow \neg k ∥ \|N\|)$
307	208 168	syl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to N \in ℚ$
308		pcabs	$⊢ (k \in ℙ \land N \in ℚ) \to k pCnt \|N\| = k pCnt N$
309	230 307 308	syl2anc	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to k pCnt \|N\| = k pCnt N$
310	309	eqeq1d	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to (k pCnt \|N\| = 0 \leftrightarrow k pCnt N = 0)$
311	304 306 310	3bitr2rd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to (k pCnt N = 0 \leftrightarrow \neg k ∥ N)$
312	311	biimpar	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land \neg k ∥ N) \to k pCnt N = 0$
313	312	oveq2d	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land \neg k ∥ N) \to {(A /_{L} k)}^{k pCnt N} = {(A /_{L} k)}^{0}$
314	200	adantr	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land \neg k ∥ N) \to A /_{L} k \in ℂ$
315	314	exp0d	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land \neg k ∥ N) \to {(A /_{L} k)}^{0} = 1$
316	313 315	eqtrd	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land \neg k ∥ N) \to {(A /_{L} k)}^{k pCnt N} = 1$
317		neeq1	$⊢ x = 1 \to (x \neq 0 \leftrightarrow 1 \neq 0)$
318	317	elrab	$⊢ 1 \in \{x \in ℂ \| x \neq 0\} \leftrightarrow (1 \in ℂ \land 1 \neq 0)$
319	45 4 318	mpbir2an	$⊢ 1 \in \{x \in ℂ \| x \neq 0\}$
320	316 319	eqeltrdi	$⊢ ((((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \land \neg k ∥ N) \to {(A /_{L} k)}^{k pCnt N} \in \{x \in ℂ \| x \neq 0\}$
321	301 320	pm2.61dan	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in ℙ) \to {(A /_{L} k)}^{k pCnt N} \in \{x \in ℂ \| x \neq 0\}$
322	319	a1i	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land \neg k \in ℙ) \to 1 \in \{x \in ℂ \| x \neq 0\}$
323	321 322	ifclda	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) \in \{x \in ℂ \| x \neq 0\}$
324	323	adantr	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in (1 \dots \|N\|)) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) \in \{x \in ℂ \| x \neq 0\}$
325	194 324	eqeltrd	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in \{x \in ℂ \| x \neq 0\}$
326		neeq1	$⊢ x = k \to (x \neq 0 \leftrightarrow k \neq 0)$
327	326	elrab	$⊢ k \in \{x \in ℂ \| x \neq 0\} \leftrightarrow (k \in ℂ \land k \neq 0)$
328		neeq1	$⊢ x = y \to (x \neq 0 \leftrightarrow y \neq 0)$
329	328	elrab	$⊢ y \in \{x \in ℂ \| x \neq 0\} \leftrightarrow (y \in ℂ \land y \neq 0)$
330		mulcl	$⊢ (k \in ℂ \land y \in ℂ) \to k y \in ℂ$
331	330	ad2ant2r	$⊢ ((k \in ℂ \land k \neq 0) \land (y \in ℂ \land y \neq 0)) \to k y \in ℂ$
332		mulne0	$⊢ ((k \in ℂ \land k \neq 0) \land (y \in ℂ \land y \neq 0)) \to k y \neq 0$
333	331 332	jca	$⊢ ((k \in ℂ \land k \neq 0) \land (y \in ℂ \land y \neq 0)) \to (k y \in ℂ \land k y \neq 0)$
334	327 329 333	syl2anb	$⊢ (k \in \{x \in ℂ \| x \neq 0\} \land y \in \{x \in ℂ \| x \neq 0\}) \to (k y \in ℂ \land k y \neq 0)$
335		neeq1	$⊢ x = k y \to (x \neq 0 \leftrightarrow k y \neq 0)$
336	335	elrab	$⊢ k y \in \{x \in ℂ \| x \neq 0\} \leftrightarrow (k y \in ℂ \land k y \neq 0)$
337	334 336	sylibr	$⊢ (k \in \{x \in ℂ \| x \neq 0\} \land y \in \{x \in ℂ \| x \neq 0\}) \to k y \in \{x \in ℂ \| x \neq 0\}$
338	337	adantl	$⊢ (((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \land (k \in \{x \in ℂ \| x \neq 0\} \land y \in \{x \in ℂ \| x \neq 0\})) \to k y \in \{x \in ℂ \| x \neq 0\}$
339	184 325 338	seqcl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in \{x \in ℂ \| x \neq 0\}$
340		neeq1	$⊢ x = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \to (x \neq 0 \leftrightarrow seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0)$
341	340	elrab	$⊢ seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in \{x \in ℂ \| x \neq 0\} \leftrightarrow (seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in ℂ \land seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0)$
342	341	simprbi	$⊢ seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in \{x \in ℂ \| x \neq 0\} \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0$
343	339 342	syl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land A \gcd N = 1) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0$
344	343	ex	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (A \gcd N = 1 \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0)$
345	183 344	impbid	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \neq 0 \leftrightarrow A \gcd N = 1)$
346	38 61 345	3bitrd	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (A /_{L} N \neq 0 \leftrightarrow A \gcd N = 1)$
347	346	3expa	$⊢ ((A \in ℤ \land N \in ℤ) \land N \neq 0) \to (A /_{L} N \neq 0 \leftrightarrow A \gcd N = 1)$
348	35 347	pm2.61dane	$⊢ (A \in ℤ \land N \in ℤ) \to (A /_{L} N \neq 0 \leftrightarrow A \gcd N = 1)$

Metamath Proof Explorer

Theorem lgsne0

Proof