Metamath Proof Explorer

Theorem ppivalnn4

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

Ref Expression
Assertion ppivalnn4 
|- ( |_ ` ( ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) - ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) ) ) = 0

Proof

Step Hyp Ref Expression
1 4m1e3 
 |-  ( 4 - 1 ) = 3
2 1 fveq2i 
 |-  ( ! ` ( 4 - 1 ) ) = ( ! ` 3 )
3 fac3 
 |-  ( ! ` 3 ) = 6
4 2 3 eqtri 
 |-  ( ! ` ( 4 - 1 ) ) = 6
5 4 oveq1i 
 |-  ( ( ! ` ( 4 - 1 ) ) + 1 ) = ( 6 + 1 )
6 6p1e7 
 |-  ( 6 + 1 ) = 7
7 5 6 eqtri 
 |-  ( ( ! ` ( 4 - 1 ) ) + 1 ) = 7
8 7 oveq1i 
 |-  ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) = ( 7 / 4 )
9 4 oveq1i 
 |-  ( ( ! ` ( 4 - 1 ) ) / 4 ) = ( 6 / 4 )
10 9 fveq2i 
 |-  ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) = ( |_ ` ( 6 / 4 ) )
11 3t2e6 
 |-  ( 3 x. 2 ) = 6
12 2t2e4 
 |-  ( 2 x. 2 ) = 4
13 11 12 oveq12i 
 |-  ( ( 3 x. 2 ) / ( 2 x. 2 ) ) = ( 6 / 4 )
14 2ne0 
 |-  2 =/= 0
15 3cn 
 |-  3 e. CC
16 15 a1i 
 |-  ( 2 =/= 0 -> 3 e. CC )
17 2cnd 
 |-  ( 2 =/= 0 -> 2 e. CC )
18 id 
 |-  ( 2 =/= 0 -> 2 =/= 0 )
19 16 17 17 18 18 divcan5rd 
 |-  ( 2 =/= 0 -> ( ( 3 x. 2 ) / ( 2 x. 2 ) ) = ( 3 / 2 ) )
20 14 19 ax-mp 
 |-  ( ( 3 x. 2 ) / ( 2 x. 2 ) ) = ( 3 / 2 )
21 13 20 eqtr3i 
 |-  ( 6 / 4 ) = ( 3 / 2 )
22 21 fveq2i 
 |-  ( |_ ` ( 6 / 4 ) ) = ( |_ ` ( 3 / 2 ) )
23 ex-fl 
 |-  ( ( |_ ` ( 3 / 2 ) ) = 1 /\ ( |_ ` -u ( 3 / 2 ) ) = -u 2 )
24 23 simpli 
 |-  ( |_ ` ( 3 / 2 ) ) = 1
25 10 22 24 3eqtri 
 |-  ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) = 1
26 8 25 oveq12i 
 |-  ( ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) - ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) ) = ( ( 7 / 4 ) - 1 )
27 26 fveq2i 
 |-  ( |_ ` ( ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) - ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) ) ) = ( |_ ` ( ( 7 / 4 ) - 1 ) )
28 4cn 
 |-  4 e. CC
29 4ne0 
 |-  4 =/= 0
30 28 29 dividi 
 |-  ( 4 / 4 ) = 1
31 30 eqcomi 
 |-  1 = ( 4 / 4 )
32 31 oveq2i 
 |-  ( ( 7 / 4 ) - 1 ) = ( ( 7 / 4 ) - ( 4 / 4 ) )
33 7cn 
 |-  7 e. CC
34 28 29 pm3.2i 
 |-  ( 4 e. CC /\ 4 =/= 0 )
35 divsubdir 
 |-  ( ( 7 e. CC /\ 4 e. CC /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( 7 - 4 ) / 4 ) = ( ( 7 / 4 ) - ( 4 / 4 ) ) )
36 33 28 34 35 mp3an 
 |-  ( ( 7 - 4 ) / 4 ) = ( ( 7 / 4 ) - ( 4 / 4 ) )
37 4p3e7 
 |-  ( 4 + 3 ) = 7
38 37 eqcomi 
 |-  7 = ( 4 + 3 )
39 28 15 38 mvrladdi 
 |-  ( 7 - 4 ) = 3
40 39 oveq1i 
 |-  ( ( 7 - 4 ) / 4 ) = ( 3 / 4 )
41 36 40 eqtr3i 
 |-  ( ( 7 / 4 ) - ( 4 / 4 ) ) = ( 3 / 4 )
42 32 41 eqtri 
 |-  ( ( 7 / 4 ) - 1 ) = ( 3 / 4 )
43 42 fveq2i 
 |-  ( |_ ` ( ( 7 / 4 ) - 1 ) ) = ( |_ ` ( 3 / 4 ) )
44 3lt4 
 |-  3 < 4
45 3nn0 
 |-  3 e. NN0
46 4nn 
 |-  4 e. NN
47 divfl0 
 |-  ( ( 3 e. NN0 /\ 4 e. NN ) -> ( 3 < 4 <-> ( |_ ` ( 3 / 4 ) ) = 0 ) )
48 45 46 47 mp2an 
 |-  ( 3 < 4 <-> ( |_ ` ( 3 / 4 ) ) = 0 )
49 44 48 mpbi 
 |-  ( |_ ` ( 3 / 4 ) ) = 0
50 27 43 49 3eqtri 
 |-  ( |_ ` ( ( ( ( ! ` ( 4 - 1 ) ) + 1 ) / 4 ) - ( |_ ` ( ( ! ` ( 4 - 1 ) ) / 4 ) ) ) ) = 0