ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lgsne0 GIF version

Theorem lgsne0 14010
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.
StepHypRef Expression
1 zsqcl 10560 . . . . . . . . 9 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
21adantr 276 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴↑2) ∈ ℤ)
3 1z 9252 . . . . . . . 8 1 ∈ ℤ
4 zdceq 9301 . . . . . . . 8 (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴↑2) = 1)
52, 3, 4sylancl 413 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐴↑2) = 1)
6 iffalse 3540 . . . . . . . . 9 (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0)
76a1i 9 . . . . . . . 8 (DECID (𝐴↑2) = 1 → (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0))
87necon1aidc 2396 . . . . . . 7 (DECID (𝐴↑2) = 1 → (if((𝐴↑2) = 1, 1, 0) ≠ 0 → (𝐴↑2) = 1))
95, 8syl 14 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (if((𝐴↑2) = 1, 1, 0) ≠ 0 → (𝐴↑2) = 1))
10 iftrue 3537 . . . . . . 7 ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 1)
11 1ne0 8960 . . . . . . . 8 1 ≠ 0
1211a1i 9 . . . . . . 7 ((𝐴↑2) = 1 → 1 ≠ 0)
1310, 12eqnetrd 2369 . . . . . 6 ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) ≠ 0)
149, 13impbid1 142 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (if((𝐴↑2) = 1, 1, 0) ≠ 0 ↔ (𝐴↑2) = 1))
1514adantr 276 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) ≠ 0 ↔ (𝐴↑2) = 1))
16 zre 9230 . . . . . . 7 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
1716ad2antrr 488 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℝ)
18 absresq 11055 . . . . . 6 (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
1917, 18syl 14 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((abs‘𝐴)↑2) = (𝐴↑2))
20 sq1 10583 . . . . . 6 (1↑2) = 1
2120a1i 9 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (1↑2) = 1)
2219, 21eqeq12d 2190 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔ (𝐴↑2) = 1))
2317recnd 7960 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℂ)
2423abscld 11158 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (abs‘𝐴) ∈ ℝ)
2523absge0d 11161 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ≤ (abs‘𝐴))
26 1re 7931 . . . . . 6 1 ∈ ℝ
27 0le1 8412 . . . . . 6 0 ≤ 1
28 sq11 10562 . . . . . 6 ((((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
2926, 27, 28mpanr12 439 . . . . 5 (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
3024, 25, 29syl2anc 411 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
3115, 22, 303bitr2d 216 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) ≠ 0 ↔ (abs‘𝐴) = 1))
32 oveq2 5873 . . . . 5 (𝑁 = 0 → (𝐴 /L 𝑁) = (𝐴 /L 0))
33 lgs0 13985 . . . . . 6 (𝐴 ∈ ℤ → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))
3433adantr 276 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))
3532, 34sylan9eqr 2230 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 /L 𝑁) = if((𝐴↑2) = 1, 1, 0))
3635neeq1d 2363 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ if((𝐴↑2) = 1, 1, 0) ≠ 0))
37 oveq2 5873 . . . . 5 (𝑁 = 0 → (𝐴 gcd 𝑁) = (𝐴 gcd 0))
38 gcdid0 11948 . . . . . 6 (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
3938adantr 276 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 gcd 0) = (abs‘𝐴))
4037, 39sylan9eqr 2230 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 gcd 𝑁) = (abs‘𝐴))
4140eqeq1d 2184 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 gcd 𝑁) = 1 ↔ (abs‘𝐴) = 1))
4231, 36, 413bitr4d 220 . 2 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
43 lgscl 13986 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
4443adantr 276 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) ∈ ℤ)
45 0z 9237 . . . 4 0 ∈ ℤ
46 zapne 9300 . . . 4 (((𝐴 /L 𝑁) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝐴 /L 𝑁) # 0 ↔ (𝐴 /L 𝑁) ≠ 0))
4744, 45, 46sylancl 413 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) # 0 ↔ (𝐴 /L 𝑁) ≠ 0))
48 eqid 2175 . . . . . . 7 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
4948lgsval4 13992 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
5049breq1d 4008 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) # 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) # 0))
51 simpr 110 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 < 0 ∧ 𝐴 < 0)) → (𝑁 < 0 ∧ 𝐴 < 0))
5251iftrued 3539 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 < 0 ∧ 𝐴 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = -1)
53 neg1ne0 8999 . . . . . . . . . . . 12 -1 ≠ 0
5453a1i 9 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 < 0 ∧ 𝐴 < 0)) → -1 ≠ 0)
5552, 54eqnetrd 2369 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 < 0 ∧ 𝐴 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0)
56 simpr 110 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑁 < 0 ∧ 𝐴 < 0)) → ¬ (𝑁 < 0 ∧ 𝐴 < 0))
5756iffalsed 3542 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑁 < 0 ∧ 𝐴 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = 1)
5811a1i 9 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑁 < 0 ∧ 𝐴 < 0)) → 1 ≠ 0)
5957, 58eqnetrd 2369 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑁 < 0 ∧ 𝐴 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0)
60 simpr 110 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
61 zdclt 9303 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
6260, 45, 61sylancl 413 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 < 0)
63 simpl 109 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℤ)
64 zdclt 9303 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐴 < 0)
6563, 45, 64sylancl 413 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝐴 < 0)
66 dcan2 934 . . . . . . . . . . . 12 (DECID 𝑁 < 0 → (DECID 𝐴 < 0 → DECID (𝑁 < 0 ∧ 𝐴 < 0)))
6762, 65, 66sylc 62 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑁 < 0 ∧ 𝐴 < 0))
68 exmiddc 836 . . . . . . . . . . 11 (DECID (𝑁 < 0 ∧ 𝐴 < 0) → ((𝑁 < 0 ∧ 𝐴 < 0) ∨ ¬ (𝑁 < 0 ∧ 𝐴 < 0)))
6967, 68syl 14 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 < 0 ∧ 𝐴 < 0) ∨ ¬ (𝑁 < 0 ∧ 𝐴 < 0)))
7055, 59, 69mpjaodan 798 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0)
7170biantrurd 305 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)))
72713adant3 1017 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)))
73 neg1z 9258 . . . . . . . . . . . . 13 -1 ∈ ℤ
7473a1i 9 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → -1 ∈ ℤ)
75 1zzd 9253 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 1 ∈ ℤ)
7674, 75, 67ifcldcd 3567 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
77763adant3 1017 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
7877zcnd 9349 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
79 nnuz 9536 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
80 1zzd 9253 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 1 ∈ ℤ)
8148lgsfcl3 13993 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
8281ffvelcdmda 5643 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
83 zmulcl 9279 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑘 · 𝑥) ∈ ℤ)
8483adantl 277 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝑘 · 𝑥) ∈ ℤ)
8579, 80, 82, 84seqf 10431 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))):ℕ⟶ℤ)
86 nnabscl 11077 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
87863adant1 1015 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
8885, 87ffvelcdmd 5644 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℤ)
8988zcnd 9349 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
9078, 89mulap0bd 8587 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 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))
91 zapne 9300 . . . . . . . . . 10 ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ ∧ 0 ∈ ℤ) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) # 0 ↔ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0))
9277, 45, 91sylancl 413 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) # 0 ↔ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0))
93 zapne 9300 . . . . . . . . . 10 (((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℤ ∧ 0 ∈ ℤ) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
9488, 45, 93sylancl 413 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
9592, 94anbi12d 473 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) # 0 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0) ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)))
9677, 88zmulcld 9354 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ∈ ℤ)
97 zapne 9300 . . . . . . . . 9 (((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ∈ ℤ ∧ 0 ∈ ℤ) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) # 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0))
9896, 45, 97sylancl 413 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) # 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0))
9990, 95, 983bitr3d 218 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 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))
10072, 99bitr2d 189 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
101100, 98, 943bitr4d 220 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) # 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0))
102 gcd2n0cl 11937 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℕ)
103102nnzd 9347 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℤ)
104 zdceq 9301 . . . . . . . . 9 (((𝐴 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 gcd 𝑁) = 1)
105103, 3, 104sylancl 413 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → DECID (𝐴 gcd 𝑁) = 1)
106 eluz2b3 9577 . . . . . . . . . . . . 13 ((𝐴 gcd 𝑁) ∈ (ℤ‘2) ↔ ((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1))
107 exprmfct 12105 . . . . . . . . . . . . 13 ((𝐴 gcd 𝑁) ∈ (ℤ‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁))
108106, 107sylbir 135 . . . . . . . . . . . 12 (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁))
109 mulcl 7913 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ)
110109adantl 277 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
11181ad2antrr 488 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (ℤ‘1)) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
112 elnnuz 9537 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ‘1))
113112biimpri 133 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ‘1) → 𝑘 ∈ ℕ)
114113adantl 277 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (ℤ‘1)) → 𝑘 ∈ ℕ)
115111, 114ffvelcdmd 5644 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (ℤ‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
116115zcnd 9349 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (ℤ‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
117 mul02 8318 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℂ → (0 · 𝑘) = 0)
118117adantl 277 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (0 · 𝑘) = 0)
119 mul01 8320 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℂ → (𝑘 · 0) = 0)
120119adantl 277 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) = 0)
121 simprr 531 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (𝐴 gcd 𝑁))
122 prmz 12078 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
123122ad2antrl 490 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℤ)
124 simpl1 1000 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝐴 ∈ ℤ)
125 simpl2 1001 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℤ)
126 dvdsgcdb 11981 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝𝐴𝑝𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
127123, 124, 125, 126syl3anc 1238 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝𝐴𝑝𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
128121, 127mpbird 167 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝𝐴𝑝𝑁))
129128simprd 114 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝𝑁)
130 dvdsabsb 11785 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑝𝑁𝑝 ∥ (abs‘𝑁)))
131123, 125, 130syl2anc 411 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝𝑁𝑝 ∥ (abs‘𝑁)))
132129, 131mpbid 147 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (abs‘𝑁))
13387adantr 276 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℕ)
134 dvdsle 11817 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℤ ∧ (abs‘𝑁) ∈ ℕ) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁)))
135123, 133, 134syl2anc 411 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁)))
136132, 135mpd 13 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ≤ (abs‘𝑁))
137 prmnn 12077 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
138137ad2antrl 490 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℕ)
139138, 79eleqtrdi 2268 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (ℤ‘1))
140133nnzd 9347 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℤ)
141 elfz5 9987 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ (ℤ‘1) ∧ (abs‘𝑁) ∈ ℤ) → (𝑝 ∈ (1...(abs‘𝑁)) ↔ 𝑝 ≤ (abs‘𝑁)))
142139, 140, 141syl2anc 411 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∈ (1...(abs‘𝑁)) ↔ 𝑝 ≤ (abs‘𝑁)))
143136, 142mpbird 167 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (1...(abs‘𝑁)))
144 eleq1w 2236 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
145 oveq2 5873 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑝 → (𝐴 /L 𝑛) = (𝐴 /L 𝑝))
146 oveq1 5872 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑝 → (𝑛 pCnt 𝑁) = (𝑝 pCnt 𝑁))
147145, 146oveq12d 5883 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑝 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)))
148144, 147ifbieq1d 3554 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
149 simprl 529 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℙ)
150149iftrued 3539 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)))
151 lgscl 13986 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝐴 /L 𝑝) ∈ ℤ)
152124, 123, 151syl2anc 411 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 𝑝) ∈ ℤ)
153 simpl3 1002 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ≠ 0)
154 pczcl 12265 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑝 pCnt 𝑁) ∈ ℕ0)
155149, 125, 153, 154syl12anc 1236 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt 𝑁) ∈ ℕ0)
156 zexpcl 10505 . . . . . . . . . . . . . . . . . 18 (((𝐴 /L 𝑝) ∈ ℤ ∧ (𝑝 pCnt 𝑁) ∈ ℕ0) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) ∈ ℤ)
157152, 155, 156syl2anc 411 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) ∈ ℤ)
158150, 157eqeltrd 2252 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) ∈ ℤ)
15948, 148, 138, 158fvmptd3 5601 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
160 oveq2 5873 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 2 → (𝐴 /L 𝑝) = (𝐴 /L 2))
161 lgs2 13989 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ ℤ → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
162124, 161syl 14 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
163160, 162sylan9eqr 2230 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /L 𝑝) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
164 simpr 110 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 𝑝 = 2)
165128simpld 112 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝𝐴)
166165adantr 276 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 𝑝𝐴)
167164, 166eqbrtrrd 4022 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 2 ∥ 𝐴)
168167iftrued 3539 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = 0)
169163, 168eqtrd 2208 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /L 𝑝) = 0)
170 simpll1 1036 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝐴 ∈ ℤ)
171149adantr 276 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℙ)
172 simpr 110 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ≠ 2)
173 eldifsn 3716 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ (ℙ ∖ {2}) ↔ (𝑝 ∈ ℙ ∧ 𝑝 ≠ 2))
174171, 172, 173sylanbrc 417 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℙ ∖ {2}))
175 lgsval3 13990 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (ℙ ∖ {2})) → (𝐴 /L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1))
176170, 174, 175syl2anc 411 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1))
177 oddprm 12226 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ (ℙ ∖ {2}) → ((𝑝 − 1) / 2) ∈ ℕ)
178174, 177syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ)
179178nnnn0d 9202 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ0)
180 zexpcl 10505 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℤ ∧ ((𝑝 − 1) / 2) ∈ ℕ0) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
181170, 179, 180syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
182 zq 9599 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴↑((𝑝 − 1) / 2)) ∈ ℤ → (𝐴↑((𝑝 − 1) / 2)) ∈ ℚ)
183181, 182syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℚ)
184 zq 9599 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ ℤ → 0 ∈ ℚ)
18545, 184mp1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℚ)
186 1nn 8903 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℕ
187 nnq 9606 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℕ → 1 ∈ ℚ)
188186, 187mp1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 ∈ ℚ)
189171, 137syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℕ)
190 nnq 9606 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 ∈ ℕ → 𝑝 ∈ ℚ)
191189, 190syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℚ)
192 nngt0 8917 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 ∈ ℕ → 0 < 𝑝)
193189, 192syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 < 𝑝)
194 0zd 9238 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℤ)
195165adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝𝐴)
196 dvdsval3 11766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝑝𝐴 ↔ (𝐴 mod 𝑝) = 0))
197189, 170, 196syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝𝐴 ↔ (𝐴 mod 𝑝) = 0))
198195, 197mpbid 147 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = 0)
199 q0mod 10325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ ℚ ∧ 0 < 𝑝) → (0 mod 𝑝) = 0)
200190, 192, 199syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ℕ → (0 mod 𝑝) = 0)
201189, 200syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0 mod 𝑝) = 0)
202198, 201eqtr4d 2211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = (0 mod 𝑝))
203170, 194, 179, 191, 193, 202modqexp 10616 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝))
2041780expd 10639 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0↑((𝑝 − 1) / 2)) = 0)
205204oveq1d 5880 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((0↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
206203, 205eqtrd 2208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
207183, 185, 188, 191, 193, 206modqadd1 10331 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝))
208 0p1e1 9006 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 + 1) = 1
209208oveq1i 5875 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 + 1) mod 𝑝) = (1 mod 𝑝)
210207, 209eqtrdi 2224 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = (1 mod 𝑝))
211 prmuz2 12098 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
212171, 211syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℤ‘2))
213 eluzelz 9510 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 ∈ (ℤ‘2) → 𝑝 ∈ ℤ)
214 zq 9599 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 ∈ ℤ → 𝑝 ∈ ℚ)
215213, 214syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ (ℤ‘2) → 𝑝 ∈ ℚ)
216 eluz2gt1 9575 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ (ℤ‘2) → 1 < 𝑝)
217 q1mod 10326 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ ℚ ∧ 1 < 𝑝) → (1 mod 𝑝) = 1)
218215, 216, 217syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 ∈ (ℤ‘2) → (1 mod 𝑝) = 1)
219212, 218syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (1 mod 𝑝) = 1)
220210, 219eqtrd 2208 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = 1)
221220oveq1d 5880 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = (1 − 1))
222 1m1e0 8961 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
223221, 222eqtrdi 2224 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = 0)
224176, 223eqtrd 2208 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /L 𝑝) = 0)
225 2z 9254 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℤ
226 zdceq 9301 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑝 = 2)
227123, 225, 226sylancl 413 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → DECID 𝑝 = 2)
228 dcne 2356 . . . . . . . . . . . . . . . . . . 19 (DECID 𝑝 = 2 ↔ (𝑝 = 2 ∨ 𝑝 ≠ 2))
229227, 228sylib 122 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 = 2 ∨ 𝑝 ≠ 2))
230169, 224, 229mpjaodan 798 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 𝑝) = 0)
231230oveq1d 5880 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) = (0↑(𝑝 pCnt 𝑁)))
232 zq 9599 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℤ → 𝑁 ∈ ℚ)
233125, 232syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℚ)
234 pcabs 12292 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
235149, 233, 234syl2anc 411 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
236 pcelnn 12287 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℙ ∧ (abs‘𝑁) ∈ ℕ) → ((𝑝 pCnt (abs‘𝑁)) ∈ ℕ ↔ 𝑝 ∥ (abs‘𝑁)))
237149, 133, 236syl2anc 411 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝 pCnt (abs‘𝑁)) ∈ ℕ ↔ 𝑝 ∥ (abs‘𝑁)))
238132, 237mpbird 167 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) ∈ ℕ)
239235, 238eqeltrrd 2253 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt 𝑁) ∈ ℕ)
2402390expd 10639 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (0↑(𝑝 pCnt 𝑁)) = 0)
241231, 240eqtrd 2208 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) = 0)
242159, 150, 2413eqtrd 2212 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = 0)
243110, 116, 118, 120, 143, 242seq3z 10481 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)
244243rexlimdvaa 2593 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
245108, 244syl5 32 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
246102, 245mpand 429 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 gcd 𝑁) ≠ 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
247246a1d 22 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (DECID (𝐴 gcd 𝑁) = 1 → ((𝐴 gcd 𝑁) ≠ 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)))
248247necon1ddc 2423 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (DECID (𝐴 gcd 𝑁) = 1 → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 → (𝐴 gcd 𝑁) = 1)))
249105, 248mpd 13 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 → (𝐴 gcd 𝑁) = 1))
25094, 249sylbid 150 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0 → (𝐴 gcd 𝑁) = 1))
251 1zzd 9253 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → 1 ∈ ℤ)
252 eleq1w 2236 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
253 oveq2 5873 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘))
254 oveq1 5872 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
255253, 254oveq12d 5883 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))
256252, 255ifbieq1d 3554 . . . . . . . . . . . 12 (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
257 simpr 110 . . . . . . . . . . . 12 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
258 simp1 997 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ)
259258ad3antrrr 492 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
260 prmz 12078 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
261260adantl 277 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
262 lgscl 13986 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈ ℤ)
263259, 261, 262syl2anc 411 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℤ)
264 simpr 110 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
265 simp2 998 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ)
266265ad3antrrr 492 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
267 simp3 999 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0)
268267ad3antrrr 492 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
269 pczcl 12265 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ0)
270264, 266, 268, 269syl12anc 1236 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ0)
271 zexpcl 10505 . . . . . . . . . . . . . 14 (((𝐴 /L 𝑘) ∈ ℤ ∧ (𝑘 pCnt 𝑁) ∈ ℕ0) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
272263, 270, 271syl2anc 411 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
273 1zzd 9253 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
274 prmdc 12097 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
275274adantl 277 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → DECID 𝑘 ∈ ℙ)
276272, 273, 275ifcldadc 3561 . . . . . . . . . . . 12 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ ℤ)
27748, 256, 257, 276fvmptd3 5601 . . . . . . . . . . 11 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
278 simpll1 1036 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
279260adantl 277 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
280278, 279, 262syl2anc 411 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℤ)
281280zcnd 9349 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℂ)
282281adantr 276 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 𝑘) ∈ ℂ)
283 oveq2 5873 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 2 → (𝐴 /L 𝑘) = (𝐴 /L 2))
284278adantr 276 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → 𝐴 ∈ ℤ)
285284, 161syl 14 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
286283, 285sylan9eqr 2230 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
287 nprmdvds1 12107 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 1)
288287adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ 1)
289 simpll2 1037 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
290 dvdsgcdb 11981 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘𝐴𝑘𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
291279, 278, 289, 290syl3anc 1238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘𝐴𝑘𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
292 simplr 528 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 gcd 𝑁) = 1)
293292breq2d 4010 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ (𝐴 gcd 𝑁) ↔ 𝑘 ∥ 1))
294291, 293bitrd 188 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘𝐴𝑘𝑁) ↔ 𝑘 ∥ 1))
295288, 294mtbird 673 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ (𝑘𝐴𝑘𝑁))
296 imnan 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝐴 → ¬ 𝑘𝑁) ↔ ¬ (𝑘𝐴𝑘𝑁))
297295, 296sylibr 134 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘𝐴 → ¬ 𝑘𝑁))
298297con2d 624 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘𝑁 → ¬ 𝑘𝐴))
299298imp 124 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → ¬ 𝑘𝐴)
300 breq1 4001 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 2 → (𝑘𝐴 ↔ 2 ∥ 𝐴))
301300notbid 667 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 2 → (¬ 𝑘𝐴 ↔ ¬ 2 ∥ 𝐴))
302299, 301syl5ibcom 155 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝑘 = 2 → ¬ 2 ∥ 𝐴))
303302imp 124 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → ¬ 2 ∥ 𝐴)
304303iffalsed 3542 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
305286, 304eqtrd 2208 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
306 simpr 110 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℤ ∧ (𝐴 mod 8) ∈ {1, 7}) → (𝐴 mod 8) ∈ {1, 7})
307306iftrued 3539 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ (𝐴 mod 8) ∈ {1, 7}) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) = 1)
30811a1i 9 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ (𝐴 mod 8) ∈ {1, 7}) → 1 ≠ 0)
309307, 308eqnetrd 2369 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ (𝐴 mod 8) ∈ {1, 7}) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0)
310 simpr 110 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℤ ∧ ¬ (𝐴 mod 8) ∈ {1, 7}) → ¬ (𝐴 mod 8) ∈ {1, 7})
311310iffalsed 3542 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ ¬ (𝐴 mod 8) ∈ {1, 7}) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) = -1)
31253a1i 9 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ ¬ (𝐴 mod 8) ∈ {1, 7}) → -1 ≠ 0)
313311, 312eqnetrd 2369 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ ¬ (𝐴 mod 8) ∈ {1, 7}) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0)
314 8nn 9059 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 8 ∈ ℕ
315 zmodcl 10314 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℤ ∧ 8 ∈ ℕ) → (𝐴 mod 8) ∈ ℕ0)
316314, 315mpan2 425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℕ0)
317316nn0zd 9346 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℤ)
318 zdceq 9301 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
319317, 3, 318sylancl 413 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 1)
320 7nn 9058 . . . . . . . . . . . . . . . . . . . . . . . . . 26 7 ∈ ℕ
321320nnzi 9247 . . . . . . . . . . . . . . . . . . . . . . . . 25 7 ∈ ℤ
322 zdceq 9301 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 mod 8) ∈ ℤ ∧ 7 ∈ ℤ) → DECID (𝐴 mod 8) = 7)
323317, 321, 322sylancl 413 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 7)
324 dcor 935 . . . . . . . . . . . . . . . . . . . . . . . 24 (DECID (𝐴 mod 8) = 1 → (DECID (𝐴 mod 8) = 7 → DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
325319, 323, 324sylc 62 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ ℤ → DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7))
326 elprg 3609 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 mod 8) ∈ ℕ0 → ((𝐴 mod 8) ∈ {1, 7} ↔ ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
327316, 326syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ ℤ → ((𝐴 mod 8) ∈ {1, 7} ↔ ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
328327dcbid 838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ ℤ → (DECID (𝐴 mod 8) ∈ {1, 7} ↔ DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
329325, 328mpbird 167 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ ℤ → DECID (𝐴 mod 8) ∈ {1, 7})
330 exmiddc 836 . . . . . . . . . . . . . . . . . . . . . 22 (DECID (𝐴 mod 8) ∈ {1, 7} → ((𝐴 mod 8) ∈ {1, 7} ∨ ¬ (𝐴 mod 8) ∈ {1, 7}))
331329, 330syl 14 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ ℤ → ((𝐴 mod 8) ∈ {1, 7} ∨ ¬ (𝐴 mod 8) ∈ {1, 7}))
332309, 313, 331mpjaodan 798 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℤ → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0)
333258, 332syl 14 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0)
334333ad4antr 494 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0)
335305, 334eqnetrd 2369 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) ≠ 0)
336 simpr 110 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
337336ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℙ)
338337, 287syl 14 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ 1)
339 simplr 528 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘𝑁)
340337, 260syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℤ)
341284adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℤ)
342 simpr 110 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ≠ 2)
343 eldifsn 3716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ (ℙ ∖ {2}) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ≠ 2))
344337, 342, 343sylanbrc 417 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ (ℙ ∖ {2}))
345 oddprm 12226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ (ℙ ∖ {2}) → ((𝑘 − 1) / 2) ∈ ℕ)
346344, 345syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ)
347346nnnn0d 9202 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ0)
348 zexpcl 10505 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈ ℕ0) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
349341, 347, 348syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
350289ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑁 ∈ ℤ)
351 dvdsgcd 11980 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℤ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
352340, 349, 350, 351syl3anc 1238 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
353339, 352mpan2d 428 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
354341zcnd 9349 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℂ)
355354, 347absexpd 11169 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (abs‘(𝐴↑((𝑘 − 1) / 2))) = ((abs‘𝐴)↑((𝑘 − 1) / 2)))
356355oveq1d 5880 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)))
357 gcdabs 11956 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))
358349, 350, 357syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))
359 gcdabs 11956 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝐴) gcd (abs‘𝑁)) = (𝐴 gcd 𝑁))
360341, 350, 359syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = (𝐴 gcd 𝑁))
361292ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴 gcd 𝑁) = 1)
362360, 361eqtrd 2208 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = 1)
363299adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘𝐴)
364 dvds0 11781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ℤ → 𝑘 ∥ 0)
365340, 364syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∥ 0)
366 breq2 4002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐴 = 0 → (𝑘𝐴𝑘 ∥ 0))
367365, 366syl5ibrcom 157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴 = 0 → 𝑘𝐴))
368367necon3bd 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘𝐴𝐴 ≠ 0))
369363, 368mpd 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ≠ 0)
370 nnabscl 11077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
371341, 369, 370syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝐴) ∈ ℕ)
372 simpll3 1038 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
373289, 372, 86syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (abs‘𝑁) ∈ ℕ)
374373ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝑁) ∈ ℕ)
375 rplpwr 11995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((abs‘𝐴) ∈ ℕ ∧ (abs‘𝑁) ∈ ℕ ∧ ((𝑘 − 1) / 2) ∈ ℕ) → (((abs‘𝐴) gcd (abs‘𝑁)) = 1 → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1))
376371, 374, 346, 375syl3anc 1238 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (((abs‘𝐴) gcd (abs‘𝑁)) = 1 → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1))
377362, 376mpd 13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1)
378356, 358, 3773eqtr3d 2216 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) = 1)
379378breq2d 4010 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) ↔ 𝑘 ∥ 1))
380353, 379sylibd 149 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) → 𝑘 ∥ 1))
381338, 380mtod 663 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)))
382 prmnn 12077 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
383382adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℕ)
384383ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℕ)
385 dvdsval3 11766 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) = 0))
386384, 349, 385syl2anc 411 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) = 0))
387386necon3bbid 2385 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) ≠ 0))
388381, 387mpbid 147 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) ≠ 0)
389 lgsvalmod 13991 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℤ ∧ 𝑘 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘))
390341, 344, 389syl2anc 411 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘))
391 nnq 9606 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 𝑘 ∈ ℚ)
392 nngt0 8917 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 0 < 𝑘)
393 q0mod 10325 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℚ ∧ 0 < 𝑘) → (0 mod 𝑘) = 0)
394391, 392, 393syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → (0 mod 𝑘) = 0)
395384, 394syl 14 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (0 mod 𝑘) = 0)
396388, 390, 3953netr4d 2378 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /L 𝑘) mod 𝑘) ≠ (0 mod 𝑘))
397 oveq1 5872 . . . . . . . . . . . . . . . . . . 19 ((𝐴 /L 𝑘) = 0 → ((𝐴 /L 𝑘) mod 𝑘) = (0 mod 𝑘))
398397necon3i 2393 . . . . . . . . . . . . . . . . . 18 (((𝐴 /L 𝑘) mod 𝑘) ≠ (0 mod 𝑘) → (𝐴 /L 𝑘) ≠ 0)
399396, 398syl 14 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴 /L 𝑘) ≠ 0)
400279adantr 276 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → 𝑘 ∈ ℤ)
401 zdceq 9301 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑘 = 2)
402400, 225, 401sylancl 413 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → DECID 𝑘 = 2)
403 dcne 2356 . . . . . . . . . . . . . . . . . 18 (DECID 𝑘 = 2 ↔ (𝑘 = 2 ∨ 𝑘 ≠ 2))
404402, 403sylib 122 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝑘 = 2 ∨ 𝑘 ≠ 2))
405335, 399, 404mpjaodan 798 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 𝑘) ≠ 0)
406280adantr 276 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 𝑘) ∈ ℤ)
407 zapne 9300 . . . . . . . . . . . . . . . . 17 (((𝐴 /L 𝑘) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝐴 /L 𝑘) # 0 ↔ (𝐴 /L 𝑘) ≠ 0))
408406, 45, 407sylancl 413 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → ((𝐴 /L 𝑘) # 0 ↔ (𝐴 /L 𝑘) ≠ 0))
409405, 408mpbird 167 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 𝑘) # 0)
410336, 289, 372, 269syl12anc 1236 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ0)
411410nn0zd 9346 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℤ)
412411adantr 276 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝑘 pCnt 𝑁) ∈ ℤ)
413 expclzaplem 10514 . . . . . . . . . . . . . . 15 (((𝐴 /L 𝑘) ∈ ℂ ∧ (𝐴 /L 𝑘) # 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
414282, 409, 412, 413syl3anc 1238 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
415 dvdsabsb 11785 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘𝑁𝑘 ∥ (abs‘𝑁)))
416279, 289, 415syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘𝑁𝑘 ∥ (abs‘𝑁)))
417416notbid 667 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (¬ 𝑘𝑁 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
418 pceq0 12288 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℙ ∧ (abs‘𝑁) ∈ ℕ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
419336, 373, 418syl2anc 411 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
420289, 232syl 14 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℚ)
421 pcabs 12292 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
422336, 420, 421syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
423422eqeq1d 2184 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ (𝑘 pCnt 𝑁) = 0))
424417, 419, 4233bitr2rd 217 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt 𝑁) = 0 ↔ ¬ 𝑘𝑁))
425424biimpar 297 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → (𝑘 pCnt 𝑁) = 0)
426425oveq2d 5881 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑0))
427281adantr 276 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → (𝐴 /L 𝑘) ∈ ℂ)
428427exp0d 10617 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑0) = 1)
429426, 428eqtrd 2208 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) = 1)
430 ax-1cn 7879 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
431 1ap0 8521 . . . . . . . . . . . . . . . 16 1 # 0
432 breq1 4001 . . . . . . . . . . . . . . . . 17 (𝑥 = 1 → (𝑥 # 0 ↔ 1 # 0))
433432elrab 2891 . . . . . . . . . . . . . . . 16 (1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (1 ∈ ℂ ∧ 1 # 0))
434430, 431, 433mpbir2an 942 . . . . . . . . . . . . . . 15 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}
435429, 434eqeltrdi 2266 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
436 dvdsdc 11773 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑁 ∈ ℤ) → DECID 𝑘𝑁)
437383, 289, 436syl2anc 411 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → DECID 𝑘𝑁)
438 exmiddc 836 . . . . . . . . . . . . . . 15 (DECID 𝑘𝑁 → (𝑘𝑁 ∨ ¬ 𝑘𝑁))
439437, 438syl 14 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘𝑁 ∨ ¬ 𝑘𝑁))
440414, 435, 439mpjaodan 798 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
441440adantlr 477 . . . . . . . . . . . 12 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
442434a1i 9 . . . . . . . . . . . 12 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
443441, 442, 275ifcldadc 3561 . . . . . . . . . . 11 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
444277, 443eqeltrd 2252 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
445 breq1 4001 . . . . . . . . . . . . . 14 (𝑥 = 𝑘 → (𝑥 # 0 ↔ 𝑘 # 0))
446445elrab 2891 . . . . . . . . . . . . 13 (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (𝑘 ∈ ℂ ∧ 𝑘 # 0))
447 breq1 4001 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 # 0 ↔ 𝑦 # 0))
448447elrab 2891 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (𝑦 ∈ ℂ ∧ 𝑦 # 0))
449 mulcl 7913 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑘 · 𝑦) ∈ ℂ)
450449ad2ant2r 509 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℂ ∧ 𝑘 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑘 · 𝑦) ∈ ℂ)
451 mulap0 8584 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℂ ∧ 𝑘 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑘 · 𝑦) # 0)
452450, 451jca 306 . . . . . . . . . . . . 13 (((𝑘 ∈ ℂ ∧ 𝑘 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) # 0))
453446, 448, 452syl2anb 291 . . . . . . . . . . . 12 ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) # 0))
454 breq1 4001 . . . . . . . . . . . . 13 (𝑥 = (𝑘 · 𝑦) → (𝑥 # 0 ↔ (𝑘 · 𝑦) # 0))
455454elrab 2891 . . . . . . . . . . . 12 ((𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) # 0))
456453, 455sylibr 134 . . . . . . . . . . 11 ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
457456adantl 277 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
45879, 251, 444, 457seqf 10431 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))):ℕ⟶{𝑥 ∈ ℂ ∣ 𝑥 # 0})
45987adantr 276 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (abs‘𝑁) ∈ ℕ)
460458, 459ffvelcdmd 5644 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
461 breq1 4001 . . . . . . . . . 10 (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) → (𝑥 # 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0))
462461elrab 2891 . . . . . . . . 9 ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0))
463462simprbi 275 . . . . . . . 8 ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0)
464460, 463syl 14 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0)
465464ex 115 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 gcd 𝑁) = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0))
466250, 465impbid 129 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0 ↔ (𝐴 gcd 𝑁) = 1))
46750, 101, 4663bitrd 214 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) # 0 ↔ (𝐴 gcd 𝑁) = 1))
4684673expa 1203 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) # 0 ↔ (𝐴 gcd 𝑁) = 1))
46947, 468bitr3d 190 . 2 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
470 zdceq 9301 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
47160, 45, 470sylancl 413 . . 3 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 = 0)
472 dcne 2356 . . 3 (DECID 𝑁 = 0 ↔ (𝑁 = 0 ∨ 𝑁 ≠ 0))
473471, 472sylib 122 . 2 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ∨ 𝑁 ≠ 0))
47442, 469, 473mpjaodan 798 1 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834  w3a 978   = wceq 1353  wcel 2146  wne 2345  wrex 2454  {crab 2457  cdif 3124  ifcif 3532  {csn 3589  {cpr 3590   class class class wbr 3998  cmpt 4059  wf 5204  cfv 5208  (class class class)co 5865  cc 7784  cr 7785  0cc0 7786  1c1 7787   + caddc 7789   · cmul 7791   < clt 7966  cle 7967  cmin 8102  -cneg 8103   # cap 8512   / cdiv 8602  cn 8892  2c2 8943  7c7 8948  8c8 8949  0cn0 9149  cz 9226  cuz 9501  cq 9592  ...cfz 9979   mod cmo 10292  seqcseq 10415  cexp 10489  abscabs 10974  cdvds 11762   gcd cgcd 11910  cprime 12074   pCnt cpc 12251   /L clgs 13969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581  ax-cnex 7877  ax-resscn 7878  ax-1cn 7879  ax-1re 7880  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-mulrcl 7885  ax-addcom 7886  ax-mulcom 7887  ax-addass 7888  ax-mulass 7889  ax-distr 7890  ax-i2m1 7891  ax-0lt1 7892  ax-1rid 7893  ax-0id 7894  ax-rnegex 7895  ax-precex 7896  ax-cnre 7897  ax-pre-ltirr 7898  ax-pre-ltwlin 7899  ax-pre-lttrn 7900  ax-pre-apti 7901  ax-pre-ltadd 7902  ax-pre-mulgt0 7903  ax-pre-mulext 7904  ax-arch 7905  ax-caucvg 7906
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-xor 1376  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-reu 2460  df-rmo 2461  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-if 3533  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-id 4287  df-po 4290  df-iso 4291  df-iord 4360  df-on 4362  df-ilim 4363  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-isom 5217  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-1st 6131  df-2nd 6132  df-recs 6296  df-irdg 6361  df-frec 6382  df-1o 6407  df-2o 6408  df-oadd 6411  df-er 6525  df-en 6731  df-dom 6732  df-fin 6733  df-sup 6973  df-inf 6974  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972  df-sub 8104  df-neg 8105  df-reap 8506  df-ap 8513  df-div 8603  df-inn 8893  df-2 8951  df-3 8952  df-4 8953  df-5 8954  df-6 8955  df-7 8956  df-8 8957  df-n0 9150  df-z 9227  df-uz 9502  df-q 9593  df-rp 9625  df-fz 9980  df-fzo 10113  df-fl 10240  df-mod 10293  df-seqfrec 10416  df-exp 10490  df-ihash 10724  df-cj 10819  df-re 10820  df-im 10821  df-rsqrt 10975  df-abs 10976  df-clim 11255  df-proddc 11527  df-dvds 11763  df-gcd 11911  df-prm 12075  df-phi 12178  df-pc 12252  df-lgs 13970
This theorem is referenced by:  lgsabs1  14011  lgsprme0  14014  lgsdirnn0  14019
  Copyright terms: Public domain W3C validator