Proof of Theorem pcqdiv
Step | Hyp | Ref
| Expression |
1 | | simp2l 1018 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐴 ∈
ℚ) |
2 | | qcn 9580 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
3 | 1, 2 | syl 14 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐴 ∈
ℂ) |
4 | | simp3l 1020 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐵 ∈
ℚ) |
5 | | qcn 9580 |
. . . . . . 7
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℂ) |
6 | 4, 5 | syl 14 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐵 ∈
ℂ) |
7 | | simp3r 1021 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐵 ≠ 0) |
8 | | 0z 9210 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
9 | | zq 9572 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢ 0 ∈
ℚ |
11 | | qapne 9585 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℚ ∧ 0 ∈
ℚ) → (𝐵 # 0
↔ 𝐵 ≠
0)) |
12 | 4, 10, 11 | sylancl 411 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝐵 # 0 ↔ 𝐵 ≠ 0)) |
13 | 7, 12 | mpbird 166 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐵 # 0) |
14 | 3, 6, 13 | divcanap1d 8695 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ((𝐴 / 𝐵) · 𝐵) = 𝐴) |
15 | 14 | oveq2d 5866 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt ((𝐴 / 𝐵) · 𝐵)) = (𝑃 pCnt 𝐴)) |
16 | | simp1 992 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝑃 ∈
ℙ) |
17 | | qdivcl 9589 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) |
18 | 1, 4, 7, 17 | syl3anc 1233 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ∈ ℚ) |
19 | | simp2r 1019 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0) |
20 | | qapne 9585 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℚ ∧ 0 ∈
ℚ) → (𝐴 # 0
↔ 𝐴 ≠
0)) |
21 | 1, 10, 20 | sylancl 411 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝐴 # 0 ↔ 𝐴 ≠ 0)) |
22 | 19, 21 | mpbird 166 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐴 # 0) |
23 | 3, 6, 22, 13 | divap0d 8710 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) # 0) |
24 | | qapne 9585 |
. . . . . . 7
⊢ (((𝐴 / 𝐵) ∈ ℚ ∧ 0 ∈ ℚ)
→ ((𝐴 / 𝐵) # 0 ↔ (𝐴 / 𝐵) ≠ 0)) |
25 | 18, 10, 24 | sylancl 411 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ((𝐴 / 𝐵) # 0 ↔ (𝐴 / 𝐵) ≠ 0)) |
26 | 23, 25 | mpbid 146 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ≠ 0) |
27 | | pcqmul 12244 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴 / 𝐵) ∈ ℚ ∧ (𝐴 / 𝐵) ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt ((𝐴 / 𝐵) · 𝐵)) = ((𝑃 pCnt (𝐴 / 𝐵)) + (𝑃 pCnt 𝐵))) |
28 | 16, 18, 26, 4, 7, 27 | syl122anc 1242 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt ((𝐴 / 𝐵) · 𝐵)) = ((𝑃 pCnt (𝐴 / 𝐵)) + (𝑃 pCnt 𝐵))) |
29 | 15, 28 | eqtr3d 2205 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐴) = ((𝑃 pCnt (𝐴 / 𝐵)) + (𝑃 pCnt 𝐵))) |
30 | 29 | oveq1d 5865 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (((𝑃 pCnt (𝐴 / 𝐵)) + (𝑃 pCnt 𝐵)) − (𝑃 pCnt 𝐵))) |
31 | | pcqcl 12247 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴 / 𝐵) ∈ ℚ ∧ (𝐴 / 𝐵) ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) ∈ ℤ) |
32 | 16, 18, 26, 31 | syl12anc 1231 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) ∈ ℤ) |
33 | 32 | zcnd 9322 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) ∈ ℂ) |
34 | | pcqcl 12247 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐵) ∈ ℤ) |
35 | 34 | 3adant2 1011 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐵) ∈ ℤ) |
36 | 35 | zcnd 9322 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐵) ∈ ℂ) |
37 | 33, 36 | pncand 8218 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (((𝑃 pCnt (𝐴 / 𝐵)) + (𝑃 pCnt 𝐵)) − (𝑃 pCnt 𝐵)) = (𝑃 pCnt (𝐴 / 𝐵))) |
38 | 30, 37 | eqtr2d 2204 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵))) |