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 𝑁 ) = 𝑆 )