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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑁 ∉ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 nprmdvdsfacm1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑁 ∉ ℙ ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
2 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ℤ )
3 6nn ⊢ 6 ∈ ℕ
4 elnnuz ⊢ ( 6 ∈ ℕ ↔ 6 ∈ ( ℤ≥ ‘ 1 ) )
5 3 4 mpbi ⊢ 6 ∈ ( ℤ≥ ‘ 1 )
6 uzss ⊢ ( 6 ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 6 ) ⊆ ( ℤ≥ ‘ 1 ) )
7 5 6 ax-mp ⊢ ( ℤ≥ ‘ 6 ) ⊆ ( ℤ≥ ‘ 1 )
8 7 sseli ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
9 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
10 8 9 sylibr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ℕ )
11 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
12 10 11 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( 𝑁 − 1 ) ∈ ℕ0 )
13 12 faccld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ )
14 13 nnzd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ )
15 divides ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ ) → ( 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ↔ ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝑁 ) = ( ! ‘ ( 𝑁 − 1 ) ) ) )
16 2 14 15 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ↔ ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝑁 ) = ( ! ‘ ( 𝑁 − 1 ) ) ) )
17 oveq1 ⊢ ( ( ! ‘ ( 𝑁 − 1 ) ) = ( 𝑚 · 𝑁 ) → ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) = ( ( 𝑚 · 𝑁 ) + 1 ) )
18 17 oveq1d ⊢ ( ( ! ‘ ( 𝑁 − 1 ) ) = ( 𝑚 · 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) = ( ( ( 𝑚 · 𝑁 ) + 1 ) / 𝑁 ) )
19 fvoveq1 ⊢ ( ( ! ‘ ( 𝑁 − 1 ) ) = ( 𝑚 · 𝑁 ) → ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) = ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) )
20 18 19 oveq12d ⊢ ( ( ! ‘ ( 𝑁 − 1 ) ) = ( 𝑚 · 𝑁 ) → ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) = ( ( ( ( 𝑚 · 𝑁 ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) ) )
21 20 fveq2d ⊢ ( ( ! ‘ ( 𝑁 − 1 ) ) = ( 𝑚 · 𝑁 ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = ( ⌊ ‘ ( ( ( ( 𝑚 · 𝑁 ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) ) ) )
22 21 eqcoms ⊢ ( ( 𝑚 · 𝑁 ) = ( ! ‘ ( 𝑁 − 1 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = ( ⌊ ‘ ( ( ( ( 𝑚 · 𝑁 ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) ) ) )
23 zcn ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℂ )
24 23 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℂ )
25 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ℂ )
26 25 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → 𝑁 ∈ ℂ )
27 1cnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → 1 ∈ ℂ )
28 10 nnne0d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ≠ 0 )
29 28 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → 𝑁 ≠ 0 )
30 24 26 27 29 muldivdid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ( ( 𝑚 · 𝑁 ) + 1 ) / 𝑁 ) = ( 𝑚 + ( 1 / 𝑁 ) ) )
31 24 26 29 divcan4d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑚 · 𝑁 ) / 𝑁 ) = 𝑚 )
32 31 fveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) = ( ⌊ ‘ 𝑚 ) )
33 flid ⊢ ( 𝑚 ∈ ℤ → ( ⌊ ‘ 𝑚 ) = 𝑚 )
34 33 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ 𝑚 ) = 𝑚 )
35 32 34 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) = 𝑚 )
36 30 35 oveq12d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 𝑚 · 𝑁 ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) ) = ( ( 𝑚 + ( 1 / 𝑁 ) ) − 𝑚 ) )
37 36 fveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ ( ( ( ( 𝑚 · 𝑁 ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) ) ) = ( ⌊ ‘ ( ( 𝑚 + ( 1 / 𝑁 ) ) − 𝑚 ) ) )
38 25 28 reccld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( 1 / 𝑁 ) ∈ ℂ )
39 38 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( 1 / 𝑁 ) ∈ ℂ )
40 24 39 pncan2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑚 + ( 1 / 𝑁 ) ) − 𝑚 ) = ( 1 / 𝑁 ) )
41 40 fveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝑚 + ( 1 / 𝑁 ) ) − 𝑚 ) ) = ( ⌊ ‘ ( 1 / 𝑁 ) ) )
42 2z ⊢ 2 ∈ ℤ
43 3 nnzi ⊢ 6 ∈ ℤ
44 2re ⊢ 2 ∈ ℝ
45 6re ⊢ 6 ∈ ℝ
46 2lt6 ⊢ 2 < 6
47 44 45 46 ltleii ⊢ 2 ≤ 6
48 eluz2 ⊢ ( 6 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 6 ∈ ℤ ∧ 2 ≤ 6 ) )
49 42 43 47 48 mpbir3an ⊢ 6 ∈ ( ℤ≥ ‘ 2 )
50 uzss ⊢ ( 6 ∈ ( ℤ≥ ‘ 2 ) → ( ℤ≥ ‘ 6 ) ⊆ ( ℤ≥ ‘ 2 ) )
51 49 50 ax-mp ⊢ ( ℤ≥ ‘ 6 ) ⊆ ( ℤ≥ ‘ 2 )
52 51 sseli ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
53 nnge2recfl0 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 1 / 𝑁 ) ) = 0 )
54 52 53 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( ⌊ ‘ ( 1 / 𝑁 ) ) = 0 )
55 54 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ ( 1 / 𝑁 ) ) = 0 )
56 37 41 55 3eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ ( ( ( ( 𝑚 · 𝑁 ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( 𝑚 · 𝑁 ) / 𝑁 ) ) ) ) = 0 )
57 22 56 sylan9eqr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑁 ) = ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )
58 57 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑚 · 𝑁 ) = ( ! ‘ ( 𝑁 − 1 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
59 58 rexlimdva ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝑁 ) = ( ! ‘ ( 𝑁 − 1 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
60 16 59 sylbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
61 60 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑁 ∉ ℙ ) → ( 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
62 1 61 mpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑁 ∉ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )