Step | Hyp | Ref
| Expression |
1 | | eqid 2170 |
. . 3
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) |
2 | | eqid 2170 |
. . 3
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < ) |
3 | | eqid 2170 |
. . 3
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ (𝐴 · 𝐵)}, ℝ, < ) = sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ (𝐴 · 𝐵)}, ℝ, < ) |
4 | 1, 2, 3 | pcpremul 12247 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) + sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )) = sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ (𝐴 · 𝐵)}, ℝ, < )) |
5 | 1 | pczpre 12251 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < )) |
6 | 5 | 3adant3 1012 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐴) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < )) |
7 | 2 | pczpre 12251 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐵) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )) |
8 | 7 | 3adant2 1011 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐵) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )) |
9 | 6, 8 | oveq12d 5871 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) + sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < ))) |
10 | | zmulcl 9265 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) ∈ ℤ) |
11 | 10 | ad2ant2r 506 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ∈ ℤ) |
12 | | zcn 9217 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
13 | 12 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 𝐴 ∈
ℂ) |
14 | | zcn 9217 |
. . . . . . . 8
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) |
15 | 14 | ad2antrl 487 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 𝐵 ∈
ℂ) |
16 | | simplr 525 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0) |
17 | | simpll 524 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 𝐴 ∈
ℤ) |
18 | | 0zd 9224 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 0 ∈
ℤ) |
19 | | zapne 9286 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 0 ∈
ℤ) → (𝐴 # 0
↔ 𝐴 ≠
0)) |
20 | 17, 18, 19 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 # 0 ↔ 𝐴 ≠ 0)) |
21 | 16, 20 | mpbird 166 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 𝐴 # 0) |
22 | | simprr 527 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 𝐵 ≠ 0) |
23 | | simprl 526 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 𝐵 ∈
ℤ) |
24 | | zapne 9286 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℤ ∧ 0 ∈
ℤ) → (𝐵 # 0
↔ 𝐵 ≠
0)) |
25 | 23, 18, 24 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐵 # 0 ↔ 𝐵 ≠ 0)) |
26 | 22, 25 | mpbird 166 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → 𝐵 # 0) |
27 | 13, 15, 21, 26 | mulap0d 8576 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) # 0) |
28 | | zapne 9286 |
. . . . . . 7
⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝐴 · 𝐵) # 0 ↔ (𝐴 · 𝐵) ≠ 0)) |
29 | 11, 18, 28 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) # 0 ↔ (𝐴 · 𝐵) ≠ 0)) |
30 | 27, 29 | mpbid 146 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ≠ 0) |
31 | 11, 30 | jca 304 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) ∈ ℤ ∧ (𝐴 · 𝐵) ≠ 0)) |
32 | 3 | pczpre 12251 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴 · 𝐵) ∈ ℤ ∧ (𝐴 · 𝐵) ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ (𝐴 · 𝐵)}, ℝ, < )) |
33 | 31, 32 | sylan2 284 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0))) → (𝑃 pCnt (𝐴 · 𝐵)) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ (𝐴 · 𝐵)}, ℝ, < )) |
34 | 33 | 3impb 1194 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ (𝐴 · 𝐵)}, ℝ, < )) |
35 | 4, 9, 34 | 3eqtr4rd 2214 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))) |