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

Theorem lgsne0 14106
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 10576 . . . . . . . . 9 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
21adantr 276 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴↑2) ∈ ℤ)
3 1z 9268 . . . . . . . 8 1 ∈ ℤ
4 zdceq 9317 . . . . . . . 8 (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴↑2) = 1)
52, 3, 4sylancl 413 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐴↑2) = 1)
6 iffalse 3542 . . . . . . . . 9 (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0)
76a1i 9 . . . . . . . 8 (DECID (𝐴↑2) = 1 → (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0))
87necon1aidc 2398 . . . . . . 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 3539 . . . . . . 7 ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 1)
11 1ne0 8976 . . . . . . . 8 1 ≠ 0
1211a1i 9 . . . . . . 7 ((𝐴↑2) = 1 → 1 ≠ 0)
1310, 12eqnetrd 2371 . . . . . 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 9246 . . . . . . 7 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
1716ad2antrr 488 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℝ)
18 absresq 11071 . . . . . 6 (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
1917, 18syl 14 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((abs‘𝐴)↑2) = (𝐴↑2))
20 sq1 10599 . . . . . 6 (1↑2) = 1
2120a1i 9 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (1↑2) = 1)
2219, 21eqeq12d 2192 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔ (𝐴↑2) = 1))
2317recnd 7976 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℂ)
2423abscld 11174 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (abs‘𝐴) ∈ ℝ)
2523absge0d 11177 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ≤ (abs‘𝐴))
26 1re 7947 . . . . . 6 1 ∈ ℝ
27 0le1 8428 . . . . . 6 0 ≤ 1
28 sq11 10578 . . . . . 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 5877 . . . . 5 (𝑁 = 0 → (𝐴 /L 𝑁) = (𝐴 /L 0))
33 lgs0 14081 . . . . . 6 (𝐴 ∈ ℤ → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))
3433adantr 276 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))
3532, 34sylan9eqr 2232 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 /L 𝑁) = if((𝐴↑2) = 1, 1, 0))
3635neeq1d 2365 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ if((𝐴↑2) = 1, 1, 0) ≠ 0))
37 oveq2 5877 . . . . 5 (𝑁 = 0 → (𝐴 gcd 𝑁) = (𝐴 gcd 0))
38 gcdid0 11964 . . . . . 6 (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
3938adantr 276 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 gcd 0) = (abs‘𝐴))
4037, 39sylan9eqr 2232 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 gcd 𝑁) = (abs‘𝐴))
4140eqeq1d 2186 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 gcd 𝑁) = 1 ↔ (abs‘𝐴) = 1))
4231, 36, 413bitr4d 220 . 2 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
43 lgscl 14082 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
4443adantr 276 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) ∈ ℤ)
45 0z 9253 . . . 4 0 ∈ ℤ
46 zapne 9316 . . . 4 (((𝐴 /L 𝑁) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝐴 /L 𝑁) # 0 ↔ (𝐴 /L 𝑁) ≠ 0))
4744, 45, 46sylancl 413 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) # 0 ↔ (𝐴 /L 𝑁) ≠ 0))
48 eqid 2177 . . . . . . 7 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
4948lgsval4 14088 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
5049breq1d 4010 . . . . 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 3541 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 < 0 ∧ 𝐴 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = -1)
53 neg1ne0 9015 . . . . . . . . . . . 12 -1 ≠ 0
5453a1i 9 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 < 0 ∧ 𝐴 < 0)) → -1 ≠ 0)
5552, 54eqnetrd 2371 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 < 0 ∧ 𝐴 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0)
56 simpr 110 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑁 < 0 ∧ 𝐴 < 0)) → ¬ (𝑁 < 0 ∧ 𝐴 < 0))
5756iffalsed 3544 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑁 < 0 ∧ 𝐴 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = 1)
5811a1i 9 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑁 < 0 ∧ 𝐴 < 0)) → 1 ≠ 0)
5957, 58eqnetrd 2371 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑁 < 0 ∧ 𝐴 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0)
60 simpr 110 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
61 zdclt 9319 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
6260, 45, 61sylancl 413 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 < 0)
63 simpl 109 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℤ)
64 zdclt 9319 . . . . . . . . . . . . 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 9274 . . . . . . . . . . . . 13 -1 ∈ ℤ
7473a1i 9 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → -1 ∈ ℤ)
75 1zzd 9269 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 1 ∈ ℤ)
7674, 75, 67ifcldcd 3569 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
77763adant3 1017 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
7877zcnd 9365 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
79 nnuz 9552 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
80 1zzd 9269 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 1 ∈ ℤ)
8148lgsfcl3 14089 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
8281ffvelcdmda 5647 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
83 zmulcl 9295 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑘 · 𝑥) ∈ ℤ)
8483adantl 277 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝑘 · 𝑥) ∈ ℤ)
8579, 80, 82, 84seqf 10447 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))):ℕ⟶ℤ)
86 nnabscl 11093 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
87863adant1 1015 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
8885, 87ffvelcdmd 5648 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℤ)
8988zcnd 9365 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
9078, 89mulap0bd 8603 . . . . . . . 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 9316 . . . . . . . . . 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 9316 . . . . . . . . . 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 9370 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ∈ ℤ)
97 zapne 9316 . . . . . . . . 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 11953 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℕ)
103102nnzd 9363 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℤ)
104 zdceq 9317 . . . . . . . . 9 (((𝐴 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 gcd 𝑁) = 1)
105103, 3, 104sylancl 413 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → DECID (𝐴 gcd 𝑁) = 1)
106 eluz2b3 9593 . . . . . . . . . . . . 13 ((𝐴 gcd 𝑁) ∈ (ℤ‘2) ↔ ((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1))
107 exprmfct 12121 . . . . . . . . . . . . 13 ((𝐴 gcd 𝑁) ∈ (ℤ‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁))
108106, 107sylbir 135 . . . . . . . . . . . 12 (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁))
109 mulcl 7929 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ)
110109adantl 277 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
11181ad2antrr 488 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (ℤ‘1)) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
112 elnnuz 9553 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ‘1))
113112biimpri 133 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ‘1) → 𝑘 ∈ ℕ)
114113adantl 277 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (ℤ‘1)) → 𝑘 ∈ ℕ)
115111, 114ffvelcdmd 5648 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (ℤ‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
116115zcnd 9365 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (ℤ‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
117 mul02 8334 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℂ → (0 · 𝑘) = 0)
118117adantl 277 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (0 · 𝑘) = 0)
119 mul01 8336 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℂ → (𝑘 · 0) = 0)
120119adantl 277 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) = 0)
121 simprr 531 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (𝐴 gcd 𝑁))
122 prmz 12094 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
123122ad2antrl 490 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℤ)
124 simpl1 1000 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝐴 ∈ ℤ)
125 simpl2 1001 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℤ)
126 dvdsgcdb 11997 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝𝐴𝑝𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
127123, 124, 125, 126syl3anc 1238 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝𝐴𝑝𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
128121, 127mpbird 167 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝𝐴𝑝𝑁))
129128simprd 114 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝𝑁)
130 dvdsabsb 11801 . . . . . . . . . . . . . . . . . 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 11833 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℤ ∧ (abs‘𝑁) ∈ ℕ) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁)))
135123, 133, 134syl2anc 411 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁)))
136132, 135mpd 13 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ≤ (abs‘𝑁))
137 prmnn 12093 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
138137ad2antrl 490 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℕ)
139138, 79eleqtrdi 2270 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (ℤ‘1))
140133nnzd 9363 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℤ)
141 elfz5 10003 . . . . . . . . . . . . . . . 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 2238 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
145 oveq2 5877 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑝 → (𝐴 /L 𝑛) = (𝐴 /L 𝑝))
146 oveq1 5876 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑝 → (𝑛 pCnt 𝑁) = (𝑝 pCnt 𝑁))
147145, 146oveq12d 5887 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑝 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)))
148144, 147ifbieq1d 3556 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
149 simprl 529 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℙ)
150149iftrued 3541 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)))
151 lgscl 14082 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝐴 /L 𝑝) ∈ ℤ)
152124, 123, 151syl2anc 411 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 𝑝) ∈ ℤ)
153 simpl3 1002 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ≠ 0)
154 pczcl 12281 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑝 pCnt 𝑁) ∈ ℕ0)
155149, 125, 153, 154syl12anc 1236 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt 𝑁) ∈ ℕ0)
156 zexpcl 10521 . . . . . . . . . . . . . . . . . 18 (((𝐴 /L 𝑝) ∈ ℤ ∧ (𝑝 pCnt 𝑁) ∈ ℕ0) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) ∈ ℤ)
157152, 155, 156syl2anc 411 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) ∈ ℤ)
158150, 157eqeltrd 2254 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) ∈ ℤ)
15948, 148, 138, 158fvmptd3 5605 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
160 oveq2 5877 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 2 → (𝐴 /L 𝑝) = (𝐴 /L 2))
161 lgs2 14085 . . . . . . . . . . . . . . . . . . . . 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 2232 . . . . . . . . . . . . . . . . . . 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 4024 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 2 ∥ 𝐴)
168167iftrued 3541 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = 0)
169163, 168eqtrd 2210 . . . . . . . . . . . . . . . . . 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 3718 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ (ℙ ∖ {2}) ↔ (𝑝 ∈ ℙ ∧ 𝑝 ≠ 2))
174171, 172, 173sylanbrc 417 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℙ ∖ {2}))
175 lgsval3 14086 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (ℙ ∖ {2})) → (𝐴 /L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1))
176170, 174, 175syl2anc 411 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1))
177 oddprm 12242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ (ℙ ∖ {2}) → ((𝑝 − 1) / 2) ∈ ℕ)
178174, 177syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ)
179178nnnn0d 9218 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ0)
180 zexpcl 10521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℤ ∧ ((𝑝 − 1) / 2) ∈ ℕ0) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
181170, 179, 180syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
182 zq 9615 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴↑((𝑝 − 1) / 2)) ∈ ℤ → (𝐴↑((𝑝 − 1) / 2)) ∈ ℚ)
183181, 182syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℚ)
184 zq 9615 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ ℤ → 0 ∈ ℚ)
18545, 184mp1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℚ)
186 1nn 8919 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℕ
187 nnq 9622 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℕ → 1 ∈ ℚ)
188186, 187mp1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 ∈ ℚ)
189171, 137syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℕ)
190 nnq 9622 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 ∈ ℕ → 𝑝 ∈ ℚ)
191189, 190syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℚ)
192 nngt0 8933 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 ∈ ℕ → 0 < 𝑝)
193189, 192syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 < 𝑝)
194 0zd 9254 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℤ)
195165adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝𝐴)
196 dvdsval3 11782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝑝𝐴 ↔ (𝐴 mod 𝑝) = 0))
197189, 170, 196syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝𝐴 ↔ (𝐴 mod 𝑝) = 0))
198195, 197mpbid 147 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = 0)
199 q0mod 10341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2213 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = (0 mod 𝑝))
203170, 194, 179, 191, 193, 202modqexp 10632 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝))
2041780expd 10655 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0↑((𝑝 − 1) / 2)) = 0)
205204oveq1d 5884 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((0↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
206203, 205eqtrd 2210 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
207183, 185, 188, 191, 193, 206modqadd1 10347 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝))
208 0p1e1 9022 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 + 1) = 1
209208oveq1i 5879 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 + 1) mod 𝑝) = (1 mod 𝑝)
210207, 209eqtrdi 2226 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = (1 mod 𝑝))
211 prmuz2 12114 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
212171, 211syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℤ‘2))
213 eluzelz 9526 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 ∈ (ℤ‘2) → 𝑝 ∈ ℤ)
214 zq 9615 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 ∈ ℤ → 𝑝 ∈ ℚ)
215213, 214syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ (ℤ‘2) → 𝑝 ∈ ℚ)
216 eluz2gt1 9591 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ (ℤ‘2) → 1 < 𝑝)
217 q1mod 10342 . . . . . . . . . . . . . . . . . . . . . . . 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 2210 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = 1)
221220oveq1d 5884 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = (1 − 1))
222 1m1e0 8977 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
223221, 222eqtrdi 2226 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = 0)
224176, 223eqtrd 2210 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /L 𝑝) = 0)
225 2z 9270 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℤ
226 zdceq 9317 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑝 = 2)
227123, 225, 226sylancl 413 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → DECID 𝑝 = 2)
228 dcne 2358 . . . . . . . . . . . . . . . . . . 19 (DECID 𝑝 = 2 ↔ (𝑝 = 2 ∨ 𝑝 ≠ 2))
229227, 228sylib 122 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 = 2 ∨ 𝑝 ≠ 2))
230169, 224, 229mpjaodan 798 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 𝑝) = 0)
231230oveq1d 5884 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) = (0↑(𝑝 pCnt 𝑁)))
232 zq 9615 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℤ → 𝑁 ∈ ℚ)
233125, 232syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℚ)
234 pcabs 12308 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
235149, 233, 234syl2anc 411 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
236 pcelnn 12303 . . . . . . . . . . . . . . . . . . . 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 2255 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt 𝑁) ∈ ℕ)
2402390expd 10655 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (0↑(𝑝 pCnt 𝑁)) = 0)
241231, 240eqtrd 2210 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) = 0)
242159, 150, 2413eqtrd 2214 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = 0)
243110, 116, 118, 120, 143, 242seq3z 10497 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)
244243rexlimdvaa 2595 . . . . . . . . . . . 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 2425 . . . . . . . 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 9269 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → 1 ∈ ℤ)
252 eleq1w 2238 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
253 oveq2 5877 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘))
254 oveq1 5876 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
255253, 254oveq12d 5887 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))
256252, 255ifbieq1d 3556 . . . . . . . . . . . 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 12094 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
261260adantl 277 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
262 lgscl 14082 . . . . . . . . . . . . . . 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 12281 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ0)
270264, 266, 268, 269syl12anc 1236 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ0)
271 zexpcl 10521 . . . . . . . . . . . . . 14 (((𝐴 /L 𝑘) ∈ ℤ ∧ (𝑘 pCnt 𝑁) ∈ ℕ0) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
272263, 270, 271syl2anc 411 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
273 1zzd 9269 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
274 prmdc 12113 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
275274adantl 277 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → DECID 𝑘 ∈ ℙ)
276272, 273, 275ifcldadc 3563 . . . . . . . . . . . 12 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ ℤ)
27748, 256, 257, 276fvmptd3 5605 . . . . . . . . . . 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 9365 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℂ)
282281adantr 276 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 𝑘) ∈ ℂ)
283 oveq2 5877 . . . . . . . . . . . . . . . . . . . 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 2232 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
287 nprmdvds1 12123 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 1)
288287adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ 1)
289 simpll2 1037 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
290 dvdsgcdb 11997 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘𝐴𝑘𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
291279, 278, 289, 290syl3anc 1238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘𝐴𝑘𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
292 simplr 528 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 gcd 𝑁) = 1)
293292breq2d 4012 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4003 . . . . . . . . . . . . . . . . . . . . . . 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 3544 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
305286, 304eqtrd 2210 . . . . . . . . . . . . . . . . . 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 3541 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ (𝐴 mod 8) ∈ {1, 7}) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) = 1)
30811a1i 9 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ (𝐴 mod 8) ∈ {1, 7}) → 1 ≠ 0)
309307, 308eqnetrd 2371 . . . . . . . . . . . . . . . . . . . . 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 3544 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ ¬ (𝐴 mod 8) ∈ {1, 7}) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) = -1)
31253a1i 9 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ ¬ (𝐴 mod 8) ∈ {1, 7}) → -1 ≠ 0)
313311, 312eqnetrd 2371 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ ¬ (𝐴 mod 8) ∈ {1, 7}) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0)
314 8nn 9075 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 8 ∈ ℕ
315 zmodcl 10330 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℤ ∧ 8 ∈ ℕ) → (𝐴 mod 8) ∈ ℕ0)
316314, 315mpan2 425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℕ0)
317316nn0zd 9362 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℤ)
318 zdceq 9317 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
319317, 3, 318sylancl 413 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 1)
320 7nn 9074 . . . . . . . . . . . . . . . . . . . . . . . . . 26 7 ∈ ℕ
321320nnzi 9263 . . . . . . . . . . . . . . . . . . . . . . . . 25 7 ∈ ℤ
322 zdceq 9317 . . . . . . . . . . . . . . . . . . . . . . . . 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 3611 . . . . . . . . . . . . . . . . . . . . . . . . 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 2371 . . . . . . . . . . . . . . . . 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 3718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ (ℙ ∖ {2}) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ≠ 2))
344337, 342, 343sylanbrc 417 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ (ℙ ∖ {2}))
345 oddprm 12242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ (ℙ ∖ {2}) → ((𝑘 − 1) / 2) ∈ ℕ)
346344, 345syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ)
347346nnnn0d 9218 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ0)
348 zexpcl 10521 . . . . . . . . . . . . . . . . . . . . . . . . 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 11996 . . . . . . . . . . . . . . . . . . . . . . . 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 9365 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℂ)
355354, 347absexpd 11185 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (abs‘(𝐴↑((𝑘 − 1) / 2))) = ((abs‘𝐴)↑((𝑘 − 1) / 2)))
356355oveq1d 5884 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)))
357 gcdabs 11972 . . . . . . . . . . . . . . . . . . . . . . . . 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 11972 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2210 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = 1)
363299adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘𝐴)
364 dvds0 11797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ℤ → 𝑘 ∥ 0)
365340, 364syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∥ 0)
366 breq2 4004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐴 = 0 → (𝑘𝐴𝑘 ∥ 0))
367365, 366syl5ibrcom 157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴 = 0 → 𝑘𝐴))
368367necon3bd 2390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘𝐴𝐴 ≠ 0))
369363, 368mpd 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ≠ 0)
370 nnabscl 11093 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12011 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2218 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) = 1)
379378breq2d 4012 . . . . . . . . . . . . . . . . . . . . . 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 12093 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
383382adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℕ)
384383ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℕ)
385 dvdsval3 11782 . . . . . . . . . . . . . . . . . . . . . 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 2387 . . . . . . . . . . . . . . . . . . . 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 14087 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℤ ∧ 𝑘 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘))
390341, 344, 389syl2anc 411 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘))
391 nnq 9622 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 𝑘 ∈ ℚ)
392 nngt0 8933 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 0 < 𝑘)
393 q0mod 10341 . . . . . . . . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /L 𝑘) mod 𝑘) ≠ (0 mod 𝑘))
397 oveq1 5876 . . . . . . . . . . . . . . . . . . 19 ((𝐴 /L 𝑘) = 0 → ((𝐴 /L 𝑘) mod 𝑘) = (0 mod 𝑘))
398397necon3i 2395 . . . . . . . . . . . . . . . . . 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 9317 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑘 = 2)
402400, 225, 401sylancl 413 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → DECID 𝑘 = 2)
403 dcne 2358 . . . . . . . . . . . . . . . . . 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 9316 . . . . . . . . . . . . . . . . 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 9362 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℤ)
412411adantr 276 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝑘 pCnt 𝑁) ∈ ℤ)
413 expclzaplem 10530 . . . . . . . . . . . . . . 15 (((𝐴 /L 𝑘) ∈ ℂ ∧ (𝐴 /L 𝑘) # 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
414282, 409, 412, 413syl3anc 1238 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
415 dvdsabsb 11801 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘𝑁𝑘 ∥ (abs‘𝑁)))
416279, 289, 415syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘𝑁𝑘 ∥ (abs‘𝑁)))
417416notbid 667 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (¬ 𝑘𝑁 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
418 pceq0 12304 . . . . . . . . . . . . . . . . . . . 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 12308 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
422336, 420, 421syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
423422eqeq1d 2186 . . . . . . . . . . . . . . . . . . 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 5885 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑0))
427281adantr 276 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → (𝐴 /L 𝑘) ∈ ℂ)
428427exp0d 10633 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑0) = 1)
429426, 428eqtrd 2210 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) = 1)
430 ax-1cn 7895 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
431 1ap0 8537 . . . . . . . . . . . . . . . 16 1 # 0
432 breq1 4003 . . . . . . . . . . . . . . . . 17 (𝑥 = 1 → (𝑥 # 0 ↔ 1 # 0))
433432elrab 2893 . . . . . . . . . . . . . . . 16 (1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (1 ∈ ℂ ∧ 1 # 0))
434430, 431, 433mpbir2an 942 . . . . . . . . . . . . . . 15 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}
435429, 434eqeltrdi 2268 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
436 dvdsdc 11789 . . . . . . . . . . . . . . . 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 3563 . . . . . . . . . . 11 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
444277, 443eqeltrd 2254 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
445 breq1 4003 . . . . . . . . . . . . . 14 (𝑥 = 𝑘 → (𝑥 # 0 ↔ 𝑘 # 0))
446445elrab 2893 . . . . . . . . . . . . 13 (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (𝑘 ∈ ℂ ∧ 𝑘 # 0))
447 breq1 4003 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 # 0 ↔ 𝑦 # 0))
448447elrab 2893 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (𝑦 ∈ ℂ ∧ 𝑦 # 0))
449 mulcl 7929 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑘 · 𝑦) ∈ ℂ)
450449ad2ant2r 509 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℂ ∧ 𝑘 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑘 · 𝑦) ∈ ℂ)
451 mulap0 8600 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℂ ∧ 𝑘 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑘 · 𝑦) # 0)
452450, 451jca 306 . . . . . . . . . . . . 13 (((𝑘 ∈ ℂ ∧ 𝑘 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) # 0))
453446, 448, 452syl2anb 291 . . . . . . . . . . . 12 ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) # 0))
454 breq1 4003 . . . . . . . . . . . . 13 (𝑥 = (𝑘 · 𝑦) → (𝑥 # 0 ↔ (𝑘 · 𝑦) # 0))
455454elrab 2893 . . . . . . . . . . . 12 ((𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) # 0))
456453, 455sylibr 134 . . . . . . . . . . 11 ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
457456adantl 277 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
45879, 251, 444, 457seqf 10447 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))):ℕ⟶{𝑥 ∈ ℂ ∣ 𝑥 # 0})
45987adantr 276 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (abs‘𝑁) ∈ ℕ)
460458, 459ffvelcdmd 5648 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0})
461 breq1 4003 . . . . . . . . . 10 (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) → (𝑥 # 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) # 0))
462461elrab 2893 . . . . . . . . 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 9317 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
47160, 45, 470sylancl 413 . . 3 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 = 0)
472 dcne 2358 . . 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 2148  wne 2347  wrex 2456  {crab 2459  cdif 3126  ifcif 3534  {csn 3591  {cpr 3592   class class class wbr 4000  cmpt 4061  wf 5208  cfv 5212  (class class class)co 5869  cc 7800  cr 7801  0cc0 7802  1c1 7803   + caddc 7805   · cmul 7807   < clt 7982  cle 7983  cmin 8118  -cneg 8119   # cap 8528   / cdiv 8618  cn 8908  2c2 8959  7c7 8964  8c8 8965  0cn0 9165  cz 9242  cuz 9517  cq 9608  ...cfz 9995   mod cmo 10308  seqcseq 10431  cexp 10505  abscabs 10990  cdvds 11778   gcd cgcd 11926  cprime 12090   pCnt cpc 12267   /L clgs 14065
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920  ax-arch 7921  ax-caucvg 7922
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 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-isom 5221  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-frec 6386  df-1o 6411  df-2o 6412  df-oadd 6415  df-er 6529  df-en 6735  df-dom 6736  df-fin 6737  df-sup 6977  df-inf 6978  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-2 8967  df-3 8968  df-4 8969  df-5 8970  df-6 8971  df-7 8972  df-8 8973  df-n0 9166  df-z 9243  df-uz 9518  df-q 9609  df-rp 9641  df-fz 9996  df-fzo 10129  df-fl 10256  df-mod 10309  df-seqfrec 10432  df-exp 10506  df-ihash 10740  df-cj 10835  df-re 10836  df-im 10837  df-rsqrt 10991  df-abs 10992  df-clim 11271  df-proddc 11543  df-dvds 11779  df-gcd 11927  df-prm 12091  df-phi 12194  df-pc 12268  df-lgs 14066
This theorem is referenced by:  lgsabs1  14107  lgsprme0  14110  lgsdirnn0  14115
  Copyright terms: Public domain W3C validator