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 ( 𝑃 ∈ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 wilth ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) )
2 eluzelz ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℤ )
3 eluz2nn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ )
4 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
5 3 4 syl ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ0 )
6 5 faccld ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
7 6 nnzd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
8 7 peano2zd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ∈ ℤ )
9 divides ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) )
10 2 8 9 syl2anc ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) )
11 oveq1 ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) = ( 𝑚 · 𝑃 ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) = ( ( 𝑚 · 𝑃 ) / 𝑃 ) )
12 11 eqcoms ⊢ ( ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) = ( ( 𝑚 · 𝑃 ) / 𝑃 ) )
13 zcn ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℂ )
14 13 adantl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℂ )
15 eluzelcn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → 𝑃 ∈ ℂ )
17 eluz2n0 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ≠ 0 )
18 17 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → 𝑃 ≠ 0 )
19 14 16 18 divcan4d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑚 · 𝑃 ) / 𝑃 ) = 𝑚 )
20 12 19 sylan9eqr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) = 𝑚 )
21 6 nncnd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
22 pncan1 ⊢ ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ → ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) − 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
23 21 22 syl ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) − 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
24 23 eqcomd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ! ‘ ( 𝑃 − 1 ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) − 1 ) )
25 24 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( ! ‘ ( 𝑃 − 1 ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) − 1 ) )
26 oveq1 ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) = ( 𝑚 · 𝑃 ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) − 1 ) = ( ( 𝑚 · 𝑃 ) − 1 ) )
27 26 eqcoms ⊢ ( ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) − 1 ) = ( ( 𝑚 · 𝑃 ) − 1 ) )
28 25 27 sylan9eq ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) = ( ( 𝑚 · 𝑃 ) − 1 ) )
29 28 oveq1d ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) = ( ( ( 𝑚 · 𝑃 ) − 1 ) / 𝑃 ) )
30 simpr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
31 2 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → 𝑃 ∈ ℤ )
32 30 31 zmulcld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · 𝑃 ) ∈ ℤ )
33 32 zcnd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · 𝑃 ) ∈ ℂ )
34 1cnd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → 1 ∈ ℂ )
35 33 34 16 18 divsubdird ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( ( ( 𝑚 · 𝑃 ) − 1 ) / 𝑃 ) = ( ( ( 𝑚 · 𝑃 ) / 𝑃 ) − ( 1 / 𝑃 ) ) )
36 19 oveq1d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( ( ( 𝑚 · 𝑃 ) / 𝑃 ) − ( 1 / 𝑃 ) ) = ( 𝑚 − ( 1 / 𝑃 ) ) )
37 35 36 eqtrd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( ( ( 𝑚 · 𝑃 ) − 1 ) / 𝑃 ) = ( 𝑚 − ( 1 / 𝑃 ) ) )
38 37 adantr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ( ( 𝑚 · 𝑃 ) − 1 ) / 𝑃 ) = ( 𝑚 − ( 1 / 𝑃 ) ) )
39 29 38 eqtrd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) = ( 𝑚 − ( 1 / 𝑃 ) ) )
40 39 fveq2d ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) = ( ⌊ ‘ ( 𝑚 − ( 1 / 𝑃 ) ) ) )
41 3 anim1ci ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( 𝑚 ∈ ℤ ∧ 𝑃 ∈ ℕ ) )
42 flmrecm1 ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ⌊ ‘ ( 𝑚 − ( 1 / 𝑃 ) ) ) = ( 𝑚 − 1 ) )
43 41 42 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ ( 𝑚 − ( 1 / 𝑃 ) ) ) = ( 𝑚 − 1 ) )
44 43 adantr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ⌊ ‘ ( 𝑚 − ( 1 / 𝑃 ) ) ) = ( 𝑚 − 1 ) )
45 40 44 eqtrd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) = ( 𝑚 − 1 ) )
46 20 45 oveq12d ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) = ( 𝑚 − ( 𝑚 − 1 ) ) )
47 46 fveq2d ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) ) = ( ⌊ ‘ ( 𝑚 − ( 𝑚 − 1 ) ) ) )
48 1cnd ⊢ ( 𝑚 ∈ ℤ → 1 ∈ ℂ )
49 13 48 nncand ⊢ ( 𝑚 ∈ ℤ → ( 𝑚 − ( 𝑚 − 1 ) ) = 1 )
50 49 fveq2d ⊢ ( 𝑚 ∈ ℤ → ( ⌊ ‘ ( 𝑚 − ( 𝑚 − 1 ) ) ) = ( ⌊ ‘ 1 ) )
51 1z ⊢ 1 ∈ ℤ
52 flid ⊢ ( 1 ∈ ℤ → ( ⌊ ‘ 1 ) = 1 )
53 51 52 mp1i ⊢ ( 𝑚 ∈ ℤ → ( ⌊ ‘ 1 ) = 1 )
54 50 53 eqtrd ⊢ ( 𝑚 ∈ ℤ → ( ⌊ ‘ ( 𝑚 − ( 𝑚 − 1 ) ) ) = 1 )
55 54 adantl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( ⌊ ‘ ( 𝑚 − ( 𝑚 − 1 ) ) ) = 1 )
56 55 adantr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ⌊ ‘ ( 𝑚 − ( 𝑚 − 1 ) ) ) = 1 )
57 47 56 eqtrd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) ) = 1 )
58 57 ex ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) ) = 1 ) )
59 58 rexlimdva ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝑃 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) ) = 1 ) )
60 10 59 sylbid ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) ) = 1 ) )
61 60 imp ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) ) = 1 )
62 1 61 sylbi ⊢ ( 𝑃 ∈ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) / 𝑃 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑃 − 1 ) ) / 𝑃 ) ) ) ) = 1 )