Theorem chtvalz 31517

Description: Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.)

Assertion

Ref	Expression
chtvalz	⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))

Distinct variable group:   𝑛,𝑁

Proof of Theorem chtvalz

Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		zre 11833	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2		chtval 25369	. . 3 ⊢ (𝑁 ∈ ℝ → (θ‘𝑁) = Σ𝑛 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑛))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑛))
4		nnz 11853	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
5		ppisval 25363	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → ((0[,]𝑁) ∩ ℙ) = ((2...(⌊‘𝑁)) ∩ ℙ))
6	1, 5	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → ((0[,]𝑁) ∩ ℙ) = ((2...(⌊‘𝑁)) ∩ ℙ))
7		flid 13028	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → (⌊‘𝑁) = 𝑁)
8	7	oveq2d 7032	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (2...(⌊‘𝑁)) = (2...𝑁))
9	8	ineq1d 4108	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → ((2...(⌊‘𝑁)) ∩ ℙ) = ((2...𝑁) ∩ ℙ))
10	6, 9	eqtrd 2831	. . . . . . 7 ⊢ (𝑁 ∈ ℤ → ((0[,]𝑁) ∩ ℙ) = ((2...𝑁) ∩ ℙ))
11	4, 10	syl 17	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((0[,]𝑁) ∩ ℙ) = ((2...𝑁) ∩ ℙ))
12		2nn 11558	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ
13		nnuz 12130	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
14	12, 13	eleqtri 2881	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ≥‘1)
15		fzss1 12796	. . . . . . . . . . . 12 ⊢ (2 ∈ (ℤ≥‘1) → (2...𝑁) ⊆ (1...𝑁))
16	14, 15	ax-mp 5	. . . . . . . . . . 11 ⊢ (2...𝑁) ⊆ (1...𝑁)
17		ssdif0 4243	. . . . . . . . . . 11 ⊢ ((2...𝑁) ⊆ (1...𝑁) ↔ ((2...𝑁) ∖ (1...𝑁)) = ∅)
18	16, 17	mpbi 231	. . . . . . . . . 10 ⊢ ((2...𝑁) ∖ (1...𝑁)) = ∅
19	18	ineq1i 4105	. . . . . . . . 9 ⊢ (((2...𝑁) ∖ (1...𝑁)) ∩ ℙ) = (∅ ∩ ℙ)
20		0in 4267	. . . . . . . . 9 ⊢ (∅ ∩ ℙ) = ∅
21	19, 20	eqtri 2819	. . . . . . . 8 ⊢ (((2...𝑁) ∖ (1...𝑁)) ∩ ℙ) = ∅
22	21	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((2...𝑁) ∖ (1...𝑁)) ∩ ℙ) = ∅)
23	13	eleq2i 2874	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1))
24		fzpred 12805	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ≥‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
25	23, 24	sylbi 218	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
26	25	eqcomd 2801	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ({1} ∪ ((1 + 1)...𝑁)) = (1...𝑁))
27		1p1e2 11610	. . . . . . . . . . . . 13 ⊢ (1 + 1) = 2
28	27	oveq1i 7026	. . . . . . . . . . . 12 ⊢ ((1 + 1)...𝑁) = (2...𝑁)
29	28	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((1 + 1)...𝑁) = (2...𝑁))
30	26, 29	difeq12d 4021	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (({1} ∪ ((1 + 1)...𝑁)) ∖ ((1 + 1)...𝑁)) = ((1...𝑁) ∖ (2...𝑁)))
31		difun2 4343	. . . . . . . . . . 11 ⊢ (({1} ∪ ((1 + 1)...𝑁)) ∖ ((1 + 1)...𝑁)) = ({1} ∖ ((1 + 1)...𝑁))
32		fzpreddisj 12806	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ≥‘1) → ({1} ∩ ((1 + 1)...𝑁)) = ∅)
33	23, 32	sylbi 218	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ({1} ∩ ((1 + 1)...𝑁)) = ∅)
34		disjdif2 4342	. . . . . . . . . . . 12 ⊢ (({1} ∩ ((1 + 1)...𝑁)) = ∅ → ({1} ∖ ((1 + 1)...𝑁)) = {1})
35	33, 34	syl 17	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ({1} ∖ ((1 + 1)...𝑁)) = {1})
36	31, 35	syl5eq 2843	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (({1} ∪ ((1 + 1)...𝑁)) ∖ ((1 + 1)...𝑁)) = {1})
37	30, 36	eqtr3d 2833	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((1...𝑁) ∖ (2...𝑁)) = {1})
38	37	ineq1d 4108	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (((1...𝑁) ∖ (2...𝑁)) ∩ ℙ) = ({1} ∩ ℙ))
39		incom 4099	. . . . . . . . 9 ⊢ (ℙ ∩ {1}) = ({1} ∩ ℙ)
40		1nprm 15852	. . . . . . . . . 10 ⊢ ¬ 1 ∈ ℙ
41		disjsn 4554	. . . . . . . . . 10 ⊢ ((ℙ ∩ {1}) = ∅ ↔ ¬ 1 ∈ ℙ)
42	40, 41	mpbir 232	. . . . . . . . 9 ⊢ (ℙ ∩ {1}) = ∅
43	39, 42	eqtr3i 2821	. . . . . . . 8 ⊢ ({1} ∩ ℙ) = ∅
44	38, 43	syl6eq 2847	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((1...𝑁) ∖ (2...𝑁)) ∩ ℙ) = ∅)
45		difininv 29968	. . . . . . 7 ⊢ (((((2...𝑁) ∖ (1...𝑁)) ∩ ℙ) = ∅ ∧ (((1...𝑁) ∖ (2...𝑁)) ∩ ℙ) = ∅) → ((2...𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
46	22, 44, 45	syl2anc 584	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((2...𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
47	11, 46	eqtrd 2831	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
48	47	adantl 482	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
49		znnnlt1 11858	. . . . . 6 ⊢ (𝑁 ∈ ℤ → (¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1))
50	49	biimpa 477	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ) → 𝑁 < 1)
51		incom 4099	. . . . . . 7 ⊢ ((0[,]𝑁) ∩ ℙ) = (ℙ ∩ (0[,]𝑁))
52		isprm3 15856	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℙ ↔ (𝑛 ∈ (ℤ≥‘2) ∧ ∀𝑖 ∈ (2...(𝑛 − 1)) ¬ 𝑖 ∥ 𝑛))
53	52	simplbi 498	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ≥‘2))
54	53	ssriv 3893	. . . . . . . . 9 ⊢ ℙ ⊆ (ℤ≥‘2)
55	12	nnzi 11855	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
56		uzssico 30195	. . . . . . . . . 10 ⊢ (2 ∈ ℤ → (ℤ≥‘2) ⊆ (2[,)+∞))
57	55, 56	ax-mp 5	. . . . . . . . 9 ⊢ (ℤ≥‘2) ⊆ (2[,)+∞)
58	54, 57	sstri 3898	. . . . . . . 8 ⊢ ℙ ⊆ (2[,)+∞)
59		incom 4099	. . . . . . . . 9 ⊢ ((0[,]𝑁) ∩ (2[,)+∞)) = ((2[,)+∞) ∩ (0[,]𝑁))
60		0xr 10534	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ*
61	60	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 0 ∈ ℝ*)
62	12	nnrei 11495	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
63	62	rexri 10546	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ*
64	63	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 2 ∈ ℝ*)
65		0le0 11586	. . . . . . . . . . . 12 ⊢ 0 ≤ 0
66	65	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 0 ≤ 0)
67	1	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 𝑁 ∈ ℝ)
68		1red 10488	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 1 ∈ ℝ)
69	62	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 2 ∈ ℝ)
70		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 𝑁 < 1)
71		1lt2 11656	. . . . . . . . . . . . 13 ⊢ 1 < 2
72	71	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 1 < 2)
73	67, 68, 69, 70, 72	lttrd 10648	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 𝑁 < 2)
74		iccssico 12658	. . . . . . . . . . 11 ⊢ (((0 ∈ ℝ* ∧ 2 ∈ ℝ*) ∧ (0 ≤ 0 ∧ 𝑁 < 2)) → (0[,]𝑁) ⊆ (0[,)2))
75	61, 64, 66, 73, 74	syl22anc 835	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → (0[,]𝑁) ⊆ (0[,)2))
76		pnfxr 10541	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ*
77		icodisj 12712	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ* ∧ 2 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((0[,)2) ∩ (2[,)+∞)) = ∅)
78	60, 63, 76, 77	mp3an 1453	. . . . . . . . . 10 ⊢ ((0[,)2) ∩ (2[,)+∞)) = ∅
79		ssdisj 4323	. . . . . . . . . 10 ⊢ (((0[,]𝑁) ⊆ (0[,)2) ∧ ((0[,)2) ∩ (2[,)+∞)) = ∅) → ((0[,]𝑁) ∩ (2[,)+∞)) = ∅)
80	75, 78, 79	sylancl 586	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((0[,]𝑁) ∩ (2[,)+∞)) = ∅)
81	59, 80	syl5eqr 2845	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((2[,)+∞) ∩ (0[,]𝑁)) = ∅)
82		ssdisj 4323	. . . . . . . 8 ⊢ ((ℙ ⊆ (2[,)+∞) ∧ ((2[,)+∞) ∩ (0[,]𝑁)) = ∅) → (ℙ ∩ (0[,]𝑁)) = ∅)
83	58, 81, 82	sylancr 587	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → (ℙ ∩ (0[,]𝑁)) = ∅)
84	51, 83	syl5eq 2843	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((0[,]𝑁) ∩ ℙ) = ∅)
85		1zzd 11862	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 1 ∈ ℤ)
86		simpl 483	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 𝑁 ∈ ℤ)
87		fzn 12773	. . . . . . . . . 10 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 1 ↔ (1...𝑁) = ∅))
88	87	biimpa 477	. . . . . . . . 9 ⊢ (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 < 1) → (1...𝑁) = ∅)
89	85, 86, 70, 88	syl21anc 834	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → (1...𝑁) = ∅)
90	89	ineq1d 4108	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((1...𝑁) ∩ ℙ) = (∅ ∩ ℙ))
91	90, 20	syl6eq 2847	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((1...𝑁) ∩ ℙ) = ∅)
92	84, 91	eqtr4d 2834	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
93	50, 92	syldan 591	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ) → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
94		exmidd 890	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℕ ∨ ¬ 𝑁 ∈ ℕ))
95	48, 93, 94	mpjaodan 953	. . 3 ⊢ (𝑁 ∈ ℤ → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
96	95	sumeq1d 14891	. 2 ⊢ (𝑁 ∈ ℤ → Σ𝑛 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑛) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))
97	3, 96	eqtrd 2831	1 ⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∀wral 3105   ∖ cdif 3856   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  ∅c0 4211  {csn 4472   class class class wbr 4962  ‘cfv 6225  (class class class)co 7016  ℝcr 10382  0cc0 10383  1c1 10384   + caddc 10386  +∞cpnf 10518  ℝ^*cxr 10520   < clt 10521   ≤ cle 10522   − cmin 10717  ℕcn 11486  2c2 11540  ℤcz 11829  ℤ_≥cuz 12093  [,)cico 12590  [,]cicc 12591  ...cfz 12742  ⌊cfl 13010  Σcsu 14876   ∥ cdvds 15440  ℙcprime 15844  logclog 24819  θccht 25350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-2o 7954  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-sup 8752  df-inf 8753  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-n0 11746  df-z 11830  df-uz 12094  df-rp 12240  df-ico 12594  df-icc 12595  df-fz 12743  df-fl 13012  df-seq 13220  df-exp 13280  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-sum 14877  df-dvds 15441  df-prm 15845  df-cht 25356

This theorem is referenced by:  hgt750lemd  31536