Metamath Proof Explorer

Theorem ppivalnnnprmge6

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

Ref Expression
Assertion ppivalnnnprmge6 
|- ( ( N e. ( ZZ>= ` 6 ) /\ N e/ Prime ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 nprmdvdsfacm1 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ N e/ Prime ) -> N || ( ! ` ( N - 1 ) ) )
2 eluzelz 
 |-  ( N e. ( ZZ>= ` 6 ) -> N e. ZZ )
3 6nn 
 |-  6 e. NN
4 elnnuz 
 |-  ( 6 e. NN <-> 6 e. ( ZZ>= ` 1 ) )
5 3 4 mpbi 
 |-  6 e. ( ZZ>= ` 1 )
6 uzss 
 |-  ( 6 e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 6 ) C_ ( ZZ>= ` 1 ) )
7 5 6 ax-mp 
 |-  ( ZZ>= ` 6 ) C_ ( ZZ>= ` 1 )
8 7 sseli 
 |-  ( N e. ( ZZ>= ` 6 ) -> N e. ( ZZ>= ` 1 ) )
9 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
10 8 9 sylibr 
 |-  ( N e. ( ZZ>= ` 6 ) -> N e. NN )
11 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
12 10 11 syl 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( N - 1 ) e. NN0 )
13 12 faccld 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( ! ` ( N - 1 ) ) e. NN )
14 13 nnzd 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( ! ` ( N - 1 ) ) e. ZZ )
15 divides 
 |-  ( ( N e. ZZ /\ ( ! ` ( N - 1 ) ) e. ZZ ) -> ( N || ( ! ` ( N - 1 ) ) <-> E. m e. ZZ ( m x. N ) = ( ! ` ( N - 1 ) ) ) )
16 2 14 15 syl2anc 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( N || ( ! ` ( N - 1 ) ) <-> E. m e. ZZ ( m x. N ) = ( ! ` ( N - 1 ) ) ) )
17 oveq1 
 |-  ( ( ! ` ( N - 1 ) ) = ( m x. N ) -> ( ( ! ` ( N - 1 ) ) + 1 ) = ( ( m x. N ) + 1 ) )
18 17 oveq1d 
 |-  ( ( ! ` ( N - 1 ) ) = ( m x. N ) -> ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) = ( ( ( m x. N ) + 1 ) / N ) )
19 fvoveq1 
 |-  ( ( ! ` ( N - 1 ) ) = ( m x. N ) -> ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) = ( |_ ` ( ( m x. N ) / N ) ) )
20 18 19 oveq12d 
 |-  ( ( ! ` ( N - 1 ) ) = ( m x. N ) -> ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) = ( ( ( ( m x. N ) + 1 ) / N ) - ( |_ ` ( ( m x. N ) / N ) ) ) )
21 20 fveq2d 
 |-  ( ( ! ` ( N - 1 ) ) = ( m x. N ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = ( |_ ` ( ( ( ( m x. N ) + 1 ) / N ) - ( |_ ` ( ( m x. N ) / N ) ) ) ) )
22 21 eqcoms 
 |-  ( ( m x. N ) = ( ! ` ( N - 1 ) ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = ( |_ ` ( ( ( ( m x. N ) + 1 ) / N ) - ( |_ ` ( ( m x. N ) / N ) ) ) ) )
23 zcn 
 |-  ( m e. ZZ -> m e. CC )
24 23 adantl 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> m e. CC )
25 eluzelcn 
 |-  ( N e. ( ZZ>= ` 6 ) -> N e. CC )
26 25 adantr 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> N e. CC )
27 1cnd 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> 1 e. CC )
28 10 nnne0d 
 |-  ( N e. ( ZZ>= ` 6 ) -> N =/= 0 )
29 28 adantr 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> N =/= 0 )
30 24 26 27 29 muldivdid 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( ( ( m x. N ) + 1 ) / N ) = ( m + ( 1 / N ) ) )
31 24 26 29 divcan4d 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( ( m x. N ) / N ) = m )
32 31 fveq2d 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( |_ ` ( ( m x. N ) / N ) ) = ( |_ ` m ) )
33 flid 
 |-  ( m e. ZZ -> ( |_ ` m ) = m )
34 33 adantl 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( |_ ` m ) = m )
35 32 34 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( |_ ` ( ( m x. N ) / N ) ) = m )
36 30 35 oveq12d 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( ( ( ( m x. N ) + 1 ) / N ) - ( |_ ` ( ( m x. N ) / N ) ) ) = ( ( m + ( 1 / N ) ) - m ) )
37 36 fveq2d 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( |_ ` ( ( ( ( m x. N ) + 1 ) / N ) - ( |_ ` ( ( m x. N ) / N ) ) ) ) = ( |_ ` ( ( m + ( 1 / N ) ) - m ) ) )
38 25 28 reccld 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( 1 / N ) e. CC )
39 38 adantr 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( 1 / N ) e. CC )
40 24 39 pncan2d 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( ( m + ( 1 / N ) ) - m ) = ( 1 / N ) )
41 40 fveq2d 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( |_ ` ( ( m + ( 1 / N ) ) - m ) ) = ( |_ ` ( 1 / N ) ) )
42 2z 
 |-  2 e. ZZ
43 3 nnzi 
 |-  6 e. ZZ
44 2re 
 |-  2 e. RR
45 6re 
 |-  6 e. RR
46 2lt6 
 |-  2 < 6
47 44 45 46 ltleii 
 |-  2 <_ 6
48 eluz2 
 |-  ( 6 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 6 e. ZZ /\ 2 <_ 6 ) )
49 42 43 47 48 mpbir3an 
 |-  6 e. ( ZZ>= ` 2 )
50 uzss 
 |-  ( 6 e. ( ZZ>= ` 2 ) -> ( ZZ>= ` 6 ) C_ ( ZZ>= ` 2 ) )
51 49 50 ax-mp 
 |-  ( ZZ>= ` 6 ) C_ ( ZZ>= ` 2 )
52 51 sseli 
 |-  ( N e. ( ZZ>= ` 6 ) -> N e. ( ZZ>= ` 2 ) )
53 nnge2recfl0 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( 1 / N ) ) = 0 )
54 52 53 syl 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( |_ ` ( 1 / N ) ) = 0 )
55 54 adantr 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( |_ ` ( 1 / N ) ) = 0 )
56 37 41 55 3eqtrd 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( |_ ` ( ( ( ( m x. N ) + 1 ) / N ) - ( |_ ` ( ( m x. N ) / N ) ) ) ) = 0 )
57 22 56 sylan9eqr 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) /\ ( m x. N ) = ( ! ` ( N - 1 ) ) ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )
58 57 ex 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ m e. ZZ ) -> ( ( m x. N ) = ( ! ` ( N - 1 ) ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
59 58 rexlimdva 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( E. m e. ZZ ( m x. N ) = ( ! ` ( N - 1 ) ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
60 16 59 sylbid 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( N || ( ! ` ( N - 1 ) ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
61 60 adantr 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ N e/ Prime ) -> ( N || ( ! ` ( N - 1 ) ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
62 1 61 mpd 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ N e/ Prime ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )