chtvalz - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > chtvalz		Structured version Visualization version GIF version

Theorem chtvalz 30707

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 11381	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2		chtval 24836	. . 3 ⊢ (𝑁 ∈ ℝ → (θ‘𝑁) = Σ𝑛 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑛))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑛))
4		nnz 11399	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
5		ppisval 24830	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → ((0[,]𝑁) ∩ ℙ) = ((2...(⌊‘𝑁)) ∩ ℙ))
6	1, 5	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → ((0[,]𝑁) ∩ ℙ) = ((2...(⌊‘𝑁)) ∩ ℙ))
7		flid 12609	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → (⌊‘𝑁) = 𝑁)
8	7	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (2...(⌊‘𝑁)) = (2...𝑁))
9	8	ineq1d 3813	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → ((2...(⌊‘𝑁)) ∩ ℙ) = ((2...𝑁) ∩ ℙ))
10	6, 9	eqtrd 2656	. . . . . . 7 ⊢ (𝑁 ∈ ℤ → ((0[,]𝑁) ∩ ℙ) = ((2...𝑁) ∩ ℙ))
11	4, 10	syl 17	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((0[,]𝑁) ∩ ℙ) = ((2...𝑁) ∩ ℙ))
12		2nn 11185	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ
13		nnuz 11723	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ_≥‘1)
14	12, 13	eleqtri 2699	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ_≥‘1)
15		fzss1 12380	. . . . . . . . . . . 12 ⊢ (2 ∈ (ℤ_≥‘1) → (2...𝑁) ⊆ (1...𝑁))
16	14, 15	ax-mp 5	. . . . . . . . . . 11 ⊢ (2...𝑁) ⊆ (1...𝑁)
17		ssdif0 3942	. . . . . . . . . . 11 ⊢ ((2...𝑁) ⊆ (1...𝑁) ↔ ((2...𝑁) ∖ (1...𝑁)) = ∅)
18	16, 17	mpbi 220	. . . . . . . . . 10 ⊢ ((2...𝑁) ∖ (1...𝑁)) = ∅
19	18	ineq1i 3810	. . . . . . . . 9 ⊢ (((2...𝑁) ∖ (1...𝑁)) ∩ ℙ) = (∅ ∩ ℙ)
20		0in 3969	. . . . . . . . 9 ⊢ (∅ ∩ ℙ) = ∅
21	19, 20	eqtri 2644	. . . . . . . 8 ⊢ (((2...𝑁) ∖ (1...𝑁)) ∩ ℙ) = ∅
22	21	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((2...𝑁) ∖ (1...𝑁)) ∩ ℙ) = ∅)
23	13	eleq2i 2693	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
24		fzpred 12389	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
25	23, 24	sylbi 207	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
26	25	eqcomd 2628	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ({1} ∪ ((1 + 1)...𝑁)) = (1...𝑁))
27		1p1e2 11134	. . . . . . . . . . . . 13 ⊢ (1 + 1) = 2
28	27	oveq1i 6660	. . . . . . . . . . . 12 ⊢ ((1 + 1)...𝑁) = (2...𝑁)
29	28	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((1 + 1)...𝑁) = (2...𝑁))
30	26, 29	difeq12d 3729	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (({1} ∪ ((1 + 1)...𝑁)) ∖ ((1 + 1)...𝑁)) = ((1...𝑁) ∖ (2...𝑁)))
31		difun2 4048	. . . . . . . . . . 11 ⊢ (({1} ∪ ((1 + 1)...𝑁)) ∖ ((1 + 1)...𝑁)) = ({1} ∖ ((1 + 1)...𝑁))
32		fzpreddisj 12390	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘1) → ({1} ∩ ((1 + 1)...𝑁)) = ∅)
33	23, 32	sylbi 207	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ({1} ∩ ((1 + 1)...𝑁)) = ∅)
34		disjdif2 4047	. . . . . . . . . . . 12 ⊢ (({1} ∩ ((1 + 1)...𝑁)) = ∅ → ({1} ∖ ((1 + 1)...𝑁)) = {1})
35	33, 34	syl 17	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ({1} ∖ ((1 + 1)...𝑁)) = {1})
36	31, 35	syl5eq 2668	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (({1} ∪ ((1 + 1)...𝑁)) ∖ ((1 + 1)...𝑁)) = {1})
37	30, 36	eqtr3d 2658	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((1...𝑁) ∖ (2...𝑁)) = {1})
38	37	ineq1d 3813	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (((1...𝑁) ∖ (2...𝑁)) ∩ ℙ) = ({1} ∩ ℙ))
39		incom 3805	. . . . . . . . 9 ⊢ (ℙ ∩ {1}) = ({1} ∩ ℙ)
40		1nprm 15392	. . . . . . . . . 10 ⊢ ¬ 1 ∈ ℙ
41		disjsn 4246	. . . . . . . . . 10 ⊢ ((ℙ ∩ {1}) = ∅ ↔ ¬ 1 ∈ ℙ)
42	40, 41	mpbir 221	. . . . . . . . 9 ⊢ (ℙ ∩ {1}) = ∅
43	39, 42	eqtr3i 2646	. . . . . . . 8 ⊢ ({1} ∩ ℙ) = ∅
44	38, 43	syl6eq 2672	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((1...𝑁) ∖ (2...𝑁)) ∩ ℙ) = ∅)
45		difininv 29354	. . . . . . 7 ⊢ (((((2...𝑁) ∖ (1...𝑁)) ∩ ℙ) = ∅ ∧ (((1...𝑁) ∖ (2...𝑁)) ∩ ℙ) = ∅) → ((2...𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
46	22, 44, 45	syl2anc 693	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((2...𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
47	11, 46	eqtrd 2656	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
48	47	adantl 482	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
49		znnnlt1 11404	. . . . . 6 ⊢ (𝑁 ∈ ℤ → (¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1))
50	49	biimpa 501	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ) → 𝑁 < 1)
51		incom 3805	. . . . . . 7 ⊢ ((0[,]𝑁) ∩ ℙ) = (ℙ ∩ (0[,]𝑁))
52		isprm3 15396	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℙ ↔ (𝑛 ∈ (ℤ_≥‘2) ∧ ∀𝑖 ∈ (2...(𝑛 − 1)) ¬ 𝑖 ∥ 𝑛))
53	52	simplbi 476	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ_≥‘2))
54	53	ssriv 3607	. . . . . . . . 9 ⊢ ℙ ⊆ (ℤ_≥‘2)
55	12	nnzi 11401	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
56		uzssico 29546	. . . . . . . . . 10 ⊢ (2 ∈ ℤ → (ℤ_≥‘2) ⊆ (2[,)+∞))
57	55, 56	ax-mp 5	. . . . . . . . 9 ⊢ (ℤ_≥‘2) ⊆ (2[,)+∞)
58	54, 57	sstri 3612	. . . . . . . 8 ⊢ ℙ ⊆ (2[,)+∞)
59		incom 3805	. . . . . . . . 9 ⊢ ((0[,]𝑁) ∩ (2[,)+∞)) = ((2[,)+∞) ∩ (0[,]𝑁))
60		0xr 10086	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
61	60	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 0 ∈ ℝ^*)
62	12	nnrei 11029	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
63	62	rexri 10097	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ^*
64	63	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 2 ∈ ℝ^*)
65		0le0 11110	. . . . . . . . . . . 12 ⊢ 0 ≤ 0
66	65	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 0 ≤ 0)
67	1	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 𝑁 ∈ ℝ)
68		1red 10055	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 1 ∈ ℝ)
69	62	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 2 ∈ ℝ)
70		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 𝑁 < 1)
71		1lt2 11194	. . . . . . . . . . . . 13 ⊢ 1 < 2
72	71	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 1 < 2)
73	67, 68, 69, 70, 72	lttrd 10198	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 𝑁 < 2)
74		iccssico 12245	. . . . . . . . . . 11 ⊢ (((0 ∈ ℝ^* ∧ 2 ∈ ℝ^*) ∧ (0 ≤ 0 ∧ 𝑁 < 2)) → (0[,]𝑁) ⊆ (0[,)2))
75	61, 64, 66, 73, 74	syl22anc 1327	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → (0[,]𝑁) ⊆ (0[,)2))
76		pnfxr 10092	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ^*
77		icodisj 12297	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 2 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((0[,)2) ∩ (2[,)+∞)) = ∅)
78	60, 63, 76, 77	mp3an 1424	. . . . . . . . . 10 ⊢ ((0[,)2) ∩ (2[,)+∞)) = ∅
79		ssdisj 4026	. . . . . . . . . 10 ⊢ (((0[,]𝑁) ⊆ (0[,)2) ∧ ((0[,)2) ∩ (2[,)+∞)) = ∅) → ((0[,]𝑁) ∩ (2[,)+∞)) = ∅)
80	75, 78, 79	sylancl 694	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((0[,]𝑁) ∩ (2[,)+∞)) = ∅)
81	59, 80	syl5eqr 2670	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((2[,)+∞) ∩ (0[,]𝑁)) = ∅)
82		ssdisj 4026	. . . . . . . 8 ⊢ ((ℙ ⊆ (2[,)+∞) ∧ ((2[,)+∞) ∩ (0[,]𝑁)) = ∅) → (ℙ ∩ (0[,]𝑁)) = ∅)
83	58, 81, 82	sylancr 695	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → (ℙ ∩ (0[,]𝑁)) = ∅)
84	51, 83	syl5eq 2668	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((0[,]𝑁) ∩ ℙ) = ∅)
85		1zzd 11408	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 1 ∈ ℤ)
86		simpl 473	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → 𝑁 ∈ ℤ)
87		fzn 12357	. . . . . . . . . 10 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 1 ↔ (1...𝑁) = ∅))
88	87	biimpa 501	. . . . . . . . 9 ⊢ (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 < 1) → (1...𝑁) = ∅)
89	85, 86, 70, 88	syl21anc 1325	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → (1...𝑁) = ∅)
90	89	ineq1d 3813	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((1...𝑁) ∩ ℙ) = (∅ ∩ ℙ))
91	90, 20	syl6eq 2672	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((1...𝑁) ∩ ℙ) = ∅)
92	84, 91	eqtr4d 2659	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 1) → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
93	50, 92	syldan 487	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ) → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
94		exmidd 432	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℕ ∨ ¬ 𝑁 ∈ ℕ))
95	48, 93, 94	mpjaodan 827	. . 3 ⊢ (𝑁 ∈ ℤ → ((0[,]𝑁) ∩ ℙ) = ((1...𝑁) ∩ ℙ))
96	95	sumeq1d 14431	. 2 ⊢ (𝑁 ∈ ℤ → Σ𝑛 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑛) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))
97	3, 96	eqtrd 2656	1 ⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 {csn 4177 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 +∞cpnf 10071 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 ℕcn 11020 2c2 11070 ℤcz 11377 ℤ_≥cuz 11687 [,)cico 12177 [,]cicc 12178 ...cfz 12326 ⌊cfl 12591 Σcsu 14416 ∥ cdvds 14983 ℙcprime 15385 logclog 24301 θccht 24817

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ico 12181 df-icc 12182 df-fz 12327 df-fl 12593 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-sum 14417 df-dvds 14984 df-prm 15386 df-cht 24823

This theorem is referenced by: hgt750lemd 30726

W3C validator