Step | Hyp | Ref
| Expression |
1 | | ax-1cn 10330 |
. . . . . . 7
⊢ 1 ∈
ℂ |
2 | | 0cn 10368 |
. . . . . . 7
⊢ 0 ∈
ℂ |
3 | 1, 2 | ifcli 4353 |
. . . . . 6
⊢ if((𝐵↑2) = 1, 1, 0) ∈
ℂ |
4 | 3 | mulid2i 10382 |
. . . . 5
⊢ (1
· if((𝐵↑2) = 1,
1, 0)) = if((𝐵↑2) = 1,
1, 0) |
5 | | iftrue 4313 |
. . . . . . 7
⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) =
1) |
6 | 5 | adantl 475 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) =
1) |
7 | 6 | oveq1d 6937 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) ·
if((𝐵↑2) = 1, 1, 0)) =
(1 · if((𝐵↑2) =
1, 1, 0))) |
8 | | simpl1 1199 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℤ) |
9 | 8 | zcnd 11835 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℂ) |
10 | 9 | ad2antrr 716 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐴 ∈
ℂ) |
11 | | simpl2 1201 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℤ) |
12 | 11 | zcnd 11835 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℂ) |
13 | 12 | ad2antrr 716 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐵 ∈
ℂ) |
14 | 10, 13 | sqmuld 13339 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) |
15 | | simpr 479 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐴↑2) = 1) |
16 | 15 | oveq1d 6937 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴↑2) · (𝐵↑2)) = (1 · (𝐵↑2))) |
17 | 12 | sqcld 13325 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵↑2) ∈ ℂ) |
18 | 17 | ad2antrr 716 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐵↑2) ∈
ℂ) |
19 | 18 | mulid2d 10395 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (1 ·
(𝐵↑2)) = (𝐵↑2)) |
20 | 14, 16, 19 | 3eqtrd 2818 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = (𝐵↑2)) |
21 | 20 | eqeq1d 2780 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (((𝐴 · 𝐵)↑2) = 1 ↔ (𝐵↑2) = 1)) |
22 | 21 | ifbid 4329 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = if((𝐵↑2) = 1, 1, 0)) |
23 | 4, 7, 22 | 3eqtr4a 2840 |
. . . 4
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) ·
if((𝐵↑2) = 1, 1, 0)) =
if(((𝐴 · 𝐵)↑2) = 1, 1,
0)) |
24 | 3 | mul02i 10565 |
. . . . 5
⊢ (0
· if((𝐵↑2) = 1,
1, 0)) = 0 |
25 | | iffalse 4316 |
. . . . . . 7
⊢ (¬
(𝐴↑2) = 1 →
if((𝐴↑2) = 1, 1, 0) =
0) |
26 | 25 | adantl 475 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) =
0) |
27 | 26 | oveq1d 6937 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) ·
if((𝐵↑2) = 1, 1, 0)) =
(0 · if((𝐵↑2) =
1, 1, 0))) |
28 | | dvdsmul1 15410 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵)) |
29 | 8, 11, 28 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∥ (𝐴 · 𝐵)) |
30 | 8, 11 | zmulcld 11840 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ∈ ℤ) |
31 | | dvdssq 15686 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 · 𝐵) ∈ ℤ) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))) |
32 | 8, 30, 31 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))) |
33 | 29, 32 | mpbid 224 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)) |
34 | 33 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)) |
35 | | breq2 4890 |
. . . . . . . . 9
⊢ (((𝐴 · 𝐵)↑2) = 1 → ((𝐴↑2) ∥ ((𝐴 · 𝐵)↑2) ↔ (𝐴↑2) ∥ 1)) |
36 | 34, 35 | syl5ibcom 237 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) ∥ 1)) |
37 | | simprl 761 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0) |
38 | 37 | neneqd 2974 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ 𝐴 = 0) |
39 | | sqeq0 13245 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) |
40 | 9, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) |
41 | 38, 40 | mtbird 317 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ (𝐴↑2) = 0) |
42 | | zsqcl2 13260 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℕ0) |
43 | 8, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈
ℕ0) |
44 | | elnn0 11644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴↑2) ∈
ℕ0 ↔ ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0)) |
45 | 43, 44 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0)) |
46 | 45 | ord 853 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (¬ (𝐴↑2) ∈ ℕ → (𝐴↑2) = 0)) |
47 | 41, 46 | mt3d 143 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈ ℕ) |
48 | 47 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℕ) |
49 | 48 | nnzd 11833 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ) |
50 | | 1nn 11387 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
51 | | dvdsle 15439 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℤ ∧ 1
∈ ℕ) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1)) |
52 | 49, 50, 51 | sylancl 580 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1)) |
53 | 48 | nnge1d 11423 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → 1 ≤ (𝐴↑2)) |
54 | 52, 53 | jctird 522 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → ((𝐴↑2) ≤ 1 ∧ 1 ≤
(𝐴↑2)))) |
55 | 48 | nnred 11391 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℝ) |
56 | | 1re 10376 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
57 | | letri3 10462 |
. . . . . . . . . 10
⊢ (((𝐴↑2) ∈ ℝ ∧ 1
∈ ℝ) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2)))) |
58 | 55, 56, 57 | sylancl 580 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2)))) |
59 | 54, 58 | sylibrd 251 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) = 1)) |
60 | 36, 59 | syld 47 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) = 1)) |
61 | 60 | con3dimp 399 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → ¬
((𝐴 · 𝐵)↑2) = 1) |
62 | 61 | iffalsed 4318 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = 0) |
63 | 24, 27, 62 | 3eqtr4a 2840 |
. . . 4
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) ·
if((𝐵↑2) = 1, 1, 0)) =
if(((𝐴 · 𝐵)↑2) = 1, 1,
0)) |
64 | 23, 63 | pm2.61dan 803 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) =
if(((𝐴 · 𝐵)↑2) = 1, 1,
0)) |
65 | | oveq2 6930 |
. . . . 5
⊢ (𝑁 = 0 → (𝐴 /L 𝑁) = (𝐴 /L 0)) |
66 | | lgs0 25487 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 /L 0) =
if((𝐴↑2) = 1, 1,
0)) |
67 | 8, 66 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 /L 0) = if((𝐴↑2) = 1, 1,
0)) |
68 | 65, 67 | sylan9eqr 2836 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴 /L 𝑁) = if((𝐴↑2) = 1, 1, 0)) |
69 | | oveq2 6930 |
. . . . 5
⊢ (𝑁 = 0 → (𝐵 /L 𝑁) = (𝐵 /L 0)) |
70 | | lgs0 25487 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → (𝐵 /L 0) =
if((𝐵↑2) = 1, 1,
0)) |
71 | 11, 70 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵 /L 0) = if((𝐵↑2) = 1, 1,
0)) |
72 | 69, 71 | sylan9eqr 2836 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐵 /L 𝑁) = if((𝐵↑2) = 1, 1, 0)) |
73 | 68, 72 | oveq12d 6940 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1,
0))) |
74 | | oveq2 6930 |
. . . 4
⊢ (𝑁 = 0 → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 · 𝐵) /L 0)) |
75 | | lgs0 25487 |
. . . . 5
⊢ ((𝐴 · 𝐵) ∈ ℤ → ((𝐴 · 𝐵) /L 0) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0)) |
76 | 30, 75 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 0) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0)) |
77 | 74, 76 | sylan9eqr 2836 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /L 𝑁) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0)) |
78 | 64, 73, 77 | 3eqtr4rd 2825 |
. 2
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
79 | | lgsdilem 25501 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1))) |
80 | 79 | adantr 474 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1))) |
81 | | mulcl 10356 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
82 | 81 | adantl 475 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
83 | | mulcom 10358 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
84 | 83 | adantl 475 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
85 | | mulass 10360 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
86 | 85 | adantl 475 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
87 | | simpl3 1203 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝑁 ∈ ℤ) |
88 | | nnabscl 14472 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
89 | 87, 88 | sylan 575 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ) |
90 | | nnuz 12029 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
91 | 89, 90 | syl6eleq 2869 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
(ℤ≥‘1)) |
92 | | simpll1 1226 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ) |
93 | | simpll3 1230 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ) |
94 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0) |
95 | | eqid 2778 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
96 | 95 | lgsfcl3 25495 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
97 | 92, 93, 94, 96 | syl3anc 1439 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
98 | | elfznn 12687 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ) |
99 | | ffvelrn 6621 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
100 | 97, 98, 99 | syl2an 589 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
101 | 100 | zcnd 11835 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
102 | | simpll2 1228 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐵 ∈ ℤ) |
103 | | eqid 2778 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
104 | 103 | lgsfcl3 25495 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
105 | 102, 93, 94, 104 | syl3anc 1439 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
106 | | ffvelrn 6621 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
107 | 105, 98, 106 | syl2an 589 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
108 | 107 | zcnd 11835 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
109 | 92 | adantr 474 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈
ℤ) |
110 | 102 | adantr 474 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐵 ∈
ℤ) |
111 | | simpr 479 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈
ℙ) |
112 | | lgsdirprm 25508 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑘) = ((𝐴 /L 𝑘) · (𝐵 /L 𝑘))) |
113 | 109, 110,
111, 112 | syl3anc 1439 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑘) = ((𝐴 /L 𝑘) · (𝐵 /L 𝑘))) |
114 | 113 | oveq1d 6937 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /L 𝑘) · (𝐵 /L 𝑘))↑(𝑘 pCnt 𝑁))) |
115 | | prmz 15794 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℤ) |
116 | | lgscl 25488 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈
ℤ) |
117 | 92, 115, 116 | syl2an 589 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈
ℤ) |
118 | 117 | zcnd 11835 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈
ℂ) |
119 | | lgscl 25488 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐵 /L 𝑘) ∈
ℤ) |
120 | 102, 115,
119 | syl2an 589 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /L 𝑘) ∈
ℤ) |
121 | 120 | zcnd 11835 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /L 𝑘) ∈
ℂ) |
122 | 93 | adantr 474 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈
ℤ) |
123 | 94 | adantr 474 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0) |
124 | | pczcl 15957 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
125 | 111, 122,
123, 124 | syl12anc 827 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
126 | 118, 121,
125 | mulexpd 13342 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 /L 𝑘) · (𝐵 /L 𝑘))↑(𝑘 pCnt 𝑁)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
127 | 114, 126 | eqtrd 2814 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
128 | | iftrue 4313 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁))) |
129 | 128 | adantl 475 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁))) |
130 | | iftrue 4313 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
131 | | iftrue 4313 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
132 | 130, 131 | oveq12d 6940 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
133 | 132 | adantl 475 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
134 | 127, 129,
133 | 3eqtr4d 2824 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
135 | | 1t1e1 11544 |
. . . . . . . . . . 11
⊢ (1
· 1) = 1 |
136 | 135 | eqcomi 2787 |
. . . . . . . . . 10
⊢ 1 = (1
· 1) |
137 | | iffalse 4316 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
(((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1) |
138 | | iffalse 4316 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1) |
139 | | iffalse 4316 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐵 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1) |
140 | 138, 139 | oveq12d 6940 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ℙ →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (1 · 1)) |
141 | 136, 137,
140 | 3eqtr4a 2840 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
(((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
142 | 141 | adantl 475 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ ¬ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
143 | 134, 142 | pm2.61dan 803 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
144 | 143 | adantr 474 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
145 | 98 | adantl 475 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → 𝑘 ∈ ℕ) |
146 | | eleq1w 2842 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
147 | | oveq2 6930 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐴 · 𝐵) /L 𝑛) = ((𝐴 · 𝐵) /L 𝑘)) |
148 | | oveq1 6929 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁)) |
149 | 147, 148 | oveq12d 6940 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)) = (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁))) |
150 | 146, 149 | ifbieq1d 4330 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
151 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
152 | | ovex 6954 |
. . . . . . . . 9
⊢ (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
153 | | 1ex 10372 |
. . . . . . . . 9
⊢ 1 ∈
V |
154 | 152, 153 | ifex 4355 |
. . . . . . . 8
⊢ if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
155 | 150, 151,
154 | fvmpt 6542 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
156 | 145, 155 | syl 17 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
157 | | oveq2 6930 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘)) |
158 | 157, 148 | oveq12d 6940 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
159 | 146, 158 | ifbieq1d 4330 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
160 | | ovex 6954 |
. . . . . . . . . 10
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
161 | 160, 153 | ifex 4355 |
. . . . . . . . 9
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
162 | 159, 95, 161 | fvmpt 6542 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
163 | 145, 162 | syl 17 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
164 | | oveq2 6930 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐵 /L 𝑛) = (𝐵 /L 𝑘)) |
165 | 164, 148 | oveq12d 6940 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
166 | 146, 165 | ifbieq1d 4330 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
167 | | ovex 6954 |
. . . . . . . . . 10
⊢ ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
168 | 167, 153 | ifex 4355 |
. . . . . . . . 9
⊢ if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
169 | 166, 103,
168 | fvmpt 6542 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
170 | 145, 169 | syl 17 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
171 | 163, 170 | oveq12d 6940 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
172 | 144, 156,
171 | 3eqtr4d 2824 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘))) |
173 | 82, 84, 86, 91, 101, 108, 172 | seqcaopr 13156 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
174 | 80, 173 | oveq12d 6940 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 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‘𝑁))))) |
175 | 30 | adantr 474 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 · 𝐵) ∈ ℤ) |
176 | 151 | lgsval4 25494 |
. . . 4
⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
(((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
177 | 175, 93, 94, 176 | syl3anc 1439 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
(((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
178 | 95 | lgsval4 25494 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
179 | 92, 93, 94, 178 | syl3anc 1439 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
180 | 103 | lgsval4 25494 |
. . . . . 6
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐵 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐵 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
181 | 102, 93, 94, 180 | syl3anc 1439 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐵 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐵 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
182 | 179, 181 | oveq12d 6940 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 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‘𝑁))))) |
183 | | neg1cn 11496 |
. . . . . . 7
⊢ -1 ∈
ℂ |
184 | 183, 1 | ifcli 4353 |
. . . . . 6
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ |
185 | 184 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ) |
186 | | mulcl 10356 |
. . . . . . 7
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
187 | 186 | adantl 475 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
188 | 91, 101, 187 | seqcl 13139 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ) |
189 | 183, 1 | ifcli 4353 |
. . . . . 6
⊢ if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈
ℂ |
190 | 189 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈
ℂ) |
191 | 91, 108, 187 | seqcl 13139 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ) |
192 | 185, 188,
190, 191 | mul4d 10588 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 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‘𝑁))))) |
193 | 182, 192 | eqtrd 2814 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 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‘𝑁))))) |
194 | 174, 177,
193 | 3eqtr4d 2824 |
. 2
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
195 | 78, 194 | pm2.61dane 3057 |
1
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |