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