# Metamath Proof Explorer

## Theorem pcdiv

Description: Division property of the prime power function. (Contributed by Mario Carneiro, 1-Mar-2014)

Ref Expression
Assertion pcdiv ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {P}\mathrm{pCnt}\left(\frac{{A}}{{B}}\right)=\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {P}\in ℙ$
2 simp2l ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {A}\in ℤ$
3 simp3 ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {B}\in ℕ$
4 znq ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to \frac{{A}}{{B}}\in ℚ$
5 2 3 4 syl2anc ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to \frac{{A}}{{B}}\in ℚ$
6 2 zcnd ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {A}\in ℂ$
7 3 nncnd ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {B}\in ℂ$
8 simp2r ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {A}\ne 0$
9 3 nnne0d ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {B}\ne 0$
10 6 7 8 9 divne0d ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to \frac{{A}}{{B}}\ne 0$
11 eqid ${⊢}sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)$
12 eqid ${⊢}sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)$
13 11 12 pcval ${⊢}\left({P}\in ℙ\wedge \left(\frac{{A}}{{B}}\in ℚ\wedge \frac{{A}}{{B}}\ne 0\right)\right)\to {P}\mathrm{pCnt}\left(\frac{{A}}{{B}}\right)=\left(\iota {z}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)$
14 1 5 10 13 syl12anc ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {P}\mathrm{pCnt}\left(\frac{{A}}{{B}}\right)=\left(\iota {z}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)$
15 eqid ${⊢}sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)$
16 15 pczpre ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\right)\to {P}\mathrm{pCnt}{A}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)$
17 16 3adant3 ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {P}\mathrm{pCnt}{A}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)$
18 nnz ${⊢}{B}\in ℕ\to {B}\in ℤ$
19 nnne0 ${⊢}{B}\in ℕ\to {B}\ne 0$
20 18 19 jca ${⊢}{B}\in ℕ\to \left({B}\in ℤ\wedge {B}\ne 0\right)$
21 eqid ${⊢}sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)$
22 21 pczpre ${⊢}\left({P}\in ℙ\wedge \left({B}\in ℤ\wedge {B}\ne 0\right)\right)\to {P}\mathrm{pCnt}{B}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)$
23 20 22 sylan2 ${⊢}\left({P}\in ℙ\wedge {B}\in ℕ\right)\to {P}\mathrm{pCnt}{B}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)$
24 23 3adant2 ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {P}\mathrm{pCnt}{B}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)$
25 17 24 oveq12d ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)$
26 eqid ${⊢}\frac{{A}}{{B}}=\frac{{A}}{{B}}$
27 25 26 jctil ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to \left(\frac{{A}}{{B}}=\frac{{A}}{{B}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)\right)$
28 oveq1 ${⊢}{x}={A}\to \frac{{x}}{{y}}=\frac{{A}}{{y}}$
29 28 eqeq2d ${⊢}{x}={A}\to \left(\frac{{A}}{{B}}=\frac{{x}}{{y}}↔\frac{{A}}{{B}}=\frac{{A}}{{y}}\right)$
30 breq2 ${⊢}{x}={A}\to \left({{P}}^{{n}}\parallel {x}↔{{P}}^{{n}}\parallel {A}\right)$
31 30 rabbidv ${⊢}{x}={A}\to \left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\}=\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\}$
32 31 supeq1d ${⊢}{x}={A}\to sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)$
33 32 oveq1d ${⊢}{x}={A}\to sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)$
34 33 eqeq2d ${⊢}{x}={A}\to \left(\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)↔\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)$
35 29 34 anbi12d ${⊢}{x}={A}\to \left(\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)↔\left(\frac{{A}}{{B}}=\frac{{A}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)$
36 oveq2 ${⊢}{y}={B}\to \frac{{A}}{{y}}=\frac{{A}}{{B}}$
37 36 eqeq2d ${⊢}{y}={B}\to \left(\frac{{A}}{{B}}=\frac{{A}}{{y}}↔\frac{{A}}{{B}}=\frac{{A}}{{B}}\right)$
38 breq2 ${⊢}{y}={B}\to \left({{P}}^{{n}}\parallel {y}↔{{P}}^{{n}}\parallel {B}\right)$
39 38 rabbidv ${⊢}{y}={B}\to \left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\}=\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\}$
40 39 supeq1d ${⊢}{y}={B}\to sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)$
41 40 oveq2d ${⊢}{y}={B}\to sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)$
42 41 eqeq2d ${⊢}{y}={B}\to \left(\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)↔\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)\right)$
43 37 42 anbi12d ${⊢}{y}={B}\to \left(\left(\frac{{A}}{{B}}=\frac{{A}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)↔\left(\frac{{A}}{{B}}=\frac{{A}}{{B}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)\right)\right)$
44 35 43 rspc2ev ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\wedge \left(\frac{{A}}{{B}}=\frac{{A}}{{B}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {A}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {B}\right\},ℝ,<\right)\right)\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)$
45 2 3 27 44 syl3anc ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)$
46 ovex ${⊢}\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)\in \mathrm{V}$
47 11 12 pceu ${⊢}\left({P}\in ℙ\wedge \left(\frac{{A}}{{B}}\in ℚ\wedge \frac{{A}}{{B}}\ne 0\right)\right)\to \exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)$
48 1 5 10 47 syl12anc ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to \exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)$
49 eqeq1 ${⊢}{z}=\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)\to \left({z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)↔\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)$
50 49 anbi2d ${⊢}{z}=\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)\to \left(\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)↔\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)$
51 50 2rexbidv ${⊢}{z}=\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)$
52 51 iota2 ${⊢}\left(\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)\in \mathrm{V}\wedge \exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)↔\left(\iota {z}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)=\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)\right)$
53 46 48 52 sylancr ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge \left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)↔\left(\iota {z}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)=\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)\right)$
54 45 53 mpbid ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to \left(\iota {z}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\frac{{A}}{{B}}=\frac{{x}}{{y}}\wedge {z}=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {x}\right\},ℝ,<\right)-sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel {y}\right\},ℝ,<\right)\right)\right)=\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)$
55 14 54 eqtrd ${⊢}\left({P}\in ℙ\wedge \left({A}\in ℤ\wedge {A}\ne 0\right)\wedge {B}\in ℕ\right)\to {P}\mathrm{pCnt}\left(\frac{{A}}{{B}}\right)=\left({P}\mathrm{pCnt}{A}\right)-\left({P}\mathrm{pCnt}{B}\right)$