Metamath Proof Explorer

Theorem pcdiv

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

Ref Expression
Assertion pcdiv ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → 𝑃 ∈ ℙ )
2 simp2l ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℤ )
3 simp3 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℕ )
4 znq ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℚ )
5 2 3 4 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℚ )
6 2 zcnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℂ )
7 3 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℂ )
8 simp2r ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → 𝐴 ≠ 0 )
9 3 nnne0d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → 𝐵 ≠ 0 )
10 6 7 8 9 divne0d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ≠ 0 )
11 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
12 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
13 11 12 pcval ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 / 𝐵 ) ∈ ℚ ∧ ( 𝐴 / 𝐵 ) ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
14 1 5 10 13 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
15 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < )
16 15 pczpre ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) )
17 16 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( 𝑃 pCnt 𝐴 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) )
18 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
19 nnne0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
20 18 19 jca ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) )
21 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < )
22 21 pczpre ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) )
23 20 22 sylan2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( 𝑃 pCnt 𝐵 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) )
24 23 3adant2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( 𝑃 pCnt 𝐵 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) )
25 17 24 oveq12d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) ) )
26 eqid ⊢ ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝐵 )
27 25 26 jctil ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝐵 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) ) ) )
28 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 / 𝑦 ) = ( 𝐴 / 𝑦 ) )
29 28 eqeq2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ↔ ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝑦 ) ) )
30 breq2 ⊢ ( 𝑥 = 𝐴 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 ) )
31 30 rabbidv ⊢ ( 𝑥 = 𝐴 → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } )
32 31 supeq1d ⊢ ( 𝑥 = 𝐴 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) )
33 32 oveq1d ⊢ ( 𝑥 = 𝐴 → ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) )
34 33 eqeq2d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ↔ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
35 29 34 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
36 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 / 𝑦 ) = ( 𝐴 / 𝐵 ) )
37 36 eqeq2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝑦 ) ↔ ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝐵 ) ) )
38 breq2 ⊢ ( 𝑦 = 𝐵 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 ) )
39 38 rabbidv ⊢ ( 𝑦 = 𝐵 → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } )
40 39 supeq1d ⊢ ( 𝑦 = 𝐵 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) )
41 40 oveq2d ⊢ ( 𝑦 = 𝐵 → ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) ) )
42 41 eqeq2d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ↔ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) ) ) )
43 37 42 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝐵 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) ) ) ) )
44 35 43 rspc2ev ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ∧ ( ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝐵 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
45 2 3 27 44 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
46 ovex ⊢ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) ∈ V
47 11 12 pceu ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 / 𝐵 ) ∈ ℚ ∧ ( 𝐴 / 𝐵 ) ≠ 0 ) ) → ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
48 1 5 10 47 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
49 eqeq1 ⊢ ( 𝑧 = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) → ( 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ↔ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
50 49 anbi2d ⊢ ( 𝑧 = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) → ( ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
51 50 2rexbidv ⊢ ( 𝑧 = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
52 51 iota2 ⊢ ( ( ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) ∈ V ∧ ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) ) )
53 46 48 52 sylancr ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) ) )
54 45 53 mpbid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) )
55 14 54 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℕ ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) )