rpvmasum - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rpvmasum		Structured version Visualization version GIF version

Theorem rpvmasum 27656

Description: The sum of the von Mangoldt function over those integers 𝑛≡𝐴 (mod 𝑁) is asymptotic to log𝑥 / ϕ(𝑥) + 𝑂(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)

**Hypotheses**
Ref	Expression
rpvmasum.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l	⊢ 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a	⊢ (𝜑 → 𝑁 ∈ ℕ)
rpvmasum.u	⊢ 𝑈 = (Unit‘𝑍)
rpvmasum.b	⊢ (𝜑 → 𝐴 ∈ 𝑈)
rpvmasum.t	⊢ 𝑇 = (^◡𝐿 “ {𝐴})

**Assertion**
Ref	Expression
rpvmasum	⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))

Distinct variable groups: 𝑥,𝑛,𝐴 𝑛,𝑁,𝑥 𝜑,𝑛,𝑥 𝑇,𝑛,𝑥 𝑈,𝑛,𝑥 𝑛,𝑍,𝑥 𝑛,𝐿,𝑥 𝐴,𝑛

Proof of Theorem rpvmasum Dummy variables 𝑚 𝑦 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpvmasum.z	. . . . . . . . . . . . . 14 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
2		rpvmasum.l	. . . . . . . . . . . . . 14 ⊢ 𝐿 = (ℤRHom‘𝑍)
3		rpvmasum.a	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4	3	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) → 𝑁 ∈ ℕ)
5		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (DChr‘𝑁) = (DChr‘𝑁)
6		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (Base‘(DChr‘𝑁)) = (Base‘(DChr‘𝑁))
7		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (0_g‘(DChr‘𝑁)) = (0_g‘(DChr‘𝑁))
8		2fveq3 6887	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑦‘(𝐿‘𝑚)) = (𝑦‘(𝐿‘𝑛)))
9		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛)
10	8, 9	oveq12d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝑦‘(𝐿‘𝑚)) / 𝑚) = ((𝑦‘(𝐿‘𝑛)) / 𝑛))
11	10	cbvsumv 15747	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = Σ𝑛 ∈ ℕ ((𝑦‘(𝐿‘𝑛)) / 𝑛)
12	11	eqeq1i 2774	. . . . . . . . . . . . . . 15 ⊢ (Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0 ↔ Σ𝑛 ∈ ℕ ((𝑦‘(𝐿‘𝑛)) / 𝑛) = 0)
13	12	rabbii 3428	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} = {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑛 ∈ ℕ ((𝑦‘(𝐿‘𝑛)) / 𝑛) = 0}
14		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) → 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})
15	1, 2, 4, 5, 6, 7, 13, 14	dchrisum0 27650	. . . . . . . . . . . . 13 ⊢ ¬ (𝜑 ∧ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})
16	15	imnani 405	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})
17	16	eq0rdv 4378	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} = ∅)
18	17	fveq2d 6886	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) = (♯‘∅))
19		hash0 14403	. . . . . . . . . 10 ⊢ (♯‘∅) = 0
20	18, 19	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝜑 → (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) = 0)
21	20	oveq2d 7427	. . . . . . . 8 ⊢ (𝜑 → (1 − (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})) = (1 − 0))
22		1m0e1 12360	. . . . . . . 8 ⊢ (1 − 0) = 1
23	21, 22	eqtrdi 2820	. . . . . . 7 ⊢ (𝜑 → (1 − (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})) = 1)
24	23	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1 − (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})) = 1)
25	24	oveq2d 7427	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((log‘𝑥) · (1 − (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}))) = ((log‘𝑥) · 1))
26		relogcl 26706	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
27	26	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
28	27	recnd 11237	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
29	28	mulridd 11226	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((log‘𝑥) · 1) = (log‘𝑥))
30	25, 29	eqtrd 2804	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((log‘𝑥) · (1 − (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}))) = (log‘𝑥))
31	30	oveq2d 7427	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})))) = (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
32	31	mpteq2dva 5208	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}))))) = (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
33		eqid 2769	. . 3 ⊢ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} = {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}
34		rpvmasum.u	. . 3 ⊢ 𝑈 = (Unit‘𝑍)
35		rpvmasum.b	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
36		rpvmasum.t	. . 3 ⊢ 𝑇 = (^◡𝐿 “ {𝐴})
37	15	pm2.21i 120	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) → 𝐴 = (1_r‘𝑍))
38	1, 2, 3, 5, 6, 7, 33, 34, 35, 36, 37	rpvmasum2 27642	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}))))) ∈ 𝑂(1))
39	32, 38	eqeltrrd 2870	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 ∈ wcel 2149 {crab 3423 ∖ cdif 3910 ∩ cin 3912 ∅c0 4294 {csn 4594 ↦ cmpt 5196 ^◡ccnv 5661 “ cima 5665 ‘cfv 6537 (class class class)co 7411 ℝcr 11099 0cc0 11100 1c1 11101 · cmul 11105 − cmin 11441 / cdiv 11871 ℕcn 12233 ℝ⁺crp 13016 ...cfz 13535 ⌊cfl 13823 ♯chash 14366 𝑂(1)co1 15537 Σcsu 15737 ϕcphi 16823 Basecbs 17269 0_gc0g 17492 1_rcur 20263 Unitcui 20437 ℤRHomczrh 21618 ℤ/nℤczn 21621 logclog 26685 Λcvma 27222 DChrcdchr 27362

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9610 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178 ax-addf 11179 ax-mulf 11180

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-disj 5081 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-rpss 7721 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8157 df-tpos 8222 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-2o 8454 df-oadd 8457 df-omul 8458 df-er 8694 df-ec 8696 df-qs 8700 df-map 8826 df-pm 8827 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fsupp 9322 df-fi 9371 df-sup 9402 df-inf 9403 df-oi 9472 df-dju 9887 df-card 9925 df-acn 9928 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12505 df-xnn0 12578 df-z 12592 df-dec 12712 df-uz 12863 df-q 12973 df-rp 13017 df-xneg 13137 df-xadd 13138 df-xmul 13139 df-ioo 13376 df-ioc 13377 df-ico 13378 df-icc 13379 df-fz 13536 df-fzo 13683 df-fl 13825 df-mod 13903 df-seq 14038 df-exp 14098 df-fac 14310 df-bc 14339 df-hash 14367 df-word 14551 df-concat 14608 df-s1 14634 df-shft 15104 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-limsup 15522 df-clim 15539 df-rlim 15540 df-o1 15541 df-lo1 15542 df-sum 15738 df-ef 16121 df-e 16122 df-sin 16123 df-cos 16124 df-tan 16125 df-pi 16126 df-dvds 16311 df-gcd 16553 df-prm 16730 df-numer 16794 df-denom 16795 df-phi 16825 df-pc 16897 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-starv 17325 df-sca 17326 df-vsca 17327 df-ip 17328 df-tset 17329 df-ple 17330 df-ds 17332 df-unif 17333 df-hom 17334 df-cco 17335 df-rest 17475 df-topn 17476 df-0g 17494 df-gsum 17495 df-topgen 17496 df-pt 17497 df-prds 17500 df-xrs 17556 df-qtop 17561 df-imas 17562 df-qus 17563 df-xps 17564 df-mre 17638 df-mrc 17639 df-acs 17641 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-mhm 18841 df-submnd 18842 df-grp 19003 df-minusg 19004 df-sbg 19005 df-mulg 19134 df-subg 19189 df-nsg 19190 df-eqg 19191 df-ghm 19284 df-gim 19329 df-ga 19360 df-cntz 19387 df-oppg 19416 df-od 19598 df-gex 19599 df-pgp 19600 df-lsm 19706 df-pj1 19707 df-cmn 19852 df-abl 19853 df-cyg 19948 df-dprd 20067 df-dpj 20068 df-mgp 20217 df-rng 20231 df-ur 20264 df-ring 20317 df-cring 20318 df-oppr 20419 df-dvdsr 20439 df-unit 20440 df-invr 20470 df-dvr 20483 df-rhm 20554 df-subrng 20631 df-subrg 20655 df-drng 20815 df-lmod 20961 df-lss 21031 df-lsp 21071 df-sra 21272 df-rgmod 21273 df-lidl 21310 df-rsp 21311 df-2idl 21360 df-psmet 21483 df-xmet 21484 df-met 21485 df-bl 21486 df-mopn 21487 df-fbas 21488 df-fg 21489 df-cnfld 21492 df-zring 21566 df-zrh 21622 df-zn 21625 df-top 23020 df-topon 23037 df-topsp 23059 df-bases 23072 df-cld 23145 df-ntr 23146 df-cls 23147 df-nei 23224 df-lp 23262 df-perf 23263 df-cn 23353 df-cnp 23354 df-haus 23441 df-cmp 23513 df-tx 23688 df-hmeo 23881 df-fil 23972 df-fm 24064 df-flim 24065 df-flf 24066 df-xms 24446 df-ms 24447 df-tms 24448 df-cncf 25006 df-0p 25798 df-limc 25994 df-dv 25995 df-ply 26314 df-idp 26315 df-coe 26316 df-dgr 26317 df-quot 26421 df-ulm 26506 df-log 26687 df-cxp 26688 df-atan 26998 df-em 27123 df-cht 27227 df-vma 27228 df-chp 27229 df-ppi 27230 df-mu 27231 df-dchr 27363

This theorem is referenced by: rplogsum 27657

W3C validator