Metamath Proof Explorer


Theorem ppinprm

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

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

Proof

Step Hyp Ref Expression
1 simprr ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) )
2 1 elin2d ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ℙ )
3 simprl ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ¬ ( 𝐴 + 1 ) ∈ ℙ )
4 nelne2 ( ( 𝑥 ∈ ℙ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → 𝑥 ≠ ( 𝐴 + 1 ) )
5 2 3 4 syl2anc ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ≠ ( 𝐴 + 1 ) )
6 velsn ( 𝑥 ∈ { ( 𝐴 + 1 ) } ↔ 𝑥 = ( 𝐴 + 1 ) )
7 6 necon3bbii ( ¬ 𝑥 ∈ { ( 𝐴 + 1 ) } ↔ 𝑥 ≠ ( 𝐴 + 1 ) )
8 5 7 sylibr ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ¬ 𝑥 ∈ { ( 𝐴 + 1 ) } )
9 1 elin1d ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( 2 ... ( 𝐴 + 1 ) ) )
10 2z 2 ∈ ℤ
11 zcn ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
12 11 adantr ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℂ )
13 ax-1cn 1 ∈ ℂ
14 pncan ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
15 12 13 14 sylancl ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
16 elfzuz2 ( 𝑥 ∈ ( 2 ... ( 𝐴 + 1 ) ) → ( 𝐴 + 1 ) ∈ ( ℤ ‘ 2 ) )
17 uz2m1nn ( ( 𝐴 + 1 ) ∈ ( ℤ ‘ 2 ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ )
18 9 16 17 3syl ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ )
19 15 18 eqeltrrd ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℕ )
20 nnuz ℕ = ( ℤ ‘ 1 )
21 2m1e1 ( 2 − 1 ) = 1
22 21 fveq2i ( ℤ ‘ ( 2 − 1 ) ) = ( ℤ ‘ 1 )
23 20 22 eqtr4i ℕ = ( ℤ ‘ ( 2 − 1 ) )
24 19 23 eleqtrdi ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ( ℤ ‘ ( 2 − 1 ) ) )
25 fzsuc2 ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ( ℤ ‘ ( 2 − 1 ) ) ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) )
26 10 24 25 sylancr ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) )
27 9 26 eleqtrd ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) )
28 elun ( 𝑥 ∈ ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ↔ ( 𝑥 ∈ ( 2 ... 𝐴 ) ∨ 𝑥 ∈ { ( 𝐴 + 1 ) } ) )
29 27 28 sylib ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( 𝑥 ∈ ( 2 ... 𝐴 ) ∨ 𝑥 ∈ { ( 𝐴 + 1 ) } ) )
30 29 ord ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( ¬ 𝑥 ∈ ( 2 ... 𝐴 ) → 𝑥 ∈ { ( 𝐴 + 1 ) } ) )
31 8 30 mt3d ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( 2 ... 𝐴 ) )
32 31 2 elind ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) )
33 32 expr ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) → 𝑥 ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )
34 33 ssrdv ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ⊆ ( ( 2 ... 𝐴 ) ∩ ℙ ) )
35 uzid ( 𝐴 ∈ ℤ → 𝐴 ∈ ( ℤ𝐴 ) )
36 35 adantr ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ( ℤ𝐴 ) )
37 peano2uz ( 𝐴 ∈ ( ℤ𝐴 ) → ( 𝐴 + 1 ) ∈ ( ℤ𝐴 ) )
38 fzss2 ( ( 𝐴 + 1 ) ∈ ( ℤ𝐴 ) → ( 2 ... 𝐴 ) ⊆ ( 2 ... ( 𝐴 + 1 ) ) )
39 ssrin ( ( 2 ... 𝐴 ) ⊆ ( 2 ... ( 𝐴 + 1 ) ) → ( ( 2 ... 𝐴 ) ∩ ℙ ) ⊆ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) )
40 36 37 38 39 4syl ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... 𝐴 ) ∩ ℙ ) ⊆ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) )
41 34 40 eqssd ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... 𝐴 ) ∩ ℙ ) )
42 41 fveq2d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )
43 peano2z ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ )
44 43 adantr ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℤ )
45 ppival2 ( ( 𝐴 + 1 ) ∈ ℤ → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) )
46 44 45 syl ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) )
47 ppival2 ( 𝐴 ∈ ℤ → ( π𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )
48 47 adantr ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( π𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )
49 42 46 48 3eqtr4d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( π𝐴 ) )