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 27394

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 4540	. . . . . 6 ⊢ (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0)
2	1	necon1ai 2966	. . . . 5 ⊢ (if((𝐴↑2) = 1, 1, 0) ≠ 0 → (𝐴↑2) = 1)
3		iftrue 4537	. . . . . 6 ⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 1)
4		ax-1ne0 11222	. . . . . . 7 ⊢ 1 ≠ 0
5	4	a1i 11	. . . . . 6 ⊢ ((𝐴↑2) = 1 → 1 ≠ 0)
6	3, 5	eqnetrd 3006	. . . . 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 12615	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
9	8	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℝ)
10		absresq 15338	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
11	9, 10	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((abs‘𝐴)↑2) = (𝐴↑2))
12		sq1 14231	. . . . . . 7 ⊢ (1↑2) = 1
13	12	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (1↑2) = 1)
14	11, 13	eqeq12d 2751	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔ (𝐴↑2) = 1))
15	9	recnd 11287	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℂ)
16	15	abscld 15472	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (abs‘𝐴) ∈ ℝ)
17	15	absge0d 15480	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ≤ (abs‘𝐴))
18		1re 11259	. . . . . . 7 ⊢ 1 ∈ ℝ
19		0le1 11784	. . . . . . 7 ⊢ 0 ≤ 1
20		sq11 14168	. . . . . . 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 7439	. . . . 5 ⊢ (𝑁 = 0 → (𝐴 /_L 𝑁) = (𝐴 /_L 0))
26		lgs0 27369	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
27	26	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
28	25, 27	sylan9eqr 2797	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 /_L 𝑁) = if((𝐴↑2) = 1, 1, 0))
29	28	neeq1d 2998	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ if((𝐴↑2) = 1, 1, 0) ≠ 0))
30		oveq2 7439	. . . . 5 ⊢ (𝑁 = 0 → (𝐴 gcd 𝑁) = (𝐴 gcd 0))
31		gcdid0 16554	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
32	31	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 gcd 0) = (abs‘𝐴))
33	30, 32	sylan9eqr 2797	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 gcd 𝑁) = (abs‘𝐴))
34	33	eqeq1d 2737	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 gcd 𝑁) = 1 ↔ (abs‘𝐴) = 1))
35	24, 29, 34	3bitr4d 311	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
36		eqid 2735	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
37	36	lgsval4 27376	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
38	37	neeq1d 2998	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0))
39		neeq1 3001	. . . . . . 7 ⊢ (-1 = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) → (-1 ≠ 0 ↔ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0))
40		neeq1 3001	. . . . . . 7 ⊢ (1 = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) → (1 ≠ 0 ↔ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0))
41		neg1ne0 12380	. . . . . . 7 ⊢ -1 ≠ 0
42	39, 40, 41, 4	keephyp 4602	. . . . . 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 12378	. . . . . . . 8 ⊢ -1 ∈ ℂ
45		ax-1cn 11211	. . . . . . . 8 ⊢ 1 ∈ ℂ
46	44, 45	ifcli 4578	. . . . . . 7 ⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ
47	46	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
48		nnabscl 15361	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
49	48	3adant1 1129	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
50		nnuz 12919	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
51	49, 50	eleqtrdi 2849	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ (ℤ_≥‘1))
52	36	lgsfcl3 27377	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
53		elfznn 13590	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ)
54		ffvelcdm 7101	. . . . . . . . 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 12721	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
57		mulcl 11237	. . . . . . . 8 ⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ)
58	57	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
59	51, 56, 58	seqcl 14060	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
60	47, 59	mulne0bd 11912	. . . . 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 16543	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℕ)
63		eluz2b3 12962	. . . . . . . . 9 ⊢ ((𝐴 gcd 𝑁) ∈ (ℤ_≥‘2) ↔ ((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1))
64		exprmfct 16738	. . . . . . . . 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 11437	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℂ → (0 · 𝑘) = 0)
69	68	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (0 · 𝑘) = 0)
70		mul01 11438	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℂ → (𝑘 · 0) = 0)
71	70	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) = 0)
72		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (𝐴 gcd 𝑁))
73		prmz 16709	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
74	73	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℤ)
75		simpl1 1190	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝐴 ∈ ℤ)
76		simpl2 1191	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℤ)
77		dvdsgcdb 16579	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
78	74, 75, 76, 77	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
79	72, 78	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁))
80	79	simprd 495	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ 𝑁)
81		dvdsabsb 16310	. . . . . . . . . . . . . 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 16344	. . . . . . . . . . . . 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 16708	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
89	88	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℕ)
90	89, 50	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (ℤ_≥‘1))
91	84	nnzd 12638	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℤ)
92		elfz5 13553	. . . . . . . . . . . 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 2822	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
96		oveq2 7439	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑝 → (𝐴 /_L 𝑛) = (𝐴 /_L 𝑝))
97		oveq1 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑁) = (𝑝 pCnt 𝑁))
98	96, 97	oveq12d 7449	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑝 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)))
99	95, 98	ifbieq1d 4555	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
100		ovex 7464	. . . . . . . . . . . . . 14 ⊢ ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)) ∈ V
101		1ex 11255	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
102	100, 101	ifex 4581	. . . . . . . . . . . . 13 ⊢ if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1) ∈ V
103	99, 36, 102	fvmpt 7016	. . . . . . . . . . . 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 4537	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)))
106	105	ad2antrl 728	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → if(𝑝 ∈ ℙ, ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)))
107		oveq2 7439	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 2 → (𝐴 /_L 𝑝) = (𝐴 /_L 2))
108		lgs2 27373	. . . . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . . 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 5172	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 2 ∥ 𝐴)
115	114	iftrued 4539	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = 0)
116	110, 115	eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /_L 𝑝) = 0)
117		simpll1 1211	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝐴 ∈ ℤ)
118		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℙ)
119	118	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℙ)
120		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ≠ 2)
121		eldifsn 4791	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ {2}) ↔ (𝑝 ∈ ℙ ∧ 𝑝 ≠ 2))
122	119, 120, 121	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℙ ∖ {2}))
123		lgsval3 27374	. . . . . . . . . . . . . . . 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 16844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 ∈ (ℙ ∖ {2}) → ((𝑝 − 1) / 2) ∈ ℕ)
126	122, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ)
127	126	nnnn0d 12585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ₀)
128		zexpcl 14114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℤ ∧ ((𝑝 − 1) / 2) ∈ ℕ₀) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
129	117, 127, 128	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
130	129	zred 12720	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℝ)
131		0red 11262	. . . . . . . . . . . . . . . . . . . 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 13073	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℝ⁺)
135		0zd 12623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℤ)
136	112	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∥ 𝐴)
137		dvdsval3 16291	. . . . . . . . . . . . . . . . . . . . . . . . 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 13939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 ∈ ℝ⁺ → (0 mod 𝑝) = 0)
141	134, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0 mod 𝑝) = 0)
142	139, 141	eqtr4d 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = (0 mod 𝑝))
143		modexp 14274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (((𝑝 − 1) / 2) ∈ ℕ₀ ∧ 𝑝 ∈ ℝ⁺) ∧ (𝐴 mod 𝑝) = (0 mod 𝑝)) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝))
144	117, 135, 127, 134, 142, 143	syl221anc 1380	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝))
145	126	0expd 14176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0↑((𝑝 − 1) / 2)) = 0)
146	145	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((0↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
147	144, 146	eqtrd 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
148		modadd1 13945	. . . . . . . . . . . . . . . . . . . 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 1380	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝))
150		0p1e1 12386	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 + 1) = 1
151	150	oveq1i 7441	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 + 1) mod 𝑝) = (1 mod 𝑝)
152	149, 151	eqtrdi 2791	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = (1 mod 𝑝))
153	133	nnred 12279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℝ)
154		prmuz2 16730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
155	119, 154	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℤ_≥‘2))
156		eluz2b2 12961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ (ℤ_≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝))
157	155, 156	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝 ∈ ℕ ∧ 1 < 𝑝))
158	157	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 < 𝑝)
159		1mod 13940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ∈ ℝ ∧ 1 < 𝑝) → (1 mod 𝑝) = 1)
160	153, 158, 159	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (1 mod 𝑝) = 1)
161	152, 160	eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = 1)
162	161	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = (1 − 1))
163		1m1e0 12336	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
164	162, 163	eqtrdi 2791	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = 0)
165	124, 164	eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /_L 𝑝) = 0)
166	116, 165	pm2.61dane 3027	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /_L 𝑝) = 0)
167	166	oveq1d 7446	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)) = (0↑(𝑝 pCnt 𝑁)))
168		zq 12994	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℚ)
169	76, 168	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℚ)
170		pcabs 16909	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
171	118, 169, 170	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
172		pcelnn 16904	. . . . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt 𝑁) ∈ ℕ)
176	175	0expd 14176	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (0↑(𝑝 pCnt 𝑁)) = 0)
177	167, 176	eqtrd 2775	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /_L 𝑝)↑(𝑝 pCnt 𝑁)) = 0)
178	104, 106, 177	3eqtrd 2779	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = 0)
179	66, 67, 69, 71, 94, 84, 178	seqz 14088	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)
180	179	rexlimdvaa 3154	. . . . . . . 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 2960	. . . . 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 2822	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
187		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (𝐴 /_L 𝑛) = (𝐴 /_L 𝑘))
188		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
189	187, 188	oveq12d 7449	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
190	186, 189	ifbieq1d 4555	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
191		ovex 7464	. . . . . . . . . . . 12 ⊢ ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
192	191, 101	ifex 4581	. . . . . . . . . . 11 ⊢ if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
193	190, 36, 192	fvmpt 7016	. . . . . . . . . 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 1211	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
196		prmz 16709	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
197	196	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
198		lgscl 27370	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /_L 𝑘) ∈ ℤ)
199	195, 197, 198	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℤ)
200	199	zcnd 12721	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℂ)
201	200	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝐴 /_L 𝑘) ∈ ℂ)
202		oveq2 7439	. . . . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → (𝐴 /_L 𝑘) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
206		nprmdvds1 16740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 1)
207	206	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ 1)
208		simpll2 1212	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
209		dvdsgcdb 16579	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
210	197, 195, 208, 209	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
211		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 gcd 𝑁) = 1)
212	211	breq2d 5160	. . . . . . . . . . . . . . . . . . . . . . . 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 5151	. . . . . . . . . . . . . . . . . . . 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 4542	. . . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → (𝐴 /_L 𝑘) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
225		neeq1 3001	. . . . . . . . . . . . . . . . 17 ⊢ (1 = if((𝐴 mod 8) ∈ {1, 7}, 1, -1) → (1 ≠ 0 ↔ if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0))
226		neeq1 3001	. . . . . . . . . . . . . . . . 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 4602	. . . . . . . . . . . . . . . 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 3006	. . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . . 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 4791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (ℙ ∖ {2}) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ≠ 2))
238	231, 236, 237	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ (ℙ ∖ {2}))
239		oddprm 16844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (ℙ ∖ {2}) → ((𝑘 − 1) / 2) ∈ ℕ)
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ)
241	240	nnnn0d 12585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ₀)
242		zexpcl 14114	. . . . . . . . . . . . . . . . . . . . . 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 16578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℤ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘 ∥ 𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
246	234, 243, 244, 245	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 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 12721	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℂ)
249	248, 241	absexpd 15488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (abs‘(𝐴↑((𝑘 − 1) / 2))) = ((abs‘𝐴)↑((𝑘 − 1) / 2)))
250	249	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)))
251		gcdabs 16565	. . . . . . . . . . . . . . . . . . . . . 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 16565	. . . . . . . . . . . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = 1)
257	218	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ 𝐴)
258		dvds0 16306	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ ℤ → 𝑘 ∥ 0)
259	234, 258	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∥ 0)
260		breq2 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 = 0 → (𝑘 ∥ 𝐴 ↔ 𝑘 ∥ 0))
261	259, 260	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴 = 0 → 𝑘 ∥ 𝐴))
262	261	necon3bd 2952	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘 ∥ 𝐴 → 𝐴 ≠ 0))
263	257, 262	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ≠ 0)
264		nnabscl 15361	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
265	235, 263, 264	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝐴) ∈ ℕ)
266		simpll3 1213	. . . . . . . . . . . . . . . . . . . . . . . . 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 16592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((abs‘𝐴) ∈ ℕ ∧ (abs‘𝑁) ∈ ℕ ∧ ((𝑘 − 1) / 2) ∈ ℕ) → (((abs‘𝐴) gcd (abs‘𝑁)) = 1 → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1))
270	265, 268, 240, 269	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) = 1)
273	272	breq2d 5160	. . . . . . . . . . . . . . . . . . 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 16708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
277	276	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℕ)
278	277	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℕ)
279		dvdsval3 16291	. . . . . . . . . . . . . . . . . . 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 2976	. . . . . . . . . . . . . . . . 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 27375	. . . . . . . . . . . . . . . . 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 13073	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℝ⁺)
286		0mod 13939	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℝ⁺ → (0 mod 𝑘) = 0)
287	285, 286	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (0 mod 𝑘) = 0)
288	282, 284, 287	3netr4d 3016	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /_L 𝑘) mod 𝑘) ≠ (0 mod 𝑘))
289		oveq1 7438	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 /_L 𝑘) = 0 → ((𝐴 /_L 𝑘) mod 𝑘) = (0 mod 𝑘))
290	289	necon3i 2971	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 /_L 𝑘) mod 𝑘) ≠ (0 mod 𝑘) → (𝐴 /_L 𝑘) ≠ 0)
291	288, 290	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴 /_L 𝑘) ≠ 0)
292	229, 291	pm2.61dane 3027	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝐴 /_L 𝑘) ≠ 0)
293		pczcl 16882	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
294	230, 208, 266, 293	syl12anc 837	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
295	294	nn0zd 12637	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℤ)
296	295	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝑘 pCnt 𝑁) ∈ ℤ)
297		neeq1 3001	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) → (𝑥 ≠ 0 ↔ ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0))
298		expclz 14122	. . . . . . . . . . . . . 14 ⊢ (((𝐴 /_L 𝑘) ∈ ℂ ∧ (𝐴 /_L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℂ)
299		expne0i 14132	. . . . . . . . . . . . . 14 ⊢ (((𝐴 /_L 𝑘) ∈ ℂ ∧ (𝐴 /_L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0)
300	297, 298, 299	elrabd 3697	. . . . . . . . . . . . 13 ⊢ (((𝐴 /_L 𝑘) ∈ ℂ ∧ (𝐴 /_L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
301	201, 292, 296, 300	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
302		dvdsabsb 16310	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∥ 𝑁 ↔ 𝑘 ∥ (abs‘𝑁)))
303	197, 208, 302	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ 𝑁 ↔ 𝑘 ∥ (abs‘𝑁)))
304	303	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (¬ 𝑘 ∥ 𝑁 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
305		pceq0 16905	. . . . . . . . . . . . . . . . . 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 16909	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
309	230, 307, 308	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
310	309	eqeq1d 2737	. . . . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) = ((𝐴 /_L 𝑘)↑0))
314	200	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → (𝐴 /_L 𝑘) ∈ ℂ)
315	314	exp0d 14177	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑0) = 1)
316	313, 315	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) = 1)
317		neeq1 3001	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝑥 ≠ 0 ↔ 1 ≠ 0))
318	317	elrab 3695	. . . . . . . . . . . . . 14 ⊢ (1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (1 ∈ ℂ ∧ 1 ≠ 0))
319	45, 4, 318	mpbir2an 711	. . . . . . . . . . . . 13 ⊢ 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}
320	316, 319	eqeltrdi 2847	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
321	301, 320	pm2.61dan 813	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
322	319	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
323	321, 322	ifclda 4566	. . . . . . . . . 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 2839	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
326		neeq1 3001	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑘 → (𝑥 ≠ 0 ↔ 𝑘 ≠ 0))
327	326	elrab 3695	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
328		neeq1 3001	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ≠ 0 ↔ 𝑦 ≠ 0))
329	328	elrab 3695	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
330		mulcl 11237	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑘 · 𝑦) ∈ ℂ)
331	330	ad2ant2r 747	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑘 · 𝑦) ∈ ℂ)
332		mulne0 11903	. . . . . . . . . . . 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 3001	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 · 𝑦) → (𝑥 ≠ 0 ↔ (𝑘 · 𝑦) ≠ 0))
336	335	elrab 3695	. . . . . . . . . 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 14060	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
340		neeq1 3001	. . . . . . . . 9 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) → (𝑥 ≠ 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
341	340	elrab 3695	. . . . . . . 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 1117	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
348	35, 347	pm2.61dane 3027	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 /_L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∃wrex 3068 {crab 3433 ∖ cdif 3960 ifcif 4531 {csn 4631 {cpr 4633 class class class wbr 5148 ↦ cmpt 5231 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 · cmul 11158 < clt 11293 ≤ cle 11294 − cmin 11490 -cneg 11491 / cdiv 11918 ℕcn 12264 2c2 12319 7c7 12324 8c8 12325 ℕ₀cn0 12524 ℤcz 12611 ℤ_≥cuz 12876 ℚcq 12988 ℝ⁺crp 13032 ...cfz 13544 mod cmo 13906 seqcseq 14039 ↑cexp 14099 abscabs 15270 ∥ cdvds 16287 gcd cgcd 16528 ℙcprime 16705 pCnt cpc 16870 /_L clgs 27353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-2o 8506 df-oadd 8509 df-er 8744 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-sup 9480 df-inf 9481 df-dju 9939 df-card 9977 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-n0 12525 df-xnn0 12598 df-z 12612 df-uz 12877 df-q 12989 df-rp 13033 df-fz 13545 df-fzo 13692 df-fl 13829 df-mod 13907 df-seq 14040 df-exp 14100 df-hash 14367 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-dvds 16288 df-gcd 16529 df-prm 16706 df-phi 16800 df-pc 16871 df-lgs 27354

This theorem is referenced by: lgsabs1 27395 lgsprme0 27398 lgsdirnn0 27403 lgsqr 27410 lgsdchr 27414 lgsquad3 27446 2lgsoddprm 27475

W3C validator