Step | Hyp | Ref
| Expression |
1 | | 3anrot 1043 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈
ℤ)) |
2 | | lgsdilem 25049 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1))) |
3 | 1, 2 | sylanb 489 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1))) |
4 | | ancom 466 |
. . . . 5
⊢ (((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ (𝑀 · 𝑁) < 0)) |
5 | | ifbi 4107 |
. . . . 5
⊢ ((((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ (𝑀 · 𝑁) < 0)) → if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1)) |
6 | 4, 5 | ax-mp 5 |
. . . 4
⊢
if(((𝑀 ·
𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1) |
7 | | ancom 466 |
. . . . . 6
⊢ ((𝑀 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑀 < 0)) |
8 | | ifbi 4107 |
. . . . . 6
⊢ (((𝑀 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑀 < 0)) → if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1)) |
9 | 7, 8 | ax-mp 5 |
. . . . 5
⊢ if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) |
10 | | ancom 466 |
. . . . . 6
⊢ ((𝑁 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑁 < 0)) |
11 | | ifbi 4107 |
. . . . . 6
⊢ (((𝑁 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑁 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1)) |
12 | 10, 11 | ax-mp 5 |
. . . . 5
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1) |
13 | 9, 12 | oveq12i 6662 |
. . . 4
⊢
(if((𝑀 < 0 ∧
𝐴 < 0), -1, 1) ·
if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1)) |
14 | 3, 6, 13 | 3eqtr4g 2681 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))) |
15 | | mulcl 10020 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
16 | 15 | adantl 482 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
17 | | mulcom 10022 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
18 | 17 | adantl 482 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
19 | | mulass 10024 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
20 | 19 | adantl 482 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
21 | | simpl2 1065 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ∈ ℤ) |
22 | | simpl3 1066 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℤ) |
23 | 21, 22 | zmulcld 11488 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ∈ ℤ) |
24 | 21 | zcnd 11483 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ∈ ℂ) |
25 | 22 | zcnd 11483 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℂ) |
26 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ≠ 0) |
27 | | simprr 796 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ≠ 0) |
28 | 24, 25, 26, 27 | mulne0d 10679 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ≠ 0) |
29 | | nnabscl 14065 |
. . . . . . 7
⊢ (((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (abs‘(𝑀 · 𝑁)) ∈ ℕ) |
30 | 23, 28, 29 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) ∈ ℕ) |
31 | | nnuz 11723 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
32 | 30, 31 | syl6eleq 2711 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) ∈
(ℤ≥‘1)) |
33 | | simpl1 1064 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝐴 ∈ ℤ) |
34 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) |
35 | 34 | lgsfcl3 25043 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)),
1)):ℕ⟶ℤ) |
36 | 33, 21, 26, 35 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)),
1)):ℕ⟶ℤ) |
37 | | elfznn 12370 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(abs‘(𝑀 · 𝑁))) → 𝑘 ∈ ℕ) |
38 | | ffvelrn 6357 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ) |
39 | 36, 37, 38 | syl2an 494 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ) |
40 | 39 | zcnd 11483 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℂ) |
41 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
42 | 41 | lgsfcl3 25043 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
43 | 33, 22, 27, 42 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
44 | | ffvelrn 6357 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
45 | 43, 37, 44 | syl2an 494 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
46 | 45 | zcnd 11483 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
47 | | simpr 477 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈
ℙ) |
48 | 21 | ad2antrr 762 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈
ℤ) |
49 | 26 | ad2antrr 762 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ≠ 0) |
50 | 22 | ad2antrr 762 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈
ℤ) |
51 | 27 | ad2antrr 762 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0) |
52 | | pcmul 15556 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt (𝑀 · 𝑁)) = ((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁))) |
53 | 47, 48, 49, 50, 51, 52 | syl122anc 1335 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (𝑀 · 𝑁)) = ((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁))) |
54 | 53 | oveq2d 6666 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) = ((𝐴 /L 𝑘)↑((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁)))) |
55 | 33 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈
ℤ) |
56 | | prmz 15389 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℤ) |
57 | 56 | adantl 482 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈
ℤ) |
58 | | lgscl 25036 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈
ℤ) |
59 | 55, 57, 58 | syl2anc 693 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈
ℤ) |
60 | 59 | zcnd 11483 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈
ℂ) |
61 | | pczcl 15553 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
62 | 47, 50, 51, 61 | syl12anc 1324 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
63 | | pczcl 15553 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝑘 pCnt 𝑀) ∈
ℕ0) |
64 | 47, 48, 49, 63 | syl12anc 1324 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑀) ∈
ℕ0) |
65 | 60, 62, 64 | expaddd 13010 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁))) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
66 | 54, 65 | eqtrd 2656 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
67 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁)))) |
68 | 67 | adantl 482 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁)))) |
69 | | iftrue 4092 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀))) |
70 | | iftrue 4092 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
71 | 69, 70 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
72 | 71 | adantl 482 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
73 | 66, 68, 72 | 3eqtr4rd 2667 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
74 | | 1t1e1 11175 |
. . . . . . . . 9
⊢ (1
· 1) = 1 |
75 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) = 1) |
76 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1) |
77 | 75, 76 | oveq12d 6668 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ ℙ →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (1 · 1)) |
78 | | iffalse 4095 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = 1) |
79 | 74, 77, 78 | 3eqtr4a 2682 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ ℙ →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
80 | 79 | adantl 482 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ ¬ 𝑘 ∈ ℙ) →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
81 | 73, 80 | pm2.61dan 832 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
82 | 37 | adantl 482 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℕ) |
83 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
84 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘)) |
85 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑀) = (𝑘 pCnt 𝑀)) |
86 | 84, 85 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀))) |
87 | 83, 86 | ifbieq1d 4109 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
88 | | ovex 6678 |
. . . . . . . . . 10
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) ∈ V |
89 | | 1ex 10035 |
. . . . . . . . . 10
⊢ 1 ∈
V |
90 | 88, 89 | ifex 4156 |
. . . . . . . . 9
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) ∈ V |
91 | 87, 34, 90 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
92 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁)) |
93 | 84, 92 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
94 | 83, 93 | ifbieq1d 4109 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
95 | | ovex 6678 |
. . . . . . . . . 10
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
96 | 95, 89 | ifex 4156 |
. . . . . . . . 9
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
97 | 94, 41, 96 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
98 | 91, 97 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
99 | 82, 98 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
100 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑛 pCnt (𝑀 · 𝑁)) = (𝑘 pCnt (𝑀 · 𝑁))) |
101 | 84, 100 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))) = ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁)))) |
102 | 83, 101 | ifbieq1d 4109 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
103 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)) |
104 | | ovex 6678 |
. . . . . . . . 9
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) ∈ V |
105 | 104, 89 | ifex 4156 |
. . . . . . . 8
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) ∈ V |
106 | 102, 103,
105 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
107 | 82, 106 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
108 | 81, 99, 107 | 3eqtr4rd 2667 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))‘𝑘) = (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘))) |
109 | 16, 18, 20, 32, 40, 46, 108 | seqcaopr 12838 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁))) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁))))) |
110 | 33, 21, 22, 26, 27, 34 | lgsdilem2 25058 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁)))) |
111 | 33, 22, 21, 27, 26, 41 | lgsdilem2 25058 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑁 · 𝑀)))) |
112 | 24, 25 | mulcomd 10061 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
113 | 112 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) = (abs‘(𝑁 · 𝑀))) |
114 | 113 | fveq2d 6195 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑁 · 𝑀)))) |
115 | 111, 114 | eqtr4d 2659 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁)))) |
116 | 110, 115 | oveq12d 6668 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁))) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁))))) |
117 | 109, 116 | eqtr4d 2659 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
118 | 14, 117 | oveq12d 6668 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁)))) = ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · ((seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
119 | 103 | lgsval4 25042 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (𝐴 /L (𝑀 · 𝑁)) = (if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))))) |
120 | 33, 23, 28, 119 | syl3anc 1326 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L (𝑀 · 𝑁)) = (if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))))) |
121 | 34 | lgsval4 25042 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝐴 /L 𝑀) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)))) |
122 | 33, 21, 26, 121 | syl3anc 1326 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L 𝑀) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)))) |
123 | 41 | lgsval4 25042 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
124 | 33, 22, 27, 123 | syl3anc 1326 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
125 | 122, 124 | oveq12d 6668 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)) = ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀))) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
126 | | neg1cn 11124 |
. . . . . 6
⊢ -1 ∈
ℂ |
127 | | ax-1cn 9994 |
. . . . . 6
⊢ 1 ∈
ℂ |
128 | 126, 127 | keepel 4155 |
. . . . 5
⊢ if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ |
129 | 128 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ) |
130 | | nnabscl 14065 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℕ) |
131 | 21, 26, 130 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑀) ∈
ℕ) |
132 | 131, 31 | syl6eleq 2711 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑀) ∈
(ℤ≥‘1)) |
133 | | elfznn 12370 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(abs‘𝑀)) → 𝑘 ∈ ℕ) |
134 | 36, 133, 38 | syl2an 494 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘𝑀))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ) |
135 | 134 | zcnd 11483 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘𝑀))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℂ) |
136 | | mulcl 10020 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
137 | 136 | adantl 482 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
138 | 132, 135,
137 | seqcl 12821 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) ∈ ℂ) |
139 | 126, 127 | keepel 4155 |
. . . . 5
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ |
140 | 139 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ) |
141 | | nnabscl 14065 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
142 | 22, 27, 141 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑁) ∈
ℕ) |
143 | 142, 31 | syl6eleq 2711 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑁) ∈
(ℤ≥‘1)) |
144 | | elfznn 12370 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ) |
145 | 43, 144, 44 | syl2an 494 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
146 | 145 | zcnd 11483 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
147 | 143, 146,
137 | seqcl 12821 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ) |
148 | 129, 138,
140, 147 | mul4d 10248 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀))) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) = ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · ((seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
149 | 125, 148 | eqtrd 2656 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)) = ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · ((seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
150 | 118, 120,
149 | 3eqtr4d 2666 |
1
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁))) |