| Step | Hyp | Ref
| Expression |
| 1 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 2 | | 0cn 11253 |
. . . . . . 7
⊢ 0 ∈
ℂ |
| 3 | 1, 2 | ifcli 4573 |
. . . . . 6
⊢ if((𝐵↑2) = 1, 1, 0) ∈
ℂ |
| 4 | 3 | mullidi 11266 |
. . . . 5
⊢ (1
· if((𝐵↑2) = 1,
1, 0)) = if((𝐵↑2) = 1,
1, 0) |
| 5 | | iftrue 4531 |
. . . . . . 7
⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) =
1) |
| 6 | 5 | adantl 481 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) =
1) |
| 7 | 6 | oveq1d 7446 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) ·
if((𝐵↑2) = 1, 1, 0)) =
(1 · if((𝐵↑2) =
1, 1, 0))) |
| 8 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℤ) |
| 9 | 8 | zcnd 12723 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℂ) |
| 10 | 9 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐴 ∈
ℂ) |
| 11 | | simpl2 1193 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℤ) |
| 12 | 11 | zcnd 12723 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℂ) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐵 ∈
ℂ) |
| 14 | 10, 13 | sqmuld 14198 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) |
| 15 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐴↑2) = 1) |
| 16 | 15 | oveq1d 7446 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴↑2) · (𝐵↑2)) = (1 · (𝐵↑2))) |
| 17 | 12 | sqcld 14184 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵↑2) ∈ ℂ) |
| 18 | 17 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐵↑2) ∈
ℂ) |
| 19 | 18 | mullidd 11279 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (1 ·
(𝐵↑2)) = (𝐵↑2)) |
| 20 | 14, 16, 19 | 3eqtrd 2781 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = (𝐵↑2)) |
| 21 | 20 | eqeq1d 2739 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (((𝐴 · 𝐵)↑2) = 1 ↔ (𝐵↑2) = 1)) |
| 22 | 21 | ifbid 4549 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = if((𝐵↑2) = 1, 1, 0)) |
| 23 | 4, 7, 22 | 3eqtr4a 2803 |
. . . 4
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) ·
if((𝐵↑2) = 1, 1, 0)) =
if(((𝐴 · 𝐵)↑2) = 1, 1,
0)) |
| 24 | 3 | mul02i 11450 |
. . . . 5
⊢ (0
· if((𝐵↑2) = 1,
1, 0)) = 0 |
| 25 | | iffalse 4534 |
. . . . . . 7
⊢ (¬
(𝐴↑2) = 1 →
if((𝐴↑2) = 1, 1, 0) =
0) |
| 26 | 25 | adantl 481 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) =
0) |
| 27 | 26 | oveq1d 7446 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) ·
if((𝐵↑2) = 1, 1, 0)) =
(0 · if((𝐵↑2) =
1, 1, 0))) |
| 28 | | dvdsmul1 16315 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵)) |
| 29 | 8, 11, 28 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∥ (𝐴 · 𝐵)) |
| 30 | 8, 11 | zmulcld 12728 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ∈ ℤ) |
| 31 | | dvdssq 16604 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 · 𝐵) ∈ ℤ) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))) |
| 32 | 8, 30, 31 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))) |
| 33 | 29, 32 | mpbid 232 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)) |
| 34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)) |
| 35 | | breq2 5147 |
. . . . . . . . 9
⊢ (((𝐴 · 𝐵)↑2) = 1 → ((𝐴↑2) ∥ ((𝐴 · 𝐵)↑2) ↔ (𝐴↑2) ∥ 1)) |
| 36 | 34, 35 | syl5ibcom 245 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) ∥ 1)) |
| 37 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0) |
| 38 | 37 | neneqd 2945 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ 𝐴 = 0) |
| 39 | | sqeq0 14160 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) |
| 40 | 9, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) |
| 41 | 38, 40 | mtbird 325 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ (𝐴↑2) = 0) |
| 42 | | zsqcl2 14178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℕ0) |
| 43 | 8, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈
ℕ0) |
| 44 | | elnn0 12528 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴↑2) ∈
ℕ0 ↔ ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0)) |
| 45 | 43, 44 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0)) |
| 46 | 45 | ord 865 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (¬ (𝐴↑2) ∈ ℕ → (𝐴↑2) = 0)) |
| 47 | 41, 46 | mt3d 148 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈ ℕ) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℕ) |
| 49 | 48 | nnzd 12640 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ) |
| 50 | | 1nn 12277 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
| 51 | | dvdsle 16347 |
. . . . . . . . . . 11
⊢ (((𝐴↑2) ∈ ℤ ∧ 1
∈ ℕ) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1)) |
| 52 | 49, 50, 51 | sylancl 586 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1)) |
| 53 | 48 | nnge1d 12314 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → 1 ≤ (𝐴↑2)) |
| 54 | 52, 53 | jctird 526 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → ((𝐴↑2) ≤ 1 ∧ 1 ≤
(𝐴↑2)))) |
| 55 | 48 | nnred 12281 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℝ) |
| 56 | | 1re 11261 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
| 57 | | letri3 11346 |
. . . . . . . . . 10
⊢ (((𝐴↑2) ∈ ℝ ∧ 1
∈ ℝ) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2)))) |
| 58 | 55, 56, 57 | sylancl 586 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2)))) |
| 59 | 54, 58 | sylibrd 259 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) = 1)) |
| 60 | 36, 59 | syld 47 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) = 1)) |
| 61 | 60 | con3dimp 408 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → ¬
((𝐴 · 𝐵)↑2) = 1) |
| 62 | 61 | iffalsed 4536 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = 0) |
| 63 | 24, 27, 62 | 3eqtr4a 2803 |
. . . 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 813 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) =
if(((𝐴 · 𝐵)↑2) = 1, 1,
0)) |
| 65 | | oveq2 7439 |
. . . . 5
⊢ (𝑁 = 0 → (𝐴 /L 𝑁) = (𝐴 /L 0)) |
| 66 | | lgs0 27354 |
. . . . . 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 2799 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴 /L 𝑁) = if((𝐴↑2) = 1, 1, 0)) |
| 69 | | oveq2 7439 |
. . . . 5
⊢ (𝑁 = 0 → (𝐵 /L 𝑁) = (𝐵 /L 0)) |
| 70 | | lgs0 27354 |
. . . . . 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 2799 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐵 /L 𝑁) = if((𝐵↑2) = 1, 1, 0)) |
| 73 | 68, 72 | oveq12d 7449 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1,
0))) |
| 74 | | oveq2 7439 |
. . . 4
⊢ (𝑁 = 0 → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 · 𝐵) /L 0)) |
| 75 | | lgs0 27354 |
. . . . 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 2799 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /L 𝑁) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0)) |
| 78 | 64, 73, 77 | 3eqtr4rd 2788 |
. 2
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
| 79 | | lgsdilem 27368 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1))) |
| 80 | 79 | adantr 480 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1))) |
| 81 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝑁 ∈ ℤ) |
| 82 | | nnabscl 15364 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
| 83 | 81, 82 | sylan 580 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ) |
| 84 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 85 | 83, 84 | eleqtrdi 2851 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
(ℤ≥‘1)) |
| 86 | | simpll1 1213 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ) |
| 87 | | simpll3 1215 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ) |
| 88 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0) |
| 89 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
| 90 | 89 | lgsfcl3 27362 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
| 91 | 86, 87, 88, 90 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
| 92 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ) |
| 93 | | ffvelcdm 7101 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
| 94 | 91, 92, 93 | syl2an 596 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
| 95 | 94 | zcnd 12723 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
| 96 | | simpll2 1214 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐵 ∈ ℤ) |
| 97 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
| 98 | 97 | lgsfcl3 27362 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
| 99 | 96, 87, 88, 98 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
| 100 | | ffvelcdm 7101 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
| 101 | 99, 92, 100 | syl2an 596 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
| 102 | 101 | zcnd 12723 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
| 103 | 86 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈
ℤ) |
| 104 | 96 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐵 ∈
ℤ) |
| 105 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈
ℙ) |
| 106 | | lgsdirprm 27375 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑘) = ((𝐴 /L 𝑘) · (𝐵 /L 𝑘))) |
| 107 | 103, 104,
105, 106 | syl3anc 1373 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑘) = ((𝐴 /L 𝑘) · (𝐵 /L 𝑘))) |
| 108 | 107 | oveq1d 7446 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /L 𝑘) · (𝐵 /L 𝑘))↑(𝑘 pCnt 𝑁))) |
| 109 | | prmz 16712 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℤ) |
| 110 | | lgscl 27355 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈
ℤ) |
| 111 | 86, 109, 110 | syl2an 596 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈
ℤ) |
| 112 | 111 | zcnd 12723 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈
ℂ) |
| 113 | | lgscl 27355 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐵 /L 𝑘) ∈
ℤ) |
| 114 | 96, 109, 113 | syl2an 596 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /L 𝑘) ∈
ℤ) |
| 115 | 114 | zcnd 12723 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /L 𝑘) ∈
ℂ) |
| 116 | 87 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈
ℤ) |
| 117 | 88 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0) |
| 118 | | pczcl 16886 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
| 119 | 105, 116,
117, 118 | syl12anc 837 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
| 120 | 112, 115,
119 | mulexpd 14201 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 /L 𝑘) · (𝐵 /L 𝑘))↑(𝑘 pCnt 𝑁)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
| 121 | 108, 120 | eqtrd 2777 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
| 122 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 123 | 122 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 124 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 125 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 126 | 124, 125 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
| 127 | 126 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
| 128 | 121, 123,
127 | 3eqtr4d 2787 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
| 129 | | 1t1e1 12428 |
. . . . . . . . . . 11
⊢ (1
· 1) = 1 |
| 130 | 129 | eqcomi 2746 |
. . . . . . . . . 10
⊢ 1 = (1
· 1) |
| 131 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
(((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1) |
| 132 | | iffalse 4534 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1) |
| 133 | | iffalse 4534 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐵 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1) |
| 134 | 132, 133 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ℙ →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (1 · 1)) |
| 135 | 130, 131,
134 | 3eqtr4a 2803 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
(((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
| 136 | 135 | adantl 481 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ ¬ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
| 137 | 128, 136 | pm2.61dan 813 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
| 138 | 137 | adantr 480 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
| 139 | 92 | adantl 481 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → 𝑘 ∈ ℕ) |
| 140 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
| 141 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐴 · 𝐵) /L 𝑛) = ((𝐴 · 𝐵) /L 𝑘)) |
| 142 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁)) |
| 143 | 141, 142 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)) = (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 144 | 140, 143 | ifbieq1d 4550 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 145 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
| 146 | | ovex 7464 |
. . . . . . . . 9
⊢ (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
| 147 | | 1ex 11257 |
. . . . . . . . 9
⊢ 1 ∈
V |
| 148 | 146, 147 | ifex 4576 |
. . . . . . . 8
⊢ if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
| 149 | 144, 145,
148 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 150 | 139, 149 | syl 17 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 151 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘)) |
| 152 | 151, 142 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 153 | 140, 152 | ifbieq1d 4550 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 154 | | ovex 7464 |
. . . . . . . . . 10
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
| 155 | 154, 147 | ifex 4576 |
. . . . . . . . 9
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
| 156 | 153, 89, 155 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 157 | 139, 156 | syl 17 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 158 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐵 /L 𝑛) = (𝐵 /L 𝑘)) |
| 159 | 158, 142 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 160 | 140, 159 | ifbieq1d 4550 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 161 | | ovex 7464 |
. . . . . . . . . 10
⊢ ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
| 162 | 161, 147 | ifex 4576 |
. . . . . . . . 9
⊢ if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
| 163 | 160, 97, 162 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 164 | 139, 163 | syl 17 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 165 | 157, 164 | oveq12d 7449 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
| 166 | 138, 150,
165 | 3eqtr4d 2787 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘))) |
| 167 | 85, 95, 102, 166 | prodfmul 15926 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 168 | 80, 167 | oveq12d 7449 |
. . 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‘𝑁))))) |
| 169 | 30 | adantr 480 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 · 𝐵) ∈ ℤ) |
| 170 | 145 | lgsval4 27361 |
. . . 4
⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
(((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 171 | 169, 87, 88, 170 | syl3anc 1373 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
(((𝐴 · 𝐵) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 172 | 89 | lgsval4 27361 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 173 | 86, 87, 88, 172 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 174 | 97 | lgsval4 27361 |
. . . . . 6
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐵 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐵 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 175 | 96, 87, 88, 174 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐵 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐵 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 176 | 173, 175 | oveq12d 7449 |
. . . 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‘𝑁))))) |
| 177 | | neg1cn 12380 |
. . . . . . 7
⊢ -1 ∈
ℂ |
| 178 | 177, 1 | ifcli 4573 |
. . . . . 6
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ |
| 179 | 178 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ) |
| 180 | | mulcl 11239 |
. . . . . . 7
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
| 181 | 180 | adantl 481 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝐴 ≠ 0
∧ 𝐵 ≠ 0)) ∧
𝑁 ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
| 182 | 85, 95, 181 | seqcl 14063 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ) |
| 183 | 177, 1 | ifcli 4573 |
. . . . . 6
⊢ if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈
ℂ |
| 184 | 183 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈
ℂ) |
| 185 | 85, 102, 181 | seqcl 14063 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ) |
| 186 | 179, 182,
184, 185 | mul4d 11473 |
. . . 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‘𝑁))))) |
| 187 | 176, 186 | eqtrd 2777 |
. . 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‘𝑁))))) |
| 188 | 168, 171,
187 | 3eqtr4d 2787 |
. 2
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |
| 189 | 78, 188 | pm2.61dane 3029 |
1
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁))) |