# Metamath Proof Explorer

## Theorem chtnprm

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

Ref Expression
Assertion chtnprm ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \theta \left({A}+1\right)=\theta \left({A}\right)$

### Proof

Step Hyp Ref Expression
1 simprr ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)$
2 1 elin2d ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {x}\in ℙ$
3 simprl ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to ¬{A}+1\in ℙ$
4 nelne2 ${⊢}\left({x}\in ℙ\wedge ¬{A}+1\in ℙ\right)\to {x}\ne {A}+1$
5 2 3 4 syl2anc ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {x}\ne {A}+1$
6 velsn ${⊢}{x}\in \left\{{A}+1\right\}↔{x}={A}+1$
7 6 necon3bbii ${⊢}¬{x}\in \left\{{A}+1\right\}↔{x}\ne {A}+1$
8 5 7 sylibr ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to ¬{x}\in \left\{{A}+1\right\}$
9 1 elin1d ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {x}\in \left(2\dots {A}+1\right)$
10 2z ${⊢}2\in ℤ$
11 zcn ${⊢}{A}\in ℤ\to {A}\in ℂ$
12 11 adantr ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {A}\in ℂ$
13 ax-1cn ${⊢}1\in ℂ$
14 pncan ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\right)\to {A}+1-1={A}$
15 12 13 14 sylancl ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {A}+1-1={A}$
16 elfzuz2 ${⊢}{x}\in \left(2\dots {A}+1\right)\to {A}+1\in {ℤ}_{\ge 2}$
17 uz2m1nn ${⊢}{A}+1\in {ℤ}_{\ge 2}\to {A}+1-1\in ℕ$
18 9 16 17 3syl ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {A}+1-1\in ℕ$
19 15 18 eqeltrrd ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {A}\in ℕ$
20 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
21 2m1e1 ${⊢}2-1=1$
22 21 fveq2i ${⊢}{ℤ}_{\ge \left(2-1\right)}={ℤ}_{\ge 1}$
23 20 22 eqtr4i ${⊢}ℕ={ℤ}_{\ge \left(2-1\right)}$
24 19 23 eleqtrdi ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {A}\in {ℤ}_{\ge \left(2-1\right)}$
25 fzsuc2 ${⊢}\left(2\in ℤ\wedge {A}\in {ℤ}_{\ge \left(2-1\right)}\right)\to \left(2\dots {A}+1\right)=\left(2\dots {A}\right)\cup \left\{{A}+1\right\}$
26 10 24 25 sylancr ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to \left(2\dots {A}+1\right)=\left(2\dots {A}\right)\cup \left\{{A}+1\right\}$
27 9 26 eleqtrd ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {x}\in \left(\left(2\dots {A}\right)\cup \left\{{A}+1\right\}\right)$
28 elun ${⊢}{x}\in \left(\left(2\dots {A}\right)\cup \left\{{A}+1\right\}\right)↔\left({x}\in \left(2\dots {A}\right)\vee {x}\in \left\{{A}+1\right\}\right)$
29 27 28 sylib ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to \left({x}\in \left(2\dots {A}\right)\vee {x}\in \left\{{A}+1\right\}\right)$
30 29 ord ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to \left(¬{x}\in \left(2\dots {A}\right)\to {x}\in \left\{{A}+1\right\}\right)$
31 8 30 mt3d ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {x}\in \left(2\dots {A}\right)$
32 31 2 elind ${⊢}\left({A}\in ℤ\wedge \left(¬{A}+1\in ℙ\wedge {x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\right)\right)\to {x}\in \left(\left(2\dots {A}\right)\cap ℙ\right)$
33 32 expr ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left({x}\in \left(\left(2\dots {A}+1\right)\cap ℙ\right)\to {x}\in \left(\left(2\dots {A}\right)\cap ℙ\right)\right)$
34 33 ssrdv ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left(2\dots {A}+1\right)\cap ℙ\subseteq \left(2\dots {A}\right)\cap ℙ$
35 uzid ${⊢}{A}\in ℤ\to {A}\in {ℤ}_{\ge {A}}$
36 35 adantr ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to {A}\in {ℤ}_{\ge {A}}$
37 peano2uz ${⊢}{A}\in {ℤ}_{\ge {A}}\to {A}+1\in {ℤ}_{\ge {A}}$
38 fzss2 ${⊢}{A}+1\in {ℤ}_{\ge {A}}\to \left(2\dots {A}\right)\subseteq \left(2\dots {A}+1\right)$
39 ssrin ${⊢}\left(2\dots {A}\right)\subseteq \left(2\dots {A}+1\right)\to \left(2\dots {A}\right)\cap ℙ\subseteq \left(2\dots {A}+1\right)\cap ℙ$
40 36 37 38 39 4syl ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left(2\dots {A}\right)\cap ℙ\subseteq \left(2\dots {A}+1\right)\cap ℙ$
41 34 40 eqssd ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left(2\dots {A}+1\right)\cap ℙ=\left(2\dots {A}\right)\cap ℙ$
42 peano2z ${⊢}{A}\in ℤ\to {A}+1\in ℤ$
43 42 adantr ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to {A}+1\in ℤ$
44 flid ${⊢}{A}+1\in ℤ\to ⌊{A}+1⌋={A}+1$
45 43 44 syl ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to ⌊{A}+1⌋={A}+1$
46 45 oveq2d ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left(2\dots ⌊{A}+1⌋\right)=\left(2\dots {A}+1\right)$
47 46 ineq1d ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left(2\dots ⌊{A}+1⌋\right)\cap ℙ=\left(2\dots {A}+1\right)\cap ℙ$
48 flid ${⊢}{A}\in ℤ\to ⌊{A}⌋={A}$
49 48 adantr ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to ⌊{A}⌋={A}$
50 49 oveq2d ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left(2\dots ⌊{A}⌋\right)=\left(2\dots {A}\right)$
51 50 ineq1d ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left(2\dots ⌊{A}⌋\right)\cap ℙ=\left(2\dots {A}\right)\cap ℙ$
52 41 47 51 3eqtr4d ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left(2\dots ⌊{A}+1⌋\right)\cap ℙ=\left(2\dots ⌊{A}⌋\right)\cap ℙ$
53 zre ${⊢}{A}\in ℤ\to {A}\in ℝ$
54 53 adantr ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to {A}\in ℝ$
55 peano2re ${⊢}{A}\in ℝ\to {A}+1\in ℝ$
56 ppisval ${⊢}{A}+1\in ℝ\to \left[0,{A}+1\right]\cap ℙ=\left(2\dots ⌊{A}+1⌋\right)\cap ℙ$
57 54 55 56 3syl ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left[0,{A}+1\right]\cap ℙ=\left(2\dots ⌊{A}+1⌋\right)\cap ℙ$
58 ppisval ${⊢}{A}\in ℝ\to \left[0,{A}\right]\cap ℙ=\left(2\dots ⌊{A}⌋\right)\cap ℙ$
59 54 58 syl ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left[0,{A}\right]\cap ℙ=\left(2\dots ⌊{A}⌋\right)\cap ℙ$
60 52 57 59 3eqtr4d ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \left[0,{A}+1\right]\cap ℙ=\left[0,{A}\right]\cap ℙ$
61 60 sumeq1d ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \sum _{{p}\in \left[0,{A}+1\right]\cap ℙ}\mathrm{log}{p}=\sum _{{p}\in \left[0,{A}\right]\cap ℙ}\mathrm{log}{p}$
62 chtval ${⊢}{A}+1\in ℝ\to \theta \left({A}+1\right)=\sum _{{p}\in \left[0,{A}+1\right]\cap ℙ}\mathrm{log}{p}$
63 54 55 62 3syl ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \theta \left({A}+1\right)=\sum _{{p}\in \left[0,{A}+1\right]\cap ℙ}\mathrm{log}{p}$
64 chtval ${⊢}{A}\in ℝ\to \theta \left({A}\right)=\sum _{{p}\in \left[0,{A}\right]\cap ℙ}\mathrm{log}{p}$
65 54 64 syl ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \theta \left({A}\right)=\sum _{{p}\in \left[0,{A}\right]\cap ℙ}\mathrm{log}{p}$
66 61 63 65 3eqtr4d ${⊢}\left({A}\in ℤ\wedge ¬{A}+1\in ℙ\right)\to \theta \left({A}+1\right)=\theta \left({A}\right)$