Metamath Proof Explorer

Theorem ppivalnnnprm

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

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

Proof

Step Hyp Ref Expression
1 uzp1 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N = 2 \/ N e. ( ZZ>= ` ( 2 + 1 ) ) ) )
2 neleq1 
 |-  ( N = 2 -> ( N e/ Prime <-> 2 e/ Prime ) )
3 2prm 
 |-  2 e. Prime
4 pm2.24nel 
 |-  ( 2 e. Prime -> ( 2 e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
5 3 4 ax-mp 
 |-  ( 2 e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )
6 2 5 biimtrdi 
 |-  ( N = 2 -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
7 uzp1 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N = 3 \/ N e. ( ZZ>= ` ( 3 + 1 ) ) ) )
8 neleq1 
 |-  ( N = 3 -> ( N e/ Prime <-> 3 e/ Prime ) )
9 3prm 
 |-  3 e. Prime
10 pm2.24nel 
 |-  ( 3 e. Prime -> ( 3 e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
11 9 10 ax-mp 
 |-  ( 3 e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )
12 8 11 biimtrdi 
 |-  ( N = 3 -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
13 uzp1 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N = 4 \/ N e. ( ZZ>= ` ( 4 + 1 ) ) ) )
14 fvoveq1 
 |-  ( N = 4 -> ( ! ` ( N - 1 ) ) = ( ! ` ( 4 - 1 ) ) )
15 14 oveq1d 
 |-  ( N = 4 -> ( ( ! ` ( N - 1 ) ) + 1 ) = ( ( ! ` ( 4 - 1 ) ) + 1 ) )
16 id 
 |-  ( N = 4 -> N = 4 )
17 15 16 oveq12d 
 |-  ( N = 4 -> ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) = ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) )
18 14 16 oveq12d 
 |-  ( N = 4 -> ( ( ! ` ( N - 1 ) ) / N ) = ( ( ! ` ( 4 - 1 ) ) / 4 ) )
19 18 fveq2d 
 |-  ( N = 4 -> ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) = ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) )
20 17 19 oveq12d 
 |-  ( N = 4 -> ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) = ( ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) - ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) ) )
21 20 fveq2d 
 |-  ( N = 4 -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = ( |_ ` ( ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) - ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) ) ) )
22 ppivalnn4 
 |-  ( |_ ` ( ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) - ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) ) ) = 0
23 21 22 eqtrdi 
 |-  ( N = 4 -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )
24 23 a1d 
 |-  ( N = 4 -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
25 uzp1 
 |-  ( N e. ( ZZ>= ` 5 ) -> ( N = 5 \/ N e. ( ZZ>= ` ( 5 + 1 ) ) ) )
26 neleq1 
 |-  ( N = 5 -> ( N e/ Prime <-> 5 e/ Prime ) )
27 5prm 
 |-  5 e. Prime
28 pm2.24nel 
 |-  ( 5 e. Prime -> ( 5 e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
29 27 28 ax-mp 
 |-  ( 5 e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )
30 26 29 biimtrdi 
 |-  ( N = 5 -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
31 ppivalnnnprmge6 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ N e/ Prime ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )
32 31 ex 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
33 5p1e6 
 |-  ( 5 + 1 ) = 6
34 33 fveq2i 
 |-  ( ZZ>= ` ( 5 + 1 ) ) = ( ZZ>= ` 6 )
35 32 34 eleq2s 
 |-  ( N e. ( ZZ>= ` ( 5 + 1 ) ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
36 30 35 jaoi 
 |-  ( ( N = 5 \/ N e. ( ZZ>= ` ( 5 + 1 ) ) ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
37 25 36 syl 
 |-  ( N e. ( ZZ>= ` 5 ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
38 4p1e5 
 |-  ( 4 + 1 ) = 5
39 38 fveq2i 
 |-  ( ZZ>= ` ( 4 + 1 ) ) = ( ZZ>= ` 5 )
40 37 39 eleq2s 
 |-  ( N e. ( ZZ>= ` ( 4 + 1 ) ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
41 24 40 jaoi 
 |-  ( ( N = 4 \/ N e. ( ZZ>= ` ( 4 + 1 ) ) ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
42 13 41 syl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
43 3p1e4 
 |-  ( 3 + 1 ) = 4
44 43 fveq2i 
 |-  ( ZZ>= ` ( 3 + 1 ) ) = ( ZZ>= ` 4 )
45 42 44 eleq2s 
 |-  ( N e. ( ZZ>= ` ( 3 + 1 ) ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
46 12 45 jaoi 
 |-  ( ( N = 3 \/ N e. ( ZZ>= ` ( 3 + 1 ) ) ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
47 7 46 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
48 2p1e3 
 |-  ( 2 + 1 ) = 3
49 48 fveq2i 
 |-  ( ZZ>= ` ( 2 + 1 ) ) = ( ZZ>= ` 3 )
50 47 49 eleq2s 
 |-  ( N e. ( ZZ>= ` ( 2 + 1 ) ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
51 6 50 jaoi 
 |-  ( ( N = 2 \/ N e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
52 1 51 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N e/ Prime -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 ) )
53 52 imp 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ N e/ Prime ) -> ( |_ ` ( ( ( ( ! ` ( N - 1 ) ) + 1 ) / N ) - ( |_ ` ( ( ! ` ( N - 1 ) ) / N ) ) ) ) = 0 )