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 df-ss ( { ( 𝐴 + 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 ) )