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

Theorem lgsne0 27380
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 iffalse 4533 . . . . . 6 (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0)
21necon1ai 2967 . . . . 5 (if((𝐴↑2) = 1, 1, 0) ≠ 0 → (𝐴↑2) = 1)
3 iftrue 4530 . . . . . 6 ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 1)
4 ax-1ne0 11225 . . . . . . 7 1 ≠ 0
54a1i 11 . . . . . 6 ((𝐴↑2) = 1 → 1 ≠ 0)
63, 5eqnetrd 3007 . . . . 5 ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) ≠ 0)
72, 6impbii 209 . . . 4 (if((𝐴↑2) = 1, 1, 0) ≠ 0 ↔ (𝐴↑2) = 1)
8 zre 12619 . . . . . . . 8 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
98ad2antrr 726 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℝ)
10 absresq 15342 . . . . . . 7 (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
119, 10syl 17 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((abs‘𝐴)↑2) = (𝐴↑2))
12 sq1 14235 . . . . . . 7 (1↑2) = 1
1312a1i 11 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (1↑2) = 1)
1411, 13eqeq12d 2752 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔ (𝐴↑2) = 1))
159recnd 11290 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℂ)
1615abscld 15476 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (abs‘𝐴) ∈ ℝ)
1715absge0d 15484 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ≤ (abs‘𝐴))
18 1re 11262 . . . . . . 7 1 ∈ ℝ
19 0le1 11787 . . . . . . 7 0 ≤ 1
20 sq11 14172 . . . . . . 7 ((((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
2118, 19, 20mpanr12 705 . . . . . 6 (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
2216, 17, 21syl2anc 584 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔ (abs‘𝐴) = 1))
2314, 22bitr3d 281 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ↔ (abs‘𝐴) = 1))
247, 23bitrid 283 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) ≠ 0 ↔ (abs‘𝐴) = 1))
25 oveq2 7440 . . . . 5 (𝑁 = 0 → (𝐴 /L 𝑁) = (𝐴 /L 0))
26 lgs0 27355 . . . . . 6 (𝐴 ∈ ℤ → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))
2726adantr 480 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))
2825, 27sylan9eqr 2798 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 /L 𝑁) = if((𝐴↑2) = 1, 1, 0))
2928neeq1d 2999 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ if((𝐴↑2) = 1, 1, 0) ≠ 0))
30 oveq2 7440 . . . . 5 (𝑁 = 0 → (𝐴 gcd 𝑁) = (𝐴 gcd 0))
31 gcdid0 16558 . . . . . 6 (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
3231adantr 480 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 gcd 0) = (abs‘𝐴))
3330, 32sylan9eqr 2798 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 gcd 𝑁) = (abs‘𝐴))
3433eqeq1d 2738 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 gcd 𝑁) = 1 ↔ (abs‘𝐴) = 1))
3524, 29, 343bitr4d 311 . 2 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
36 eqid 2736 . . . . . 6 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
3736lgsval4 27362 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
3837neeq1d 2999 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0))
39 neeq1 3002 . . . . . . 7 (-1 = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) → (-1 ≠ 0 ↔ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0))
40 neeq1 3002 . . . . . . 7 (1 = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) → (1 ≠ 0 ↔ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0))
41 neg1ne0 12383 . . . . . . 7 -1 ≠ 0
4239, 40, 41, 4keephyp 4596 . . . . . 6 if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0
4342biantrur 530 . . . . 5 ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
44 neg1cn 12381 . . . . . . . 8 -1 ∈ ℂ
45 ax-1cn 11214 . . . . . . . 8 1 ∈ ℂ
4644, 45ifcli 4572 . . . . . . 7 if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ
4746a1i 11 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
48 nnabscl 15365 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
49483adant1 1130 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
50 nnuz 12922 . . . . . . . 8 ℕ = (ℤ‘1)
5149, 50eleqtrdi 2850 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ (ℤ‘1))
5236lgsfcl3 27363 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
53 elfznn 13594 . . . . . . . . 9 (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ)
54 ffvelcdm 7100 . . . . . . . . 9 (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
5552, 53, 54syl2an 596 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
5655zcnd 12725 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
57 mulcl 11240 . . . . . . . 8 ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ)
5857adantl 481 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
5951, 56, 58seqcl 14064 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
6047, 59mulne0bd 11915 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0) ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0))
6143, 60bitr2id 284 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
62 gcd2n0cl 16547 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℕ)
63 eluz2b3 12965 . . . . . . . . 9 ((𝐴 gcd 𝑁) ∈ (ℤ‘2) ↔ ((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1))
64 exprmfct 16742 . . . . . . . . 9 ((𝐴 gcd 𝑁) ∈ (ℤ‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁))
6563, 64sylbir 235 . . . . . . . 8 (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁))
6657adantl 481 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
6756adantlr 715 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
68 mul02 11440 . . . . . . . . . . 11 (𝑘 ∈ ℂ → (0 · 𝑘) = 0)
6968adantl 481 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (0 · 𝑘) = 0)
70 mul01 11441 . . . . . . . . . . 11 (𝑘 ∈ ℂ → (𝑘 · 0) = 0)
7170adantl 481 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) = 0)
72 simprr 772 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (𝐴 gcd 𝑁))
73 prmz 16713 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
7473ad2antrl 728 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℤ)
75 simpl1 1191 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝐴 ∈ ℤ)
76 simpl2 1192 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℤ)
77 dvdsgcdb 16583 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝𝐴𝑝𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
7874, 75, 76, 77syl3anc 1372 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝𝐴𝑝𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁)))
7972, 78mpbird 257 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝𝐴𝑝𝑁))
8079simprd 495 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝𝑁)
81 dvdsabsb 16314 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑝𝑁𝑝 ∥ (abs‘𝑁)))
8274, 76, 81syl2anc 584 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝𝑁𝑝 ∥ (abs‘𝑁)))
8380, 82mpbid 232 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (abs‘𝑁))
8449adantr 480 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℕ)
85 dvdsle 16348 . . . . . . . . . . . . 13 ((𝑝 ∈ ℤ ∧ (abs‘𝑁) ∈ ℕ) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁)))
8674, 84, 85syl2anc 584 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁)))
8783, 86mpd 15 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ≤ (abs‘𝑁))
88 prmnn 16712 . . . . . . . . . . . . . 14 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
8988ad2antrl 728 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℕ)
9089, 50eleqtrdi 2850 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (ℤ‘1))
9184nnzd 12642 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℤ)
92 elfz5 13557 . . . . . . . . . . . 12 ((𝑝 ∈ (ℤ‘1) ∧ (abs‘𝑁) ∈ ℤ) → (𝑝 ∈ (1...(abs‘𝑁)) ↔ 𝑝 ≤ (abs‘𝑁)))
9390, 91, 92syl2anc 584 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∈ (1...(abs‘𝑁)) ↔ 𝑝 ≤ (abs‘𝑁)))
9487, 93mpbird 257 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (1...(abs‘𝑁)))
95 eleq1w 2823 . . . . . . . . . . . . . 14 (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
96 oveq2 7440 . . . . . . . . . . . . . . 15 (𝑛 = 𝑝 → (𝐴 /L 𝑛) = (𝐴 /L 𝑝))
97 oveq1 7439 . . . . . . . . . . . . . . 15 (𝑛 = 𝑝 → (𝑛 pCnt 𝑁) = (𝑝 pCnt 𝑁))
9896, 97oveq12d 7450 . . . . . . . . . . . . . 14 (𝑛 = 𝑝 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)))
9995, 98ifbieq1d 4549 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
100 ovex 7465 . . . . . . . . . . . . . 14 ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) ∈ V
101 1ex 11258 . . . . . . . . . . . . . 14 1 ∈ V
102100, 101ifex 4575 . . . . . . . . . . . . 13 if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) ∈ V
10399, 36, 102fvmpt 7015 . . . . . . . . . . . 12 (𝑝 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
10489, 103syl 17 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1))
105 iftrue 4530 . . . . . . . . . . . 12 (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)))
106105ad2antrl 728 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)))
107 oveq2 7440 . . . . . . . . . . . . . . . 16 (𝑝 = 2 → (𝐴 /L 𝑝) = (𝐴 /L 2))
108 lgs2 27359 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℤ → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
10975, 108syl 17 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
110107, 109sylan9eqr 2798 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /L 𝑝) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
111 simpr 484 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 𝑝 = 2)
11279simpld 494 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝𝐴)
113112adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 𝑝𝐴)
114111, 113eqbrtrrd 5166 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 2 ∥ 𝐴)
115114iftrued 4532 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = 0)
116110, 115eqtrd 2776 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /L 𝑝) = 0)
117 simpll1 1212 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝐴 ∈ ℤ)
118 simprl 770 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℙ)
119118adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℙ)
120 simpr 484 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ≠ 2)
121 eldifsn 4785 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ {2}) ↔ (𝑝 ∈ ℙ ∧ 𝑝 ≠ 2))
122119, 120, 121sylanbrc 583 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℙ ∖ {2}))
123 lgsval3 27360 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (ℙ ∖ {2})) → (𝐴 /L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1))
124117, 122, 123syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1))
125 oddprm 16849 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ (ℙ ∖ {2}) → ((𝑝 − 1) / 2) ∈ ℕ)
126122, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ)
127126nnnn0d 12589 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈ ℕ0)
128 zexpcl 14118 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ ((𝑝 − 1) / 2) ∈ ℕ0) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
129117, 127, 128syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℤ)
130129zred 12724 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈ ℝ)
131 0red 11265 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℝ)
13218a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 ∈ ℝ)
133119, 88syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℕ)
134133nnrpd 13076 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℝ+)
135 0zd 12627 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈ ℤ)
136112adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝𝐴)
137 dvdsval3 16295 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑝 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝑝𝐴 ↔ (𝐴 mod 𝑝) = 0))
138133, 117, 137syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝𝐴 ↔ (𝐴 mod 𝑝) = 0))
139136, 138mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = 0)
140 0mod 13943 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ ℝ+ → (0 mod 𝑝) = 0)
141134, 140syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0 mod 𝑝) = 0)
142139, 141eqtr4d 2779 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = (0 mod 𝑝))
143 modexp 14278 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (((𝑝 − 1) / 2) ∈ ℕ0𝑝 ∈ ℝ+) ∧ (𝐴 mod 𝑝) = (0 mod 𝑝)) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝))
144117, 135, 127, 134, 142, 143syl221anc 1382 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝))
1451260expd 14180 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0↑((𝑝 − 1) / 2)) = 0)
146145oveq1d 7447 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((0↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
147144, 146eqtrd 2776 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝))
148 modadd1 13949 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴↑((𝑝 − 1) / 2)) ∈ ℝ ∧ 0 ∈ ℝ) ∧ (1 ∈ ℝ ∧ 𝑝 ∈ ℝ+) ∧ ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝)) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝))
149130, 131, 132, 134, 147, 148syl221anc 1382 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝))
150 0p1e1 12389 . . . . . . . . . . . . . . . . . . . 20 (0 + 1) = 1
151150oveq1i 7442 . . . . . . . . . . . . . . . . . . 19 ((0 + 1) mod 𝑝) = (1 mod 𝑝)
152149, 151eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = (1 mod 𝑝))
153133nnred 12282 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℝ)
154 prmuz2 16734 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
155119, 154syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℤ‘2))
156 eluz2b2 12964 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ (ℤ‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝))
157155, 156sylib 218 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝 ∈ ℕ ∧ 1 < 𝑝))
158157simprd 495 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 < 𝑝)
159 1mod 13944 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ ℝ ∧ 1 < 𝑝) → (1 mod 𝑝) = 1)
160153, 158, 159syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (1 mod 𝑝) = 1)
161152, 160eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = 1)
162161oveq1d 7447 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = (1 − 1))
163 1m1e0 12339 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
164162, 163eqtrdi 2792 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = 0)
165124, 164eqtrd 2776 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /L 𝑝) = 0)
166116, 165pm2.61dane 3028 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 𝑝) = 0)
167166oveq1d 7447 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) = (0↑(𝑝 pCnt 𝑁)))
168 zq 12997 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℤ → 𝑁 ∈ ℚ)
16976, 168syl 17 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℚ)
170 pcabs 16914 . . . . . . . . . . . . . . 15 ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
171118, 169, 170syl2anc 584 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁))
172 pcelnn 16909 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℙ ∧ (abs‘𝑁) ∈ ℕ) → ((𝑝 pCnt (abs‘𝑁)) ∈ ℕ ↔ 𝑝 ∥ (abs‘𝑁)))
173118, 84, 172syl2anc 584 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝 pCnt (abs‘𝑁)) ∈ ℕ ↔ 𝑝 ∥ (abs‘𝑁)))
17483, 173mpbird 257 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) ∈ ℕ)
175171, 174eqeltrrd 2841 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt 𝑁) ∈ ℕ)
1761750expd 14180 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (0↑(𝑝 pCnt 𝑁)) = 0)
177167, 176eqtrd 2776 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) = 0)
178104, 106, 1773eqtrd 2780 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = 0)
17966, 67, 69, 71, 94, 84, 178seqz 14092 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)
180179rexlimdvaa 3155 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
18165, 180syl5 34 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
18262, 181mpand 695 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 gcd 𝑁) ≠ 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0))
183182necon1d 2961 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 → (𝐴 gcd 𝑁) = 1))
18451adantr 480 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (abs‘𝑁) ∈ (ℤ‘1))
18553adantl 481 . . . . . . . . . 10 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → 𝑘 ∈ ℕ)
186 eleq1w 2823 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
187 oveq2 7440 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘))
188 oveq1 7439 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
189187, 188oveq12d 7450 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))
190186, 189ifbieq1d 4549 . . . . . . . . . . 11 (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
191 ovex 7465 . . . . . . . . . . . 12 ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
192191, 101ifex 4575 . . . . . . . . . . 11 if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
193190, 36, 192fvmpt 7015 . . . . . . . . . 10 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
194185, 193syl 17 . . . . . . . . 9 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
195 simpll1 1212 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
196 prmz 16713 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
197196adantl 481 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
198 lgscl 27356 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈ ℤ)
199195, 197, 198syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℤ)
200199zcnd 12725 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℂ)
201200adantr 480 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 𝑘) ∈ ℂ)
202 oveq2 7440 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → (𝐴 /L 𝑘) = (𝐴 /L 2))
203195adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → 𝐴 ∈ ℤ)
204203, 108syl 17 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
205202, 204sylan9eqr 2798 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
206 nprmdvds1 16744 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 1)
207206adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ 1)
208 simpll2 1213 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
209 dvdsgcdb 16583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘𝐴𝑘𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
210197, 195, 208, 209syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘𝐴𝑘𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁)))
211 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 gcd 𝑁) = 1)
212211breq2d 5154 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ (𝐴 gcd 𝑁) ↔ 𝑘 ∥ 1))
213210, 212bitrd 279 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘𝐴𝑘𝑁) ↔ 𝑘 ∥ 1))
214207, 213mtbird 325 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ (𝑘𝐴𝑘𝑁))
215 imnan 399 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘𝐴 → ¬ 𝑘𝑁) ↔ ¬ (𝑘𝐴𝑘𝑁))
216214, 215sylibr 234 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘𝐴 → ¬ 𝑘𝑁))
217216con2d 134 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘𝑁 → ¬ 𝑘𝐴))
218217imp 406 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → ¬ 𝑘𝐴)
219 breq1 5145 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 2 → (𝑘𝐴 ↔ 2 ∥ 𝐴))
220219notbid 318 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (¬ 𝑘𝐴 ↔ ¬ 2 ∥ 𝐴))
221218, 220syl5ibcom 245 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝑘 = 2 → ¬ 2 ∥ 𝐴))
222221imp 406 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → ¬ 2 ∥ 𝐴)
223222iffalsed 4535 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
224205, 223eqtrd 2776 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
225 neeq1 3002 . . . . . . . . . . . . . . . . 17 (1 = if((𝐴 mod 8) ∈ {1, 7}, 1, -1) → (1 ≠ 0 ↔ if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0))
226 neeq1 3002 . . . . . . . . . . . . . . . . 17 (-1 = if((𝐴 mod 8) ∈ {1, 7}, 1, -1) → (-1 ≠ 0 ↔ if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0))
227225, 226, 4, 41keephyp 4596 . . . . . . . . . . . . . . . 16 if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0
228227a1i 11 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠ 0)
229224, 228eqnetrd 3007 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) ≠ 0)
230 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
231230ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℙ)
232231, 206syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ 1)
233 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘𝑁)
234231, 196syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℤ)
235203adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℤ)
236 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ≠ 2)
237 eldifsn 4785 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (ℙ ∖ {2}) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ≠ 2))
238231, 236, 237sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ (ℙ ∖ {2}))
239 oddprm 16849 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (ℙ ∖ {2}) → ((𝑘 − 1) / 2) ∈ ℕ)
240238, 239syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ)
241240nnnn0d 12589 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈ ℕ0)
242 zexpcl 14118 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈ ℕ0) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
243235, 241, 242syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
244208ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑁 ∈ ℤ)
245 dvdsgcd 16582 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℤ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
246234, 243, 244, 245syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
247233, 246mpan2d 694 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)))
248235zcnd 12725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℂ)
249248, 241absexpd 15492 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (abs‘(𝐴↑((𝑘 − 1) / 2))) = ((abs‘𝐴)↑((𝑘 − 1) / 2)))
250249oveq1d 7447 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)))
251 gcdabs 16569 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))
252243, 244, 251syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))
253 gcdabs 16569 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝐴) gcd (abs‘𝑁)) = (𝐴 gcd 𝑁))
254235, 244, 253syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = (𝐴 gcd 𝑁))
255211ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴 gcd 𝑁) = 1)
256254, 255eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = 1)
257218adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘𝐴)
258 dvds0 16310 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ ℤ → 𝑘 ∥ 0)
259234, 258syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∥ 0)
260 breq2 5146 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 = 0 → (𝑘𝐴𝑘 ∥ 0))
261259, 260syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴 = 0 → 𝑘𝐴))
262261necon3bd 2953 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘𝐴𝐴 ≠ 0))
263257, 262mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ≠ 0)
264 nnabscl 15365 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
265235, 263, 264syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝐴) ∈ ℕ)
266 simpll3 1214 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
267208, 266, 48syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (abs‘𝑁) ∈ ℕ)
268267ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝑁) ∈ ℕ)
269 rplpwr 16596 . . . . . . . . . . . . . . . . . . . . . . 23 (((abs‘𝐴) ∈ ℕ ∧ (abs‘𝑁) ∈ ℕ ∧ ((𝑘 − 1) / 2) ∈ ℕ) → (((abs‘𝐴) gcd (abs‘𝑁)) = 1 → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1))
270265, 268, 240, 269syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (((abs‘𝐴) gcd (abs‘𝑁)) = 1 → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1))
271256, 270mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1)
272250, 252, 2713eqtr3d 2784 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) = 1)
273272breq2d 5154 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) ↔ 𝑘 ∥ 1))
274247, 273sylibd 239 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) → 𝑘 ∥ 1))
275232, 274mtod 198 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)))
276 prmnn 16712 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
277276adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℕ)
278277ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℕ)
279 dvdsval3 16295 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) = 0))
280278, 243, 279syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) = 0))
281280necon3bbid 2977 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) ≠ 0))
282275, 281mpbid 232 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) ≠ 0)
283 lgsvalmod 27361 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝑘 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘))
284235, 238, 283syl2anc 584 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘))
285278nnrpd 13076 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℝ+)
286 0mod 13943 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℝ+ → (0 mod 𝑘) = 0)
287285, 286syl 17 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (0 mod 𝑘) = 0)
288282, 284, 2873netr4d 3017 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /L 𝑘) mod 𝑘) ≠ (0 mod 𝑘))
289 oveq1 7439 . . . . . . . . . . . . . . . 16 ((𝐴 /L 𝑘) = 0 → ((𝐴 /L 𝑘) mod 𝑘) = (0 mod 𝑘))
290289necon3i 2972 . . . . . . . . . . . . . . 15 (((𝐴 /L 𝑘) mod 𝑘) ≠ (0 mod 𝑘) → (𝐴 /L 𝑘) ≠ 0)
291288, 290syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) ∧ 𝑘 ≠ 2) → (𝐴 /L 𝑘) ≠ 0)
292229, 291pm2.61dane 3028 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝐴 /L 𝑘) ≠ 0)
293 pczcl 16887 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ0)
294230, 208, 266, 293syl12anc 836 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ0)
295294nn0zd 12641 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℤ)
296295adantr 480 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → (𝑘 pCnt 𝑁) ∈ ℤ)
297 neeq1 3002 . . . . . . . . . . . . . 14 (𝑥 = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) → (𝑥 ≠ 0 ↔ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0))
298 expclz 14126 . . . . . . . . . . . . . 14 (((𝐴 /L 𝑘) ∈ ℂ ∧ (𝐴 /L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℂ)
299 expne0i 14136 . . . . . . . . . . . . . 14 (((𝐴 /L 𝑘) ∈ ℂ ∧ (𝐴 /L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0)
300297, 298, 299elrabd 3693 . . . . . . . . . . . . 13 (((𝐴 /L 𝑘) ∈ ℂ ∧ (𝐴 /L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
301201, 292, 296, 300syl3anc 1372 . . . . . . . . . . . 12 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
302 dvdsabsb 16314 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘𝑁𝑘 ∥ (abs‘𝑁)))
303197, 208, 302syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘𝑁𝑘 ∥ (abs‘𝑁)))
304303notbid 318 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (¬ 𝑘𝑁 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
305 pceq0 16910 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℙ ∧ (abs‘𝑁) ∈ ℕ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
306230, 267, 305syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑁)))
307208, 168syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℚ)
308 pcabs 16914 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
309230, 307, 308syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁))
310309eqeq1d 2738 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ (𝑘 pCnt 𝑁) = 0))
311304, 306, 3103bitr2rd 308 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt 𝑁) = 0 ↔ ¬ 𝑘𝑁))
312311biimpar 477 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → (𝑘 pCnt 𝑁) = 0)
313312oveq2d 7448 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑0))
314200adantr 480 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → (𝐴 /L 𝑘) ∈ ℂ)
315314exp0d 14181 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑0) = 1)
316313, 315eqtrd 2776 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) = 1)
317 neeq1 3002 . . . . . . . . . . . . . . 15 (𝑥 = 1 → (𝑥 ≠ 0 ↔ 1 ≠ 0))
318317elrab 3691 . . . . . . . . . . . . . 14 (1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (1 ∈ ℂ ∧ 1 ≠ 0))
31945, 4, 318mpbir2an 711 . . . . . . . . . . . . 13 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}
320316, 319eqeltrdi 2848 . . . . . . . . . . . 12 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
321301, 320pm2.61dan 812 . . . . . . . . . . 11 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
322319a1i 11 . . . . . . . . . . 11 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
323321, 322ifclda 4560 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
324323adantr 480 . . . . . . . . 9 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
325194, 324eqeltrd 2840 . . . . . . . 8 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
326 neeq1 3002 . . . . . . . . . . . 12 (𝑥 = 𝑘 → (𝑥 ≠ 0 ↔ 𝑘 ≠ 0))
327326elrab 3691 . . . . . . . . . . 11 (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
328 neeq1 3002 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 ≠ 0 ↔ 𝑦 ≠ 0))
329328elrab 3691 . . . . . . . . . . 11 (𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
330 mulcl 11240 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑘 · 𝑦) ∈ ℂ)
331330ad2ant2r 747 . . . . . . . . . . . 12 (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑘 · 𝑦) ∈ ℂ)
332 mulne0 11906 . . . . . . . . . . . 12 (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑘 · 𝑦) ≠ 0)
333331, 332jca 511 . . . . . . . . . . 11 (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0))
334327, 329, 333syl2anb 598 . . . . . . . . . 10 ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0))
335 neeq1 3002 . . . . . . . . . . 11 (𝑥 = (𝑘 · 𝑦) → (𝑥 ≠ 0 ↔ (𝑘 · 𝑦) ≠ 0))
336335elrab 3691 . . . . . . . . . 10 ((𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0))
337334, 336sylibr 234 . . . . . . . . 9 ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
338337adantl 481 . . . . . . . 8 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
339184, 325, 338seqcl 14064 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})
340 neeq1 3002 . . . . . . . . 9 (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) → (𝑥 ≠ 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
341340elrab 3691 . . . . . . . 8 ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
342341simprbi 496 . . . . . . 7 ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)
343339, 342syl 17 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)
344343ex 412 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 gcd 𝑁) = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0))
345183, 344impbid 212 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
34638, 61, 3453bitrd 305 . . 3 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
3473463expa 1118 . 2 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
34835, 347pm2.61dane 3028 1 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  wne 2939  wrex 3069  {crab 3435  cdif 3947  ifcif 4524  {csn 4625  {cpr 4627   class class class wbr 5142  cmpt 5224  wf 6556  cfv 6560  (class class class)co 7432  cc 11154  cr 11155  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161   < clt 11296  cle 11297  cmin 11493  -cneg 11494   / cdiv 11921  cn 12267  2c2 12322  7c7 12327  8c8 12328  0cn0 12528  cz 12615  cuz 12879  cq 12991  +crp 13035  ...cfz 13548   mod cmo 13910  seqcseq 14043  cexp 14103  abscabs 15274  cdvds 16291   gcd cgcd 16532  cprime 16709   pCnt cpc 16875   /L clgs 27339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-oadd 8511  df-er 8746  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-sup 9483  df-inf 9484  df-dju 9942  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-n0 12529  df-xnn0 12602  df-z 12616  df-uz 12880  df-q 12992  df-rp 13036  df-fz 13549  df-fzo 13696  df-fl 13833  df-mod 13911  df-seq 14044  df-exp 14104  df-hash 14371  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-dvds 16292  df-gcd 16533  df-prm 16710  df-phi 16804  df-pc 16876  df-lgs 27340
This theorem is referenced by:  lgsabs1  27381  lgsprme0  27384  lgsdirnn0  27389  lgsqr  27396  lgsdchr  27400  lgsquad3  27432  2lgsoddprm  27461
  Copyright terms: Public domain W3C validator