This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ppiprm

Description: The prime-counting function ppi at a prime. (Contributed by Mario Carneiro, 19-Sep-2014)

Ref Expression
Assertion ppiprm ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ( π ‘ 𝐴 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... 𝐴 ) ∈ Fin )
2 inss1 ⊢ ( ( 2 ... 𝐴 ) ∩ ℙ ) ⊆ ( 2 ... 𝐴 )
3 ssfi ⊢ ( ( ( 2 ... 𝐴 ) ∈ Fin ∧ ( ( 2 ... 𝐴 ) ∩ ℙ ) ⊆ ( 2 ... 𝐴 ) ) → ( ( 2 ... 𝐴 ) ∩ ℙ ) ∈ Fin )
4 1 2 3 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... 𝐴 ) ∩ ℙ ) ∈ Fin )
5 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℝ )
7 6 ltp1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 < ( 𝐴 + 1 ) )
8 peano2z ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ )
9 8 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℤ )
10 9 zred ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℝ )
11 6 10 ltnled ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 < ( 𝐴 + 1 ) ↔ ¬ ( 𝐴 + 1 ) ≤ 𝐴 ) )
12 7 11 mpbid ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ¬ ( 𝐴 + 1 ) ≤ 𝐴 )
13 elinel1 ⊢ ( ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) → ( 𝐴 + 1 ) ∈ ( 2 ... 𝐴 ) )
14 elfzle2 ⊢ ( ( 𝐴 + 1 ) ∈ ( 2 ... 𝐴 ) → ( 𝐴 + 1 ) ≤ 𝐴 )
15 13 14 syl ⊢ ( ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) → ( 𝐴 + 1 ) ≤ 𝐴 )
16 12 15 nsyl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ¬ ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) )
17 ovex ⊢ ( 𝐴 + 1 ) ∈ V
18 hashunsng ⊢ ( ( 𝐴 + 1 ) ∈ V → ( ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∈ Fin ∧ ¬ ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) = ( ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) + 1 ) ) )
19 17 18 ax-mp ⊢ ( ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∈ Fin ∧ ¬ ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) = ( ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) + 1 ) )
20 4 16 19 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) = ( ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) + 1 ) )
21 ppival2 ⊢ ( ( 𝐴 + 1 ) ∈ ℤ → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) )
22 9 21 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) )
23 2z ⊢ 2 ∈ ℤ
24 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
25 24 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℂ )
26 ax-1cn ⊢ 1 ∈ ℂ
27 pncan ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
28 25 26 27 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
29 prmuz2 ⊢ ( ( 𝐴 + 1 ) ∈ ℙ → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
30 29 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
31 uz2m1nn ⊢ ( ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ )
32 30 31 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ )
33 28 32 eqeltrrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℕ )
34 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
35 2m1e1 ⊢ ( 2 − 1 ) = 1
36 35 fveq2i ⊢ ( ℤ≥ ‘ ( 2 − 1 ) ) = ( ℤ≥ ‘ 1 )
37 34 36 eqtr4i ⊢ ℕ = ( ℤ≥ ‘ ( 2 − 1 ) )
38 33 37 eleqtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) )
39 fzsuc2 ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) )
40 23 38 39 sylancr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) )
41 40 ineq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ∩ ℙ ) )
42 indir ⊢ ( ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) )
43 41 42 eqtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) ) )
44 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℙ )
45 44 snssd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → { ( 𝐴 + 1 ) } ⊆ ℙ )
46 dfss2 ⊢ ( { ( 𝐴 + 1 ) } ⊆ ℙ ↔ ( { ( 𝐴 + 1 ) } ∩ ℙ ) = { ( 𝐴 + 1 ) } )
47 45 46 sylib ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( { ( 𝐴 + 1 ) } ∩ ℙ ) = { ( 𝐴 + 1 ) } )
48 47 uneq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) )
49 43 48 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) )
50 49 fveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) = ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) )
51 22 50 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) )
52 ppival2 ⊢ ( 𝐴 ∈ ℤ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )
53 52 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )
54 53 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( π ‘ 𝐴 ) + 1 ) = ( ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) + 1 ) )
55 20 51 54 3eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ( π ‘ 𝐴 ) + 1 ) )