This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pczpre

Description: Connect the prime count pre-function to the actual prime count function, when restricted to the integers. (Contributed by Mario Carneiro, 23-Feb-2014) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis pczpre.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < )
Assertion pczpre ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 pczpre.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < )
2 zq ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℚ )
3 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
4 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
5 3 4 pcval ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
6 2 5 sylanr1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) = ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
7 simprl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℤ )
8 7 zcnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℂ )
9 8 div1d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑁 / 1 ) = 𝑁 )
10 9 eqcomd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑁 = ( 𝑁 / 1 ) )
11 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
12 eqid ⊢ 1 = 1
13 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 }
14 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < )
15 13 14 pcpre1 ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 = 1 ) → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) = 0 )
16 11 12 15 sylancl ⊢ ( 𝑃 ∈ ℙ → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) = 0 )
17 16 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) = 0 )
18 17 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) ) = ( 𝑆 − 0 ) )
19 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
20 19 1 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )
21 11 20 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )
22 21 simpld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑆 ∈ ℕ0 )
23 22 nn0cnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑆 ∈ ℂ )
24 23 subid1d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 − 0 ) = 𝑆 )
25 18 24 eqtr2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) ) )
26 1nn ⊢ 1 ∈ ℕ
27 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 / 𝑦 ) = ( 𝑁 / 𝑦 ) )
28 27 eqeq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑁 = ( 𝑥 / 𝑦 ) ↔ 𝑁 = ( 𝑁 / 𝑦 ) ) )
29 breq2 ⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 ) )
30 29 rabbidv ⊢ ( 𝑥 = 𝑁 → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } )
31 30 supeq1d ⊢ ( 𝑥 = 𝑁 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) )
32 31 1 eqtr4di ⊢ ( 𝑥 = 𝑁 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) = 𝑆 )
33 32 oveq1d ⊢ ( 𝑥 = 𝑁 → ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) )
34 33 eqeq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ↔ 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
35 28 34 anbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( 𝑁 = ( 𝑁 / 𝑦 ) ∧ 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
36 oveq2 ⊢ ( 𝑦 = 1 → ( 𝑁 / 𝑦 ) = ( 𝑁 / 1 ) )
37 36 eqeq2d ⊢ ( 𝑦 = 1 → ( 𝑁 = ( 𝑁 / 𝑦 ) ↔ 𝑁 = ( 𝑁 / 1 ) ) )
38 breq2 ⊢ ( 𝑦 = 1 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 1 ) )
39 38 rabbidv ⊢ ( 𝑦 = 1 → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } )
40 39 supeq1d ⊢ ( 𝑦 = 1 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) )
41 40 oveq2d ⊢ ( 𝑦 = 1 → ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) ) )
42 41 eqeq2d ⊢ ( 𝑦 = 1 → ( 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ↔ 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) ) ) )
43 37 42 anbi12d ⊢ ( 𝑦 = 1 → ( ( 𝑁 = ( 𝑁 / 𝑦 ) ∧ 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( 𝑁 = ( 𝑁 / 1 ) ∧ 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) ) ) ) )
44 35 43 rspc2ev ⊢ ( ( 𝑁 ∈ ℤ ∧ 1 ∈ ℕ ∧ ( 𝑁 = ( 𝑁 / 1 ) ∧ 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
45 26 44 mp3an2 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 = ( 𝑁 / 1 ) ∧ 𝑆 = ( 𝑆 − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
46 7 10 25 45 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
47 ltso ⊢ < Or ℝ
48 47 supex ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) ∈ V
49 1 48 eqeltri ⊢ 𝑆 ∈ V
50 3 4 pceu ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ) → ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
51 2 50 sylanr1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
52 eqeq1 ⊢ ( 𝑧 = 𝑆 → ( 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ↔ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
53 52 anbi2d ⊢ ( 𝑧 = 𝑆 → ( ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
54 53 2rexbidv ⊢ ( 𝑧 = 𝑆 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
55 54 iota2 ⊢ ( ( 𝑆 ∈ V ∧ ∃! 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) = 𝑆 ) )
56 49 51 55 sylancr ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑆 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ↔ ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) = 𝑆 ) )
57 46 56 mpbid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑁 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) = 𝑆 )
58 6 57 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) = 𝑆 )