Metamath Proof Explorer


Theorem chtnprm

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

Ref Expression
Assertion chtnprm ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 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 peano2z ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ )
43 42 adantr ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℤ )
44 flid ( ( 𝐴 + 1 ) ∈ ℤ → ( ⌊ ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
45 43 44 syl ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ⌊ ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
46 45 oveq2d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) = ( 2 ... ( 𝐴 + 1 ) ) )
47 46 ineq1d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) = ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) )
48 flid ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
49 48 adantr ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ⌊ ‘ 𝐴 ) = 𝐴 )
50 49 oveq2d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) = ( 2 ... 𝐴 ) )
51 50 ineq1d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... 𝐴 ) ∩ ℙ ) )
52 41 47 51 3eqtr4d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
53 zre ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
54 53 adantr ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℝ )
55 peano2re ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
56 ppisval ( ( 𝐴 + 1 ) ∈ ℝ → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) )
57 54 55 56 3syl ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) )
58 ppisval ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
59 54 58 syl ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
60 52 57 59 3eqtr4d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
61 60 sumeq1d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
62 chtval ( ( 𝐴 + 1 ) ∈ ℝ → ( θ ‘ ( 𝐴 + 1 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
63 54 55 62 3syl ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ ( 𝐴 + 1 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
64 chtval ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
65 54 64 syl ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
66 61 63 65 3eqtr4d ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ ( 𝐴 + 1 ) ) = ( θ ‘ 𝐴 ) )