Step | Hyp | Ref
| Expression |
1 | | iffalse 4095 |
. . . . . 6
⊢ (¬
(𝐴↑2) = 1 →
if((𝐴↑2) = 1, 1, 0) =
0) |
2 | 1 | necon1ai 2821 |
. . . . 5
⊢
(if((𝐴↑2) = 1,
1, 0) ≠ 0 → (𝐴↑2) = 1) |
3 | | iftrue 4092 |
. . . . . 6
⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) =
1) |
4 | | ax-1ne0 10005 |
. . . . . . 7
⊢ 1 ≠
0 |
5 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐴↑2) = 1 → 1 ≠
0) |
6 | 3, 5 | eqnetrd 2861 |
. . . . 5
⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) ≠
0) |
7 | 2, 6 | impbii 199 |
. . . 4
⊢
(if((𝐴↑2) = 1,
1, 0) ≠ 0 ↔ (𝐴↑2) = 1) |
8 | | zre 11381 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
9 | 8 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℝ) |
10 | | absresq 14042 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
((abs‘𝐴)↑2) =
(𝐴↑2)) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((abs‘𝐴)↑2) = (𝐴↑2)) |
12 | | sq1 12958 |
. . . . . . 7
⊢
(1↑2) = 1 |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (1↑2) =
1) |
14 | 11, 13 | eqeq12d 2637 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔
(𝐴↑2) =
1)) |
15 | 9 | recnd 10068 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 𝐴 ∈ ℂ) |
16 | 15 | abscld 14175 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (abs‘𝐴) ∈
ℝ) |
17 | 15 | absge0d 14183 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ≤
(abs‘𝐴)) |
18 | | 1re 10039 |
. . . . . . 7
⊢ 1 ∈
ℝ |
19 | | 0le1 10551 |
. . . . . . 7
⊢ 0 ≤
1 |
20 | | sq11 12936 |
. . . . . . 7
⊢
((((abs‘𝐴)
∈ ℝ ∧ 0 ≤ (abs‘𝐴)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1))
→ (((abs‘𝐴)↑2) = (1↑2) ↔
(abs‘𝐴) =
1)) |
21 | 18, 19, 20 | mpanr12 721 |
. . . . . 6
⊢
(((abs‘𝐴)
∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (((abs‘𝐴)↑2) = (1↑2) ↔
(abs‘𝐴) =
1)) |
22 | 16, 17, 21 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (((abs‘𝐴)↑2) = (1↑2) ↔
(abs‘𝐴) =
1)) |
23 | 14, 22 | bitr3d 270 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ↔ (abs‘𝐴) = 1)) |
24 | 7, 23 | syl5bb 272 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) ≠ 0
↔ (abs‘𝐴) =
1)) |
25 | | oveq2 6658 |
. . . . 5
⊢ (𝑁 = 0 → (𝐴 /L 𝑁) = (𝐴 /L 0)) |
26 | | lgs0 25035 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 /L 0) =
if((𝐴↑2) = 1, 1,
0)) |
27 | 26 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 0) =
if((𝐴↑2) = 1, 1,
0)) |
28 | 25, 27 | sylan9eqr 2678 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 /L 𝑁) = if((𝐴↑2) = 1, 1, 0)) |
29 | 28 | neeq1d 2853 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ if((𝐴↑2) = 1, 1, 0) ≠
0)) |
30 | | oveq2 6658 |
. . . . 5
⊢ (𝑁 = 0 → (𝐴 gcd 𝑁) = (𝐴 gcd 0)) |
31 | | gcdid0 15241 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴)) |
32 | 31 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 gcd 0) = (abs‘𝐴)) |
33 | 30, 32 | sylan9eqr 2678 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴 gcd 𝑁) = (abs‘𝐴)) |
34 | 33 | eqeq1d 2624 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 gcd 𝑁) = 1 ↔ (abs‘𝐴) = 1)) |
35 | 24, 29, 34 | 3bitr4d 300 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1)) |
36 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
37 | 36 | lgsval4 25042 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
38 | 37 | neeq1d 2853 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0)) |
39 | | neeq1 2856 |
. . . . . . 7
⊢ (-1 =
if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) → (-1 ≠
0 ↔ if((𝑁 < 0 ∧
𝐴 < 0), -1, 1) ≠
0)) |
40 | | neeq1 2856 |
. . . . . . 7
⊢ (1 =
if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) → (1 ≠
0 ↔ if((𝑁 < 0 ∧
𝐴 < 0), -1, 1) ≠
0)) |
41 | | neg1ne0 11126 |
. . . . . . 7
⊢ -1 ≠
0 |
42 | 39, 40, 41, 4 | keephyp 4152 |
. . . . . 6
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 |
43 | 42 | biantrur 527 |
. . . . 5
⊢ ((seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, ((𝐴
/L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, ((𝐴
/L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)) |
44 | | neg1cn 11124 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
45 | | ax-1cn 9994 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
46 | 44, 45 | keepel 4155 |
. . . . . . 7
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ |
47 | 46 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ) |
48 | | nnabscl 14065 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
49 | 48 | 3adant1 1079 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
50 | | nnuz 11723 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
51 | 49, 50 | syl6eleq 2711 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
(ℤ≥‘1)) |
52 | 36 | lgsfcl3 25043 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
53 | | elfznn 12370 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ) |
54 | | ffvelrn 6357 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
55 | 52, 53, 54 | syl2an 494 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
56 | 55 | zcnd 11483 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
57 | | mulcl 10020 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
58 | 57 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
59 | 51, 56, 58 | seqcl 12821 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ) |
60 | 47, 59 | mulne0bd 10678 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ≠ 0 ∧ (seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, ((𝐴
/L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0) ↔ (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0)) |
61 | 43, 60 | syl5rbb 273 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) ≠ 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)) |
62 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝐴 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) |
63 | 62 | necon3ai 2819 |
. . . . . . . . 9
⊢ (𝑁 ≠ 0 → ¬ (𝐴 = 0 ∧ 𝑁 = 0)) |
64 | | gcdn0cl 15224 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝑁 = 0)) → (𝐴 gcd 𝑁) ∈ ℕ) |
65 | 63, 64 | sylan2 491 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℕ) |
66 | 65 | 3impa 1259 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 gcd 𝑁) ∈ ℕ) |
67 | | eluz2b3 11762 |
. . . . . . . . 9
⊢ ((𝐴 gcd 𝑁) ∈ (ℤ≥‘2)
↔ ((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1)) |
68 | | exprmfct 15416 |
. . . . . . . . 9
⊢ ((𝐴 gcd 𝑁) ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ (𝐴 gcd 𝑁)) |
69 | 67, 68 | sylbir 225 |
. . . . . . . 8
⊢ (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁)) |
70 | 57 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
71 | 56 | adantlr 751 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
72 | | mul02 10214 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℂ → (0
· 𝑘) =
0) |
73 | 72 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (0 · 𝑘) = 0) |
74 | | mul01 10215 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℂ → (𝑘 · 0) =
0) |
75 | 74 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) = 0) |
76 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (𝐴 gcd 𝑁)) |
77 | | prmz 15389 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
78 | 77 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℤ) |
79 | | simpl1 1064 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝐴 ∈ ℤ) |
80 | | simpl2 1065 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℤ) |
81 | | dvdsgcdb 15262 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁))) |
82 | 78, 79, 80, 81 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝐴 gcd 𝑁))) |
83 | 76, 82 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝑁)) |
84 | 83 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ 𝑁) |
85 | | dvdsabsb 15001 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑝 ∥ 𝑁 ↔ 𝑝 ∥ (abs‘𝑁))) |
86 | 78, 80, 85 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ 𝑁 ↔ 𝑝 ∥ (abs‘𝑁))) |
87 | 84, 86 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ (abs‘𝑁)) |
88 | 49 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℕ) |
89 | | dvdsle 15032 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℤ ∧
(abs‘𝑁) ∈
ℕ) → (𝑝 ∥
(abs‘𝑁) → 𝑝 ≤ (abs‘𝑁))) |
90 | 78, 88, 89 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∥ (abs‘𝑁) → 𝑝 ≤ (abs‘𝑁))) |
91 | 87, 90 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ≤ (abs‘𝑁)) |
92 | | prmnn 15388 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
93 | 92 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℕ) |
94 | 93, 50 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈
(ℤ≥‘1)) |
95 | 88 | nnzd 11481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (abs‘𝑁) ∈ ℤ) |
96 | | elfz5 12334 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
(ℤ≥‘1) ∧ (abs‘𝑁) ∈ ℤ) → (𝑝 ∈ (1...(abs‘𝑁)) ↔ 𝑝 ≤ (abs‘𝑁))) |
97 | 94, 95, 96 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 ∈ (1...(abs‘𝑁)) ↔ 𝑝 ≤ (abs‘𝑁))) |
98 | 91, 97 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ (1...(abs‘𝑁))) |
99 | | eleq1 2689 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ)) |
100 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑝 → (𝐴 /L 𝑛) = (𝐴 /L 𝑝)) |
101 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑁) = (𝑝 pCnt 𝑁)) |
102 | 100, 101 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑝 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁))) |
103 | 99, 102 | ifbieq1d 4109 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1)) |
104 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) ∈ V |
105 | | 1ex 10035 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
V |
106 | 104, 105 | ifex 4156 |
. . . . . . . . . . . . 13
⊢ if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) ∈ V |
107 | 103, 36, 106 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1)) |
108 | 93, 107 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1)) |
109 | | iftrue 4092 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁))) |
110 | 109 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → if(𝑝 ∈ ℙ, ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)), 1) = ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁))) |
111 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 2 → (𝐴 /L 𝑝) = (𝐴 /L 2)) |
112 | | lgs2 25039 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → (𝐴 /L 2) = if(2
∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1,
-1))) |
113 | 79, 112 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 2) = if(2 ∥
𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1,
-1))) |
114 | 111, 113 | sylan9eqr 2678 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /L 𝑝) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1,
-1))) |
115 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 𝑝 = 2) |
116 | 83 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∥ 𝐴) |
117 | 116 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 𝑝 ∥ 𝐴) |
118 | 115, 117 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → 2 ∥ 𝐴) |
119 | 118 | iftrued 4094 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) =
0) |
120 | 114, 119 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 = 2) → (𝐴 /L 𝑝) = 0) |
121 | | simpll1 1100 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝐴 ∈ ℤ) |
122 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑝 ∈ ℙ) |
123 | 122 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℙ) |
124 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ≠ 2) |
125 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ (ℙ ∖ {2})
↔ (𝑝 ∈ ℙ
∧ 𝑝 ≠
2)) |
126 | 123, 124,
125 | sylanbrc 698 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ (ℙ ∖
{2})) |
127 | | lgsval3 25040 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (ℙ ∖ {2}))
→ (𝐴
/L 𝑝) =
((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1)) |
128 | 121, 126,
127 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /L 𝑝) = ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1)) |
129 | | oddprm 15515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 ∈ (ℙ ∖ {2})
→ ((𝑝 − 1) / 2)
∈ ℕ) |
130 | 126, 129 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈
ℕ) |
131 | 130 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝑝 − 1) / 2) ∈
ℕ0) |
132 | | zexpcl 12875 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℤ ∧ ((𝑝 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑝 − 1) / 2)) ∈
ℤ) |
133 | 121, 131,
132 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈
ℤ) |
134 | 133 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴↑((𝑝 − 1) / 2)) ∈
ℝ) |
135 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈
ℝ) |
136 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 ∈
ℝ) |
137 | 123, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℕ) |
138 | 137 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℝ+) |
139 | | 0zd 11389 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 0 ∈
ℤ) |
140 | 116 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∥ 𝐴) |
141 | | dvdsval3 14987 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑝 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝑝 ∥ 𝐴 ↔ (𝐴 mod 𝑝) = 0)) |
142 | 137, 121,
141 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝 ∥ 𝐴 ↔ (𝐴 mod 𝑝) = 0)) |
143 | 140, 142 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = 0) |
144 | | 0mod 12701 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 ∈ ℝ+
→ (0 mod 𝑝) =
0) |
145 | 138, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0 mod 𝑝) = 0) |
146 | 143, 145 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 mod 𝑝) = (0 mod 𝑝)) |
147 | | modexp 12999 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℤ ∧ 0 ∈
ℤ) ∧ (((𝑝 −
1) / 2) ∈ ℕ0 ∧ 𝑝 ∈ ℝ+) ∧ (𝐴 mod 𝑝) = (0 mod 𝑝)) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝)) |
148 | 121, 139,
131, 138, 146, 147 | syl221anc 1337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = ((0↑((𝑝 − 1) / 2)) mod 𝑝)) |
149 | 130 | 0expd 13024 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (0↑((𝑝 − 1) / 2)) = 0) |
150 | 149 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((0↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝)) |
151 | 148, 150 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝)) |
152 | | modadd1 12707 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴↑((𝑝 − 1) / 2)) ∈ ℝ ∧ 0
∈ ℝ) ∧ (1 ∈ ℝ ∧ 𝑝 ∈ ℝ+) ∧ ((𝐴↑((𝑝 − 1) / 2)) mod 𝑝) = (0 mod 𝑝)) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝)) |
153 | 134, 135,
136, 138, 151, 152 | syl221anc 1337 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = ((0 + 1) mod 𝑝)) |
154 | | 0p1e1 11132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 + 1) =
1 |
155 | 154 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0 + 1)
mod 𝑝) = (1 mod 𝑝) |
156 | 153, 155 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = (1 mod 𝑝)) |
157 | 137 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈ ℝ) |
158 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
159 | 123, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 𝑝 ∈
(ℤ≥‘2)) |
160 | | eluz2b2 11761 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
161 | 159, 160 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
162 | 161 | simprd 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → 1 < 𝑝) |
163 | | 1mod 12702 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ ℝ ∧ 1 <
𝑝) → (1 mod 𝑝) = 1) |
164 | 157, 162,
163 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (1 mod 𝑝) = 1) |
165 | 156, 164 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) = 1) |
166 | 165 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = (1 −
1)) |
167 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
168 | 166, 167 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → ((((𝐴↑((𝑝 − 1) / 2)) + 1) mod 𝑝) − 1) = 0) |
169 | 128, 168 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) ∧ 𝑝 ≠ 2) → (𝐴 /L 𝑝) = 0) |
170 | 120, 169 | pm2.61dane 2881 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝐴 /L 𝑝) = 0) |
171 | 170 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) = (0↑(𝑝 pCnt 𝑁))) |
172 | | zq 11794 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℚ) |
173 | 80, 172 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → 𝑁 ∈ ℚ) |
174 | | pcabs 15579 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁)) |
175 | 122, 173,
174 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) = (𝑝 pCnt 𝑁)) |
176 | | pcelnn 15574 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℙ ∧
(abs‘𝑁) ∈
ℕ) → ((𝑝 pCnt
(abs‘𝑁)) ∈
ℕ ↔ 𝑝 ∥
(abs‘𝑁))) |
177 | 122, 88, 176 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑝 pCnt (abs‘𝑁)) ∈ ℕ ↔ 𝑝 ∥ (abs‘𝑁))) |
178 | 87, 177 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt (abs‘𝑁)) ∈ ℕ) |
179 | 175, 178 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (𝑝 pCnt 𝑁) ∈ ℕ) |
180 | 179 | 0expd 13024 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (0↑(𝑝 pCnt 𝑁)) = 0) |
181 | 171, 180 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝐴 /L 𝑝)↑(𝑝 pCnt 𝑁)) = 0) |
182 | 108, 110,
181 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑝) = 0) |
183 | 70, 71, 73, 75, 98, 88, 182 | seqz 12849 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐴 gcd 𝑁))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0) |
184 | 183 | rexlimdvaa 3032 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝑁) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)) |
185 | 69, 184 | syl5 34 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (((𝐴 gcd 𝑁) ∈ ℕ ∧ (𝐴 gcd 𝑁) ≠ 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)) |
186 | 66, 185 | mpand 711 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 gcd 𝑁) ≠ 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = 0)) |
187 | 186 | necon1d 2816 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 → (𝐴 gcd 𝑁) = 1)) |
188 | 51 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (abs‘𝑁) ∈
(ℤ≥‘1)) |
189 | 53 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → 𝑘 ∈ ℕ) |
190 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
191 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘)) |
192 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁)) |
193 | 191, 192 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
194 | 190, 193 | ifbieq1d 4109 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
195 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
196 | 195, 105 | ifex 4156 |
. . . . . . . . . . 11
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
197 | 194, 36, 196 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
198 | 189, 197 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
199 | | simpll1 1100 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ) |
200 | | prmz 15389 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℤ) |
201 | 200 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ) |
202 | | lgscl 25036 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈
ℤ) |
203 | 199, 201,
202 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℤ) |
204 | 203 | zcnd 11483 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℂ) |
205 | 204 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝐴 /L 𝑘) ∈ ℂ) |
206 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 2 → (𝐴 /L 𝑘) = (𝐴 /L 2)) |
207 | 199 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → 𝐴 ∈ ℤ) |
208 | 207, 112 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝐴 /L 2) = if(2 ∥
𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1,
-1))) |
209 | 206, 208 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1,
-1))) |
210 | | nprmdvds1 15418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ ℙ → ¬
𝑘 ∥
1) |
211 | 210 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ 1) |
212 | | simpll2 1101 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ) |
213 | | dvdsgcdb 15262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁))) |
214 | 201, 199,
212, 213 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁) ↔ 𝑘 ∥ (𝐴 gcd 𝑁))) |
215 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝐴 gcd 𝑁) = 1) |
216 | 215 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ (𝐴 gcd 𝑁) ↔ 𝑘 ∥ 1)) |
217 | 214, 216 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁) ↔ 𝑘 ∥ 1)) |
218 | 211, 217 | mtbird 315 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ¬ (𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁)) |
219 | | imnan 438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∥ 𝐴 → ¬ 𝑘 ∥ 𝑁) ↔ ¬ (𝑘 ∥ 𝐴 ∧ 𝑘 ∥ 𝑁)) |
220 | 218, 219 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ 𝐴 → ¬ 𝑘 ∥ 𝑁)) |
221 | 220 | con2d 129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ 𝑁 → ¬ 𝑘 ∥ 𝐴)) |
222 | 221 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → ¬ 𝑘 ∥ 𝐴) |
223 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 2 → (𝑘 ∥ 𝐴 ↔ 2 ∥ 𝐴)) |
224 | 223 | notbid 308 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 2 → (¬ 𝑘 ∥ 𝐴 ↔ ¬ 2 ∥ 𝐴)) |
225 | 222, 224 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝑘 = 2 → ¬ 2 ∥ 𝐴)) |
226 | 225 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → ¬ 2 ∥ 𝐴) |
227 | 226 | iffalsed 4097 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = if((𝐴 mod 8) ∈ {1, 7}, 1,
-1)) |
228 | 209, 227 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) = if((𝐴 mod 8) ∈ {1, 7}, 1,
-1)) |
229 | | neeq1 2856 |
. . . . . . . . . . . . . . . . 17
⊢ (1 =
if((𝐴 mod 8) ∈ {1, 7},
1, -1) → (1 ≠ 0 ↔ if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠
0)) |
230 | | neeq1 2856 |
. . . . . . . . . . . . . . . . 17
⊢ (-1 =
if((𝐴 mod 8) ∈ {1, 7},
1, -1) → (-1 ≠ 0 ↔ if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠
0)) |
231 | 229, 230,
4, 41 | keephyp 4152 |
. . . . . . . . . . . . . . . 16
⊢ if((𝐴 mod 8) ∈ {1, 7}, 1, -1)
≠ 0 |
232 | 231 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ≠
0) |
233 | 228, 232 | eqnetrd 2861 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 = 2) → (𝐴 /L 𝑘) ≠ 0) |
234 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ) |
235 | 234 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℙ) |
236 | 235, 210 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ 1) |
237 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∥ 𝑁) |
238 | 235, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℤ) |
239 | 207 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℤ) |
240 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ≠ 2) |
241 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (ℙ ∖ {2})
↔ (𝑘 ∈ ℙ
∧ 𝑘 ≠
2)) |
242 | 235, 240,
241 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ (ℙ ∖
{2})) |
243 | | oddprm 15515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ (ℙ ∖ {2})
→ ((𝑘 − 1) / 2)
∈ ℕ) |
244 | 242, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈
ℕ) |
245 | 244 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 − 1) / 2) ∈
ℕ0) |
246 | | zexpcl 12875 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑘 − 1) / 2)) ∈
ℤ) |
247 | 239, 245,
246 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴↑((𝑘 − 1) / 2)) ∈
ℤ) |
248 | 212 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑁 ∈ ℤ) |
249 | | dvdsgcd 15261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘 ∥ 𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))) |
250 | 238, 247,
248, 249 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ∧ 𝑘 ∥ 𝑁) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))) |
251 | 237, 250 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) → 𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁))) |
252 | 239 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ∈ ℂ) |
253 | 252, 245 | absexpd 14191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (abs‘(𝐴↑((𝑘 − 1) / 2))) = ((abs‘𝐴)↑((𝑘 − 1) / 2))) |
254 | 253 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁))) |
255 | | gcdabs 15250 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴↑((𝑘 − 1) / 2)) ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd
(abs‘𝑁)) = ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)) |
256 | 247, 248,
255 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘(𝐴↑((𝑘 − 1) / 2))) gcd (abs‘𝑁)) = ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁)) |
257 | | gcdabs 15250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝐴) gcd
(abs‘𝑁)) = (𝐴 gcd 𝑁)) |
258 | 239, 248,
257 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = (𝐴 gcd 𝑁)) |
259 | 215 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴 gcd 𝑁) = 1) |
260 | 258, 259 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((abs‘𝐴) gcd (abs‘𝑁)) = 1) |
261 | 222 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ 𝐴) |
262 | | dvds0 14997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ ℤ → 𝑘 ∥ 0) |
263 | 238, 262 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∥ 0) |
264 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 = 0 → (𝑘 ∥ 𝐴 ↔ 𝑘 ∥ 0)) |
265 | 263, 264 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴 = 0 → 𝑘 ∥ 𝐴)) |
266 | 265 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘 ∥ 𝐴 → 𝐴 ≠ 0)) |
267 | 261, 266 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝐴 ≠ 0) |
268 | | nnabscl 14065 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℕ) |
269 | 239, 267,
268 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝐴) ∈ ℕ) |
270 | | simpll3 1102 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0) |
271 | 212, 270,
48 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (abs‘𝑁) ∈
ℕ) |
272 | 271 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (abs‘𝑁) ∈ ℕ) |
273 | | rplpwr 15276 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((abs‘𝐴)
∈ ℕ ∧ (abs‘𝑁) ∈ ℕ ∧ ((𝑘 − 1) / 2) ∈ ℕ) →
(((abs‘𝐴) gcd
(abs‘𝑁)) = 1 →
(((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1)) |
274 | 269, 272,
244, 273 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (((abs‘𝐴) gcd (abs‘𝑁)) = 1 → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1)) |
275 | 260, 274 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (((abs‘𝐴)↑((𝑘 − 1) / 2)) gcd (abs‘𝑁)) = 1) |
276 | 254, 256,
275 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) = 1) |
277 | 276 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ ((𝐴↑((𝑘 − 1) / 2)) gcd 𝑁) ↔ 𝑘 ∥ 1)) |
278 | 251, 277 | sylibd 229 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) → 𝑘 ∥ 1)) |
279 | 236, 278 | mtod 189 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ¬ 𝑘 ∥ (𝐴↑((𝑘 − 1) / 2))) |
280 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℕ) |
281 | 280 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℕ) |
282 | 281 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℕ) |
283 | | dvdsval3 14987 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ) →
(𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) = 0)) |
284 | 282, 247,
283 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) = 0)) |
285 | 284 | necon3bbid 2831 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (¬ 𝑘 ∥ (𝐴↑((𝑘 − 1) / 2)) ↔ ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) ≠ 0)) |
286 | 279, 285 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘) ≠ 0) |
287 | | lgsvalmod 25041 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ (ℙ ∖ {2}))
→ ((𝐴
/L 𝑘) mod
𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘)) |
288 | 239, 242,
287 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /L 𝑘) mod 𝑘) = ((𝐴↑((𝑘 − 1) / 2)) mod 𝑘)) |
289 | 282 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → 𝑘 ∈ ℝ+) |
290 | | 0mod 12701 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℝ+
→ (0 mod 𝑘) =
0) |
291 | 289, 290 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (0 mod 𝑘) = 0) |
292 | 286, 288,
291 | 3netr4d 2871 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → ((𝐴 /L 𝑘) mod 𝑘) ≠ (0 mod 𝑘)) |
293 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 /L 𝑘) = 0 → ((𝐴 /L 𝑘) mod 𝑘) = (0 mod 𝑘)) |
294 | 293 | necon3i 2826 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 /L 𝑘) mod 𝑘) ≠ (0 mod 𝑘) → (𝐴 /L 𝑘) ≠ 0) |
295 | 292, 294 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) ∧ 𝑘 ≠ 2) → (𝐴 /L 𝑘) ≠ 0) |
296 | 233, 295 | pm2.61dane 2881 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝐴 /L 𝑘) ≠ 0) |
297 | | pczcl 15553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
298 | 234, 212,
270, 297 | syl12anc 1324 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
299 | 298 | nn0zd 11480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℤ) |
300 | 299 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → (𝑘 pCnt 𝑁) ∈ ℤ) |
301 | | expclz 12885 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 /L 𝑘) ∈ ℂ ∧ (𝐴 /L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℂ) |
302 | | expne0i 12892 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 /L 𝑘) ∈ ℂ ∧ (𝐴 /L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0) |
303 | | neeq1 2856 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) → (𝑥 ≠ 0 ↔ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0)) |
304 | 303 | elrab 3363 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℂ ∧ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ≠ 0)) |
305 | 301, 302,
304 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (((𝐴 /L 𝑘) ∈ ℂ ∧ (𝐴 /L 𝑘) ≠ 0 ∧ (𝑘 pCnt 𝑁) ∈ ℤ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
306 | 205, 296,
300, 305 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 ∥ 𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
307 | | dvdsabsb 15001 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∥ 𝑁 ↔ 𝑘 ∥ (abs‘𝑁))) |
308 | 201, 212,
307 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ 𝑁 ↔ 𝑘 ∥ (abs‘𝑁))) |
309 | 308 | notbid 308 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (¬ 𝑘 ∥ 𝑁 ↔ ¬ 𝑘 ∥ (abs‘𝑁))) |
310 | | pceq0 15575 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℙ ∧
(abs‘𝑁) ∈
ℕ) → ((𝑘 pCnt
(abs‘𝑁)) = 0 ↔
¬ 𝑘 ∥
(abs‘𝑁))) |
311 | 234, 271,
310 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑁))) |
312 | 212, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℚ) |
313 | | pcabs 15579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁)) |
314 | 234, 312,
313 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑁)) = (𝑘 pCnt 𝑁)) |
315 | 314 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑁)) = 0 ↔ (𝑘 pCnt 𝑁) = 0)) |
316 | 309, 311,
315 | 3bitr2rd 297 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt 𝑁) = 0 ↔ ¬ 𝑘 ∥ 𝑁)) |
317 | 316 | biimpar 502 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → (𝑘 pCnt 𝑁) = 0) |
318 | 317 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑0)) |
319 | 204 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → (𝐴 /L 𝑘) ∈ ℂ) |
320 | 319 | exp0d 13002 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /L 𝑘)↑0) = 1) |
321 | 318, 320 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) = 1) |
322 | | neeq1 2856 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → (𝑥 ≠ 0 ↔ 1 ≠ 0)) |
323 | 322 | elrab 3363 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
{𝑥 ∈ ℂ ∣
𝑥 ≠ 0} ↔ (1 ∈
ℂ ∧ 1 ≠ 0)) |
324 | 45, 4, 323 | mpbir2an 955 |
. . . . . . . . . . . . 13
⊢ 1 ∈
{𝑥 ∈ ℂ ∣
𝑥 ≠ 0} |
325 | 321, 324 | syl6eqel 2709 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑁 ≠ 0)
∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 ∥ 𝑁) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
326 | 306, 325 | pm2.61dan 832 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
327 | 324 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
328 | 326, 327 | ifclda 4120 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
329 | 328 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
330 | 198, 329 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
331 | | neeq1 2856 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → (𝑥 ≠ 0 ↔ 𝑘 ≠ 0)) |
332 | 331 | elrab 3363 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) |
333 | | neeq1 2856 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ≠ 0 ↔ 𝑦 ≠ 0)) |
334 | 333 | elrab 3363 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) |
335 | | mulcl 10020 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑘 · 𝑦) ∈ ℂ) |
336 | 335 | ad2ant2r 783 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑘 · 𝑦) ∈ ℂ) |
337 | | mulne0 10669 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑘 · 𝑦) ≠ 0) |
338 | 336, 337 | jca 554 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0)) |
339 | 332, 334,
338 | syl2anb 496 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) → ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0)) |
340 | | neeq1 2856 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 · 𝑦) → (𝑥 ≠ 0 ↔ (𝑘 · 𝑦) ≠ 0)) |
341 | 340 | elrab 3363 |
. . . . . . . . . 10
⊢ ((𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ ((𝑘 · 𝑦) ∈ ℂ ∧ (𝑘 · 𝑦) ≠ 0)) |
342 | 339, 341 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
343 | 342 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) ∧ (𝑘 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ∧ 𝑦 ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0})) → (𝑘 · 𝑦) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
344 | 188, 330,
343 | seqcl 12821 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0}) |
345 | | neeq1 2856 |
. . . . . . . . 9
⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) → (𝑥 ≠ 0 ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)) |
346 | 345 | elrab 3363 |
. . . . . . . 8
⊢ ((seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, ((𝐴
/L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} ↔ ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ ∧ (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)) |
347 | 346 | simprbi 480 |
. . . . . . 7
⊢ ((seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, ((𝐴
/L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ {𝑥 ∈ ℂ ∣ 𝑥 ≠ 0} → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0) |
348 | 344, 347 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐴 gcd 𝑁) = 1) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0) |
349 | 348 | ex 450 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 gcd 𝑁) = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0)) |
350 | 187, 349 | impbid 202 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1)) |
351 | 38, 61, 350 | 3bitrd 294 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1)) |
352 | 351 | 3expa 1265 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1)) |
353 | 35, 352 | pm2.61dane 2881 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1)) |