lgsne0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgsne0		Structured version Visualization version GIF version

Theorem lgsne0 27263

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

**Assertion**
Ref	Expression
lgsne0	⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))

Proof of Theorem lgsne0 Dummy variables 𝑘 𝑛 𝑥 𝑦 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iffalse 4487	. . . . . 6 ⊢ (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0)
2	1	necon1ai 2952	. . . . 5 ⊢ (if((𝐴↑2) = 1, 1, 0) ≠ 0 → (𝐴↑2) = 1)
3		iftrue 4484	. . . . . 6 ⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 1)
4		ax-1ne0 11097	. . . . . . 7 ⊢ 1 ≠ 0
5	4	a1i 11	. . . . . 6 ⊢ ((𝐴↑2) = 1 → 1 ≠ 0)
6	3, 5	eqnetrd 2992	. . . . 5 ⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) ≠ 0)
7	2, 6	impbii 209	. . . 4 ⊢ (if((𝐴↑2) = 1, 1, 0) ≠ 0 ↔ (𝐴↑2) = 1)
8		zre 12494	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
9	8	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℝ)
10		absresq 15228	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
11	9, 10	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((abs‘𝐴)↑2) = (𝐴↑2))
12		sq1 14121	. . . . . . 7 ⊢ (1↑2) = 1
13	12	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (1↑2) = 1)
14	11, 13	eqeq12d 2745	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔ (𝐴↑2) = 1))
15	9	recnd 11162	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℂ)
16	15	abscld 15365	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (abs‘𝐴) ∈ ℝ)
17	15	absge0d 15373	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ≤ (abs‘𝐴))
18		1re 11134	. . . . . . 7 ⊢ 1 ∈ ℝ
19		0le1 11662	. . . . . . 7 ⊢ 0 ≤ 1
20		sq11 14057	. . . . . . 7 ⊢ ((((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
21	18, 19, 20	mpanr12 705	. . . . . 6 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
22	16, 17, 21	syl2anc 584	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
23	14, 22	bitr3d 281	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ↔ (abs‘𝐴) = 1))
24	7, 23	bitrid 283	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) ≠ 0 ↔ (abs‘𝐴) = 1))
25		oveq2 7361	. . . . 5 ⊢ (𝑁 = 0 → (𝐴 /_L 𝑁) = (𝐴 /_L 0))
26		lgs0 27238	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
27	26	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
28	25, 27	sylan9eqr 2786	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 /_L 𝑁) = if((𝐴↑2) = 1, 1, 0))
29	28	neeq1d 2984	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ if((𝐴↑2) = 1, 1, 0) ≠ 0))
30		oveq2 7361	. . . . 5 ⊢ (𝑁 = 0 → (𝐴 gcd 𝑁) = (𝐴 gcd 0))
31		gcdid0 16450	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
32	31	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 gcd 0) = (abs‘𝐴))
33	30, 32	sylan9eqr 2786	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 gcd 𝑁) = (abs‘𝐴))
34	33	eqeq1d 2731	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 gcd 𝑁) = 1 ↔ (abs‘𝐴) = 1))
35	24, 29, 34	3bitr4d 311	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
36		eqid 2729	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
37	36	lgsval4 27245	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
38	37	neeq1d 2984	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0))
39		neeq1 2987	. . . . . . 7 ⊢ (-1 = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) → (-1 ≠ 0 ↔ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0))
40		neeq1 2987	. . . . . . 7 ⊢ (1 = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) → (1 ≠ 0 ↔ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0))
41		neg1ne0 12134	. . . . . . 7 ⊢ -1 ≠ 0
42	39, 40, 41, 4	keephyp 4550	. . . . . 6 ⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0
43	42	biantrur 530	. . . . 5 ⊢ ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
44		neg1cn 12132	. . . . . . . 8 ⊢ -1 ∈ ℂ
45		ax-1cn 11086	. . . . . . . 8 ⊢ 1 ∈ ℂ
46	44, 45	ifcli 4526	. . . . . . 7 ⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ
47	46	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
48		nnabscl 15252	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
49	48	3adant1 1130	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
50		nnuz 12797	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
51	49, 50	eleqtrdi 2838	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ (ℤ_≥‘1))
52	36	lgsfcl3 27246	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
53		elfznn 13475	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ)
54		ffvelcdm 7019	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
55	52, 53, 54	syl2an 596	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
56	55	zcnd 12600	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
57		mulcl 11112	. . . . . . . 8 ⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ)
58	57	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
59	51, 56, 58	seqcl 13948	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
60	47, 59	mulne0bd 11790	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0) ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0))
61	43, 60	bitr2id 284	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
62		gcd2n0cl 16439	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℕ)
63		eluz2b3 12842	. . . . . . . . 9 ⊢ ((𝐴 gcd 𝑁) ∈ (ℤ_≥‘2) ↔ ((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1))
64		exprmfct 16634	. . . . . . . . 9 ⊢ ((𝐴 gcd 𝑁) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁))
65	63, 64	sylbir 235	. . . . . . . 8 ⊢ (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁))
66	57	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
67	56	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
68		mul02 11313	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℂ → (0 · 𝑘) = 0)
69	68	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (0 · 𝑘) = 0)
70		mul01 11314	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℂ → (𝑘 · 0) = 0)
71	70	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) = 0)
72		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (𝐴 gcd 𝑁))
73		prmz 16605	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
74	73	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℤ)
75		simpl1 1192	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝐴 ∈ ℤ)
76		simpl2 1193	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℤ)
77		dvdsgcdb 16475	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
78	74, 75, 76, 77	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
79	72, 78	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁))
80	79	simprd 495	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ 𝑁)
81		dvdsabsb 16205	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑝 ∥ 𝑁 ↔ 𝑝 ∥ (abs‘𝑁)))
82	74, 76, 81	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ 𝑁 ↔ 𝑝 ∥ (abs‘𝑁)))
83	80, 82	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (abs‘𝑁))
84	49	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℕ)
85		dvdsle 16240	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ (abs‘𝑁) ∈ ℕ) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁)))
86	74, 84, 85	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁)))
87	83, 86	mpd 15	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ≤ (abs‘𝑁))
88		prmnn 16604	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
89	88	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℕ)
90	89, 50	eleqtrdi 2838	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (ℤ_≥‘1))
91	84	nnzd 12517	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℤ)
92		elfz5 13438	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ (ℤ_≥‘1) ∧ (abs‘𝑁) ∈ ℤ) → (𝑝 ∈ (1...(abs‘𝑁)) ↔ 𝑝 ≤ (abs‘𝑁)))
93	90, 91, 92	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∈ (1...(abs‘𝑁)) ↔ 𝑝 ≤ (abs‘𝑁)))
94	87, 93	mpbird 257	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (1...(abs‘𝑁)))
95		eleq1w 2811	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
96		oveq2 7361	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑝 → (𝐴 /_L 𝑛) = (𝐴 /_L 𝑝))
97		oveq1 7360	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑁) = (𝑝 pCnt 𝑁))
98	96, 97	oveq12d 7371	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑝 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)))
99	95, 98	ifbieq1d 4503	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
100		ovex 7386	. . . . . . . . . . . . . 14 ⊢ ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)) ∈ V
101		1ex 11130	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
102	100, 101	ifex 4529	. . . . . . . . . . . . 13 ⊢ if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1) ∈ V
103	99, 36, 102	fvmpt 6934	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
104	89, 103	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
105		iftrue 4484	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)))
106	105	ad2antrl 728	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)))
107		oveq2 7361	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 2 → (𝐴 /_L 𝑝) = (𝐴 /_L 2))
108		lgs2 27242	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → (𝐴 /_L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
109	75, 108	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /_L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
110	107, 109	sylan9eqr 2786	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /_L 𝑝) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
111		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 𝑝 = 2)
112	79	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ 𝐴)
113	112	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 𝑝 ∥ 𝐴)
114	111, 113	eqbrtrrd 5119	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 2 ∥ 𝐴)
115	114	iftrued 4486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = 0)
116	110, 115	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /_L 𝑝) = 0)
117		simpll1 1213	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝐴 ∈ ℤ)
118		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℙ)
119	118	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℙ)
120		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ≠ 2)
121		eldifsn 4740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ {2}) ↔ (𝑝 ∈ ℙ ∧ 𝑝 ≠ 2))
122	119, 120, 121	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℙ ∖ {2}))
123		lgsval3 27243	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (ℙ ∖ {2})) → (𝐴 /_L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1))
124	117, 122, 123	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /_L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1))
125		oddprm 16741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 ∈ (ℙ ∖ {2}) → ((𝑝 − 1) / 2) ∈ ℕ)
126	122, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ)
127	126	nnnn0d 12464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ₀)
128		zexpcl 14002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℤ ∧ ((𝑝 − 1) / 2) ∈ ℕ₀) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
129	117, 127, 128	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
130	129	zred 12599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℝ)
131		0red 11137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℝ)
132	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 ∈ ℝ)
133	119, 88	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℕ)
134	133	nnrpd 12954	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℝ⁺)
135		0zd 12502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℤ)
136	112	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∥ 𝐴)
137		dvdsval3 16186	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑝 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝑝 ∥ 𝐴 ↔ (𝐴 mod 𝑝) = 0))
138	133, 117, 137	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝 ∥ 𝐴 ↔ (𝐴 mod 𝑝) = 0))
139	136, 138	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = 0)
140		0mod 13825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 ∈ ℝ⁺ → (0 mod 𝑝) = 0)
141	134, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0 mod 𝑝) = 0)
142	139, 141	eqtr4d 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = (0 mod 𝑝))
143		modexp 14164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (((𝑝 − 1) / 2) ∈ ℕ₀ ∧ 𝑝 ∈ ℝ⁺) ∧ (𝐴 mod 𝑝) = (0 mod 𝑝)) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝))
144	117, 135, 127, 134, 142, 143	syl221anc 1383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝))
145	126	0expd 14065	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0↑((𝑝 − 1) / 2)) = 0)
146	145	oveq1d 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((0↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
147	144, 146	eqtrd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
148		modadd1 13831	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴↑((𝑝 − 1) / 2)) ∈ ℝ ∧ 0 ∈ ℝ) ∧ (1 ∈ ℝ ∧ 𝑝 ∈ ℝ⁺) ∧ ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝)) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝))
149	130, 131, 132, 134, 147, 148	syl221anc 1383	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝))
150		0p1e1 12264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 + 1) = 1
151	150	oveq1i 7363	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 + 1) mod 𝑝) = (1 mod 𝑝)
152	149, 151	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = (1 mod 𝑝))
153	133	nnred 12162	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℝ)
154		prmuz2 16626	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
155	119, 154	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℤ_≥‘2))
156		eluz2b2 12841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ (ℤ_≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝))
157	155, 156	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝 ∈ ℕ ∧ 1 < 𝑝))
158	157	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 < 𝑝)
159		1mod 13826	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ∈ ℝ ∧ 1 < 𝑝) → (1 mod 𝑝) = 1)
160	153, 158, 159	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (1 mod 𝑝) = 1)
161	152, 160	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = 1)
162	161	oveq1d 7368	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = (1 − 1))
163		1m1e0 12219	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
164	162, 163	eqtrdi 2780	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = 0)
165	124, 164	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /_L 𝑝) = 0)
166	116, 165	pm2.61dane 3012	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /_L 𝑝) = 0)
167	166	oveq1d 7368	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)) = (0↑(𝑝 pCnt 𝑁)))
168		zq 12874	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℚ)
169	76, 168	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℚ)
170		pcabs 16806	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
171	118, 169, 170	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
172		pcelnn 16801	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (abs‘𝑁) ∈ ℕ) → ((𝑝 pCnt (abs‘𝑁)) ∈ ℕ ↔ 𝑝 ∥ (abs‘𝑁)))
173	118, 84, 172	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝 pCnt (abs‘𝑁)) ∈ ℕ ↔ 𝑝 ∥ (abs‘𝑁)))
174	83, 173	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) ∈ ℕ)
175	171, 174	eqeltrrd 2829	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt 𝑁) ∈ ℕ)
176	175	0expd 14065	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (0↑(𝑝 pCnt 𝑁)) = 0)
177	167, 176	eqtrd 2764	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)) = 0)
178	104, 106, 177	3eqtrd 2768	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = 0)
179	66, 67, 69, 71, 94, 84, 178	seqz 13976	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)
180	179	rexlimdvaa 3131	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
181	65, 180	syl5 34	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
182	62, 181	mpand 695	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 gcd 𝑁) ≠ 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
183	182	necon1d 2947	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 → (𝐴 gcd 𝑁) = 1))
184	51	adantr 480	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (abs‘𝑁) ∈ (ℤ_≥‘1))
185	53	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → 𝑘 ∈ ℕ)
186		eleq1w 2811	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
187		oveq2 7361	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (𝐴 /_L 𝑛) = (𝐴 /_L 𝑘))
188		oveq1 7360	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
189	187, 188	oveq12d 7371	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
190	186, 189	ifbieq1d 4503	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
191		ovex 7386	. . . . . . . . . . . 12 ⊢ ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
192	191, 101	ifex 4529	. . . . . . . . . . 11 ⊢ if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
193	190, 36, 192	fvmpt 6934	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
194	185, 193	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
195		simpll1 1213	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
196		prmz 16605	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
197	196	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
198		lgscl 27239	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /_L 𝑘) ∈ ℤ)
199	195, 197, 198	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℤ)
200	199	zcnd 12600	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℂ)
201	200	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝐴 /_L 𝑘) ∈ ℂ)
202		oveq2 7361	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝐴 /_L 𝑘) = (𝐴 /_L 2))
203	195	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → 𝐴 ∈ ℤ)
204	203, 108	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝐴 /_L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
205	202, 204	sylan9eqr 2786	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → (𝐴 /_L 𝑘) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
206		nprmdvds1 16636	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 1)
207	206	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ 1)
208		simpll2 1214	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
209		dvdsgcdb 16475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
210	197, 195, 208, 209	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
211		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 gcd 𝑁) = 1)
212	211	breq2d 5107	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ (𝐴 gcd 𝑁) ↔ 𝑘 ∥ 1))
213	210, 212	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁) ↔ 𝑘 ∥ 1))
214	207, 213	mtbird 325	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ (𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁))
215		imnan 399	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∥ 𝐴 → ¬ 𝑘 ∥ 𝑁) ↔ ¬ (𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁))
216	214, 215	sylibr 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ 𝐴 → ¬ 𝑘 ∥ 𝑁))
217	216	con2d 134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ 𝑁 → ¬ 𝑘 ∥ 𝐴))
218	217	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → ¬ 𝑘 ∥ 𝐴)
219		breq1 5098	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 2 → (𝑘 ∥ 𝐴 ↔ 2 ∥ 𝐴))
220	219	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (¬ 𝑘 ∥ 𝐴 ↔ ¬ 2 ∥ 𝐴))
221	218, 220	syl5ibcom 245	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝑘 = 2 → ¬ 2 ∥ 𝐴))
222	221	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → ¬ 2 ∥ 𝐴)
223	222	iffalsed 4489	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
224	205, 223	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → (𝐴 /_L 𝑘) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
225		neeq1 2987	. . . . . . . . . . . . . . . . 17 ⊢ (1 = if((𝐴 mod 8) ∈ {1, 7}, 1, -1) → (1 ≠ 0 ↔ if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0))
226		neeq1 2987	. . . . . . . . . . . . . . . . 17 ⊢ (-1 = if((𝐴 mod 8) ∈ {1, 7}, 1, -1) → (-1 ≠ 0 ↔ if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0))
227	225, 226, 4, 41	keephyp 4550	. . . . . . . . . . . . . . . 16 ⊢ if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0
228	227	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0)
229	224, 228	eqnetrd 2992	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → (𝐴 /_L 𝑘) ≠ 0)
230		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
231	230	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℙ)
232	231, 206	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ 1)
233		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∥ 𝑁)
234	231, 196	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℤ)
235	203	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℤ)
236		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ≠ 2)
237		eldifsn 4740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (ℙ ∖ {2}) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ≠ 2))
238	231, 236, 237	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ (ℙ ∖ {2}))
239		oddprm 16741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (ℙ ∖ {2}) → ((𝑘 − 1) / 2) ∈ ℕ)
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ)
241	240	nnnn0d 12464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ₀)
242		zexpcl 14002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈ ℕ₀) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
243	235, 241, 242	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
244	208	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑁 ∈ ℤ)
245		dvdsgcd 16474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℤ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘 ∥ 𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
246	234, 243, 244, 245	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘 ∥ 𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
247	233, 246	mpan2d 694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
248	235	zcnd 12600	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℂ)
249	248, 241	absexpd 15381	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (abs‘(𝐴↑((𝑘 − 1) / 2))) = ((abs‘𝐴)↑((𝑘 − 1) / 2)))
250	249	oveq1d 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)))
251		gcdabs 16461	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))
252	243, 244, 251	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))
253		gcdabs 16461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝐴) gcd (abs‘𝑁)) = (𝐴 gcd 𝑁))
254	235, 244, 253	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = (𝐴 gcd 𝑁))
255	211	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴 gcd 𝑁) = 1)
256	254, 255	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = 1)
257	218	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ 𝐴)
258		dvds0 16201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ ℤ → 𝑘 ∥ 0)
259	234, 258	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∥ 0)
260		breq2 5099	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 = 0 → (𝑘 ∥ 𝐴 ↔ 𝑘 ∥ 0))
261	259, 260	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴 = 0 → 𝑘 ∥ 𝐴))
262	261	necon3bd 2939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘 ∥ 𝐴 → 𝐴 ≠ 0))
263	257, 262	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ≠ 0)
264		nnabscl 15252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
265	235, 263, 264	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝐴) ∈ ℕ)
266		simpll3 1215	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
267	208, 266, 48	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (abs‘𝑁) ∈ ℕ)
268	267	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝑁) ∈ ℕ)
269		rplpwr 16488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((abs‘𝐴) ∈ ℕ ∧ (abs‘𝑁) ∈ ℕ ∧ ((𝑘 − 1) / 2) ∈ ℕ) → (((abs‘𝐴) gcd (abs‘𝑁)) = 1 → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1))
270	265, 268, 240, 269	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (((abs‘𝐴) gcd (abs‘𝑁)) = 1 → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1))
271	256, 270	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1)
272	250, 252, 271	3eqtr3d 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) = 1)
273	272	breq2d 5107	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) ↔ 𝑘 ∥ 1))
274	247, 273	sylibd 239	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) → 𝑘 ∥ 1))
275	232, 274	mtod 198	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)))
276		prmnn 16604	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
277	276	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℕ)
278	277	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℕ)
279		dvdsval3 16186	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) = 0))
280	278, 243, 279	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) = 0))
281	280	necon3bbid 2962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) ≠ 0))
282	275, 281	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) ≠ 0)
283		lgsvalmod 27244	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ (ℙ ∖ {2})) → ((𝐴 /_L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘))
284	235, 238, 283	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /_L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘))
285	278	nnrpd 12954	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℝ⁺)
286		0mod 13825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℝ⁺ → (0 mod 𝑘) = 0)
287	285, 286	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (0 mod 𝑘) = 0)
288	282, 284, 287	3netr4d 3002	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /_L 𝑘) mod 𝑘) ≠ (0 mod 𝑘))
289		oveq1 7360	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 /_L 𝑘) = 0 → ((𝐴 /_L 𝑘) mod 𝑘) = (0 mod 𝑘))
290	289	necon3i 2957	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 /_L 𝑘) mod 𝑘) ≠ (0 mod 𝑘) → (𝐴 /_L 𝑘) ≠ 0)
291	288, 290	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴 /_L 𝑘) ≠ 0)
292	229, 291	pm2.61dane 3012	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝐴 /_L 𝑘) ≠ 0)
293		pczcl 16779	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
294	230, 208, 266, 293	syl12anc 836	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
295	294	nn0zd 12516	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℤ)
296	295	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝑘 pCnt 𝑁) ∈ ℤ)
297		neeq1 2987	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) → (𝑥 ≠ 0 ↔ ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0))
298		expclz 14010	. . . . . . . . . . . . . 14 ⊢ (((𝐴 /_L 𝑘) ∈ ℂ ∧ (𝐴 /_L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℂ)
299		expne0i 14020	. . . . . . . . . . . . . 14 ⊢ (((𝐴 /_L 𝑘) ∈ ℂ ∧ (𝐴 /_L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0)
300	297, 298, 299	elrabd 3652	. . . . . . . . . . . . 13 ⊢ (((𝐴 /_L 𝑘) ∈ ℂ ∧ (𝐴 /_L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
301	201, 292, 296, 300	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
302		dvdsabsb 16205	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∥ 𝑁 ↔ 𝑘 ∥ (abs‘𝑁)))
303	197, 208, 302	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ 𝑁 ↔ 𝑘 ∥ (abs‘𝑁)))
304	303	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (¬ 𝑘 ∥ 𝑁 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
305		pceq0 16802	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℙ ∧ (abs‘𝑁) ∈ ℕ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
306	230, 267, 305	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
307	208, 168	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℚ)
308		pcabs 16806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
309	230, 307, 308	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
310	309	eqeq1d 2731	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ (𝑘 pCnt 𝑁) = 0))
311	304, 306, 310	3bitr2rd 308	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt 𝑁) = 0 ↔ ¬ 𝑘 ∥ 𝑁))
312	311	biimpar 477	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → (𝑘 pCnt 𝑁) = 0)
313	312	oveq2d 7369	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) = ((𝐴 /_L 𝑘)↑0))
314	200	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → (𝐴 /_L 𝑘) ∈ ℂ)
315	314	exp0d 14066	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑0) = 1)
316	313, 315	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) = 1)
317		neeq1 2987	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝑥 ≠ 0 ↔ 1 ≠ 0))
318	317	elrab 3650	. . . . . . . . . . . . . 14 ⊢ (1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (1 ∈ ℂ ∧ 1 ≠ 0))
319	45, 4, 318	mpbir2an 711	. . . . . . . . . . . . 13 ⊢ 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}
320	316, 319	eqeltrdi 2836	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
321	301, 320	pm2.61dan 812	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
322	319	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
323	321, 322	ifclda 4514	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
324	323	adantr 480	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
325	194, 324	eqeltrd 2828	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
326		neeq1 2987	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑘 → (𝑥 ≠ 0 ↔ 𝑘 ≠ 0))
327	326	elrab 3650	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
328		neeq1 2987	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ≠ 0 ↔ 𝑦 ≠ 0))
329	328	elrab 3650	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
330		mulcl 11112	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑘 · 𝑦) ∈ ℂ)
331	330	ad2ant2r 747	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑘 · 𝑦) ∈ ℂ)
332		mulne0 11781	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑘 · 𝑦) ≠ 0)
333	331, 332	jca 511	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0))
334	327, 329, 333	syl2anb 598	. . . . . . . . . 10 ⊢ ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0))
335		neeq1 2987	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 · 𝑦) → (𝑥 ≠ 0 ↔ (𝑘 · 𝑦) ≠ 0))
336	335	elrab 3650	. . . . . . . . . 10 ⊢ ((𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0))
337	334, 336	sylibr 234	. . . . . . . . 9 ⊢ ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
338	337	adantl 481	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
339	184, 325, 338	seqcl 13948	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
340		neeq1 2987	. . . . . . . . 9 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) → (𝑥 ≠ 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
341	340	elrab 3650	. . . . . . . 8 ⊢ ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
342	341	simprbi 496	. . . . . . 7 ⊢ ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)
343	339, 342	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)
344	343	ex 412	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 gcd 𝑁) = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
345	183, 344	impbid 212	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
346	38, 61, 345	3bitrd 305	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
347	346	3expa 1118	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
348	35, 347	pm2.61dane 3012	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 {crab 3396 ∖ cdif 3902 ifcif 4478 {csn 4579 {cpr 4581 class class class wbr 5095 ↦ cmpt 5176 ⟶wf 6482 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 < clt 11168 ≤ cle 11169 − cmin 11366 -cneg 11367 / cdiv 11796 ℕcn 12147 2c2 12202 7c7 12207 8c8 12208 ℕ₀cn0 12403 ℤcz 12490 ℤ_≥cuz 12754 ℚcq 12868 ℝ⁺crp 12912 ...cfz 13429 mod cmo 13792 seqcseq 13927 ↑cexp 13987 abscabs 15160 ∥ cdvds 16182 gcd cgcd 16424 ℙcprime 16601 pCnt cpc 16767 /_L clgs 27222

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9351 df-inf 9352 df-dju 9816 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-n0 12404 df-xnn0 12477 df-z 12491 df-uz 12755 df-q 12869 df-rp 12913 df-fz 13430 df-fzo 13577 df-fl 13715 df-mod 13793 df-seq 13928 df-exp 13988 df-hash 14257 df-cj 15025 df-re 15026 df-im 15027 df-sqrt 15161 df-abs 15162 df-dvds 16183 df-gcd 16425 df-prm 16602 df-phi 16696 df-pc 16768 df-lgs 27223

This theorem is referenced by: lgsabs1 27264 lgsprme0 27267 lgsdirnn0 27272 lgsqr 27279 lgsdchr 27283 lgsquad3 27315 2lgsoddprm 27344

W3C validator