Theorem lgsne0

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

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

Proof

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