Metamath Proof Explorer

Theorem ppivalnnprm

Description: Value of a term of the prime-counting function pi for positive integers, according to Ján Mináč, for a prime number. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion ppivalnnprm 
|- ( P e. Prime -> ( |_ ` ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 wilth 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ P || ( ( ! ` ( P - 1 ) ) + 1 ) ) )
2 eluzelz 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. ZZ )
3 eluz2nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN )
4 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
5 3 4 syl 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 1 ) e. NN0 )
6 5 faccld 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ! ` ( P - 1 ) ) e. NN )
7 6 nnzd 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ! ` ( P - 1 ) ) e. ZZ )
8 7 peano2zd 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( ! ` ( P - 1 ) ) + 1 ) e. ZZ )
9 divides 
 |-  ( ( P e. ZZ /\ ( ( ! ` ( P - 1 ) ) + 1 ) e. ZZ ) -> ( P || ( ( ! ` ( P - 1 ) ) + 1 ) <-> E. m e. ZZ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) )
10 2 8 9 syl2anc 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P || ( ( ! ` ( P - 1 ) ) + 1 ) <-> E. m e. ZZ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) )
11 oveq1 
 |-  ( ( ( ! ` ( P - 1 ) ) + 1 ) = ( m x. P ) -> ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) = ( ( m x. P ) / P ) )
12 11 eqcoms 
 |-  ( ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) -> ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) = ( ( m x. P ) / P ) )
13 zcn 
 |-  ( m e. ZZ -> m e. CC )
14 13 adantl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> m e. CC )
15 eluzelcn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. CC )
16 15 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> P e. CC )
17 eluz2n0 
 |-  ( P e. ( ZZ>= ` 2 ) -> P =/= 0 )
18 17 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> P =/= 0 )
19 14 16 18 divcan4d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( ( m x. P ) / P ) = m )
20 12 19 sylan9eqr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) = m )
21 6 nncnd 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ! ` ( P - 1 ) ) e. CC )
22 pncan1 
 |-  ( ( ! ` ( P - 1 ) ) e. CC -> ( ( ( ! ` ( P - 1 ) ) + 1 ) - 1 ) = ( ! ` ( P - 1 ) ) )
23 21 22 syl 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( ( ! ` ( P - 1 ) ) + 1 ) - 1 ) = ( ! ` ( P - 1 ) ) )
24 23 eqcomd 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ! ` ( P - 1 ) ) = ( ( ( ! ` ( P - 1 ) ) + 1 ) - 1 ) )
25 24 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( ! ` ( P - 1 ) ) = ( ( ( ! ` ( P - 1 ) ) + 1 ) - 1 ) )
26 oveq1 
 |-  ( ( ( ! ` ( P - 1 ) ) + 1 ) = ( m x. P ) -> ( ( ( ! ` ( P - 1 ) ) + 1 ) - 1 ) = ( ( m x. P ) - 1 ) )
27 26 eqcoms 
 |-  ( ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) -> ( ( ( ! ` ( P - 1 ) ) + 1 ) - 1 ) = ( ( m x. P ) - 1 ) )
28 25 27 sylan9eq 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( ! ` ( P - 1 ) ) = ( ( m x. P ) - 1 ) )
29 28 oveq1d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( ( ! ` ( P - 1 ) ) / P ) = ( ( ( m x. P ) - 1 ) / P ) )
30 simpr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> m e. ZZ )
31 2 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> P e. ZZ )
32 30 31 zmulcld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( m x. P ) e. ZZ )
33 32 zcnd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( m x. P ) e. CC )
34 1cnd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> 1 e. CC )
35 33 34 16 18 divsubdird 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( ( ( m x. P ) - 1 ) / P ) = ( ( ( m x. P ) / P ) - ( 1 / P ) ) )
36 19 oveq1d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( ( ( m x. P ) / P ) - ( 1 / P ) ) = ( m - ( 1 / P ) ) )
37 35 36 eqtrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( ( ( m x. P ) - 1 ) / P ) = ( m - ( 1 / P ) ) )
38 37 adantr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( ( ( m x. P ) - 1 ) / P ) = ( m - ( 1 / P ) ) )
39 29 38 eqtrd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( ( ! ` ( P - 1 ) ) / P ) = ( m - ( 1 / P ) ) )
40 39 fveq2d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) = ( |_ ` ( m - ( 1 / P ) ) ) )
41 3 anim1ci 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( m e. ZZ /\ P e. NN ) )
42 flmrecm1 
 |-  ( ( m e. ZZ /\ P e. NN ) -> ( |_ ` ( m - ( 1 / P ) ) ) = ( m - 1 ) )
43 41 42 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( |_ ` ( m - ( 1 / P ) ) ) = ( m - 1 ) )
44 43 adantr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( |_ ` ( m - ( 1 / P ) ) ) = ( m - 1 ) )
45 40 44 eqtrd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) = ( m - 1 ) )
46 20 45 oveq12d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) = ( m - ( m - 1 ) ) )
47 46 fveq2d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( |_ ` ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) ) = ( |_ ` ( m - ( m - 1 ) ) ) )
48 1cnd 
 |-  ( m e. ZZ -> 1 e. CC )
49 13 48 nncand 
 |-  ( m e. ZZ -> ( m - ( m - 1 ) ) = 1 )
50 49 fveq2d 
 |-  ( m e. ZZ -> ( |_ ` ( m - ( m - 1 ) ) ) = ( |_ ` 1 ) )
51 1z 
 |-  1 e. ZZ
52 flid 
 |-  ( 1 e. ZZ -> ( |_ ` 1 ) = 1 )
53 51 52 mp1i 
 |-  ( m e. ZZ -> ( |_ ` 1 ) = 1 )
54 50 53 eqtrd 
 |-  ( m e. ZZ -> ( |_ ` ( m - ( m - 1 ) ) ) = 1 )
55 54 adantl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( |_ ` ( m - ( m - 1 ) ) ) = 1 )
56 55 adantr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( |_ ` ( m - ( m - 1 ) ) ) = 1 )
57 47 56 eqtrd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) /\ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( |_ ` ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) ) = 1 )
58 57 ex 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) -> ( |_ ` ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) ) = 1 ) )
59 58 rexlimdva 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( E. m e. ZZ ( m x. P ) = ( ( ! ` ( P - 1 ) ) + 1 ) -> ( |_ ` ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) ) = 1 ) )
60 10 59 sylbid 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P || ( ( ! ` ( P - 1 ) ) + 1 ) -> ( |_ ` ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) ) = 1 ) )
61 60 imp 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ P || ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( |_ ` ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) ) = 1 )
62 1 61 sylbi 
 |-  ( P e. Prime -> ( |_ ` ( ( ( ( ! ` ( P - 1 ) ) + 1 ) / P ) - ( |_ ` ( ( ! ` ( P - 1 ) ) / P ) ) ) ) = 1 )