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 24932

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 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) → 𝑁 ∈ ℕ)
5		eqid 2609	. . . . . . . . . . . . . 14 ⊢ (DChr‘𝑁) = (DChr‘𝑁)
6		eqid 2609	. . . . . . . . . . . . . 14 ⊢ (Base‘(DChr‘𝑁)) = (Base‘(DChr‘𝑁))
7		eqid 2609	. . . . . . . . . . . . . 14 ⊢ (0_g‘(DChr‘𝑁)) = (0_g‘(DChr‘𝑁))
8		fveq2 6088	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (𝐿‘𝑚) = (𝐿‘𝑛))
9	8	fveq2d 6092	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝑦‘(𝐿‘𝑚)) = (𝑦‘(𝐿‘𝑛)))
10		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛)
11	9, 10	oveq12d 6545	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → ((𝑦‘(𝐿‘𝑚)) / 𝑚) = ((𝑦‘(𝐿‘𝑛)) / 𝑛))
12	11	cbvsumv 14220	. . . . . . . . . . . . . . . . 17 ⊢ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = Σ𝑛 ∈ ℕ ((𝑦‘(𝐿‘𝑛)) / 𝑛)
13	12	eqeq1i 2614	. . . . . . . . . . . . . . . 16 ⊢ (Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0 ↔ Σ𝑛 ∈ ℕ ((𝑦‘(𝐿‘𝑛)) / 𝑛) = 0)
14	13	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) → (Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0 ↔ Σ𝑛 ∈ ℕ ((𝑦‘(𝐿‘𝑛)) / 𝑛) = 0))
15	14	rabbiia 3160	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} = {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑛 ∈ ℕ ((𝑦‘(𝐿‘𝑛)) / 𝑛) = 0}
16		simpr 475	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) → 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})
17	1, 2, 4, 5, 6, 7, 15, 16	dchrisum0 24926	. . . . . . . . . . . . 13 ⊢ ¬ (𝜑 ∧ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})
18	17	imnani 437	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})
19	18	eq0rdv 3930	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} = ∅)
20	19	fveq2d 6092	. . . . . . . . . 10 ⊢ (𝜑 → (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) = (#‘∅))
21		hash0 12971	. . . . . . . . . 10 ⊢ (#‘∅) = 0
22	20, 21	syl6eq 2659	. . . . . . . . 9 ⊢ (𝜑 → (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) = 0)
23	22	oveq2d 6543	. . . . . . . 8 ⊢ (𝜑 → (1 − (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})) = (1 − 0))
24		1m0e1 10978	. . . . . . . 8 ⊢ (1 − 0) = 1
25	23, 24	syl6eq 2659	. . . . . . 7 ⊢ (𝜑 → (1 − (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})) = 1)
26	25	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1 − (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})) = 1)
27	26	oveq2d 6543	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((log‘𝑥) · (1 − (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}))) = ((log‘𝑥) · 1))
28		relogcl 24043	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
29	28	adantl 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
30	29	recnd 9924	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
31	30	mulid1d 9913	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((log‘𝑥) · 1) = (log‘𝑥))
32	27, 31	eqtrd 2643	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((log‘𝑥) · (1 − (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}))) = (log‘𝑥))
33	32	oveq2d 6543	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0})))) = (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
34	33	mpteq2dva 4666	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}))))) = (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
35		eqid 2609	. . 3 ⊢ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} = {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}
36		rpvmasum.u	. . 3 ⊢ 𝑈 = (Unit‘𝑍)
37		rpvmasum.b	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
38		rpvmasum.t	. . 3 ⊢ 𝑇 = (^◡𝐿 “ {𝐴})
39	17	pm2.21i 114	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}) → 𝐴 = (1_r‘𝑍))
40	1, 2, 3, 5, 6, 7, 35, 36, 37, 38, 39	rpvmasum2 24918	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘{𝑦 ∈ ((Base‘(DChr‘𝑁)) ∖ {(0_g‘(DChr‘𝑁))}) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}))))) ∈ 𝑂(1))
41	34, 40	eqeltrrd 2688	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 194 ∧ wa 382 = wceq 1474 ∈ wcel 1976 {crab 2899 ∖ cdif 3536 ∩ cin 3538 ∅c0 3873 {csn 4124 ↦ cmpt 4637 ^◡ccnv 5027 “ cima 5031 ‘cfv 5790 (class class class)co 6527 ℝcr 9791 0cc0 9792 1c1 9793 · cmul 9797 − cmin 10117 / cdiv 10533 ℕcn 10867 ℝ⁺crp 11664 ...cfz 12152 ⌊cfl 12408 #chash 12934 𝑂(1)co1 14011 Σcsu 14210 ϕcphi 15253 Basecbs 15641 0_gc0g 15869 1_rcur 18270 Unitcui 18408 ℤRHomczrh 19612 ℤ/nℤczn 19615 logclog 24022 Λcvma 24535 DChrcdchr 24674

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2033 ax-13 2233 ax-ext 2589 ax-rep 4693 ax-sep 4703 ax-nul 4712 ax-pow 4764 ax-pr 4828 ax-un 6824 ax-inf2 8398 ax-cnex 9848 ax-resscn 9849 ax-1cn 9850 ax-icn 9851 ax-addcl 9852 ax-addrcl 9853 ax-mulcl 9854 ax-mulrcl 9855 ax-mulcom 9856 ax-addass 9857 ax-mulass 9858 ax-distr 9859 ax-i2m1 9860 ax-1ne0 9861 ax-1rid 9862 ax-rnegex 9863 ax-rrecex 9864 ax-cnre 9865 ax-pre-lttri 9866 ax-pre-lttrn 9867 ax-pre-ltadd 9868 ax-pre-mulgt0 9869 ax-pre-sup 9870 ax-addf 9871 ax-mulf 9872

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2461 df-mo 2462 df-clab 2596 df-cleq 2602 df-clel 2605 df-nfc 2739 df-ne 2781 df-nel 2782 df-ral 2900 df-rex 2901 df-reu 2902 df-rmo 2903 df-rab 2904 df-v 3174 df-sbc 3402 df-csb 3499 df-dif 3542 df-un 3544 df-in 3546 df-ss 3553 df-pss 3555 df-nul 3874 df-if 4036 df-pw 4109 df-sn 4125 df-pr 4127 df-tp 4129 df-op 4131 df-uni 4367 df-int 4405 df-iun 4451 df-iin 4452 df-disj 4548 df-br 4578 df-opab 4638 df-mpt 4639 df-tr 4675 df-eprel 4939 df-id 4943 df-po 4949 df-so 4950 df-fr 4987 df-se 4988 df-we 4989 df-xp 5034 df-rel 5035 df-cnv 5036 df-co 5037 df-dm 5038 df-rn 5039 df-res 5040 df-ima 5041 df-pred 5583 df-ord 5629 df-on 5630 df-lim 5631 df-suc 5632 df-iota 5754 df-fun 5792 df-fn 5793 df-f 5794 df-f1 5795 df-fo 5796 df-f1o 5797 df-fv 5798 df-isom 5799 df-riota 6489 df-ov 6530 df-oprab 6531 df-mpt2 6532 df-of 6772 df-rpss 6812 df-om 6935 df-1st 7036 df-2nd 7037 df-supp 7160 df-tpos 7216 df-wrecs 7271 df-recs 7332 df-rdg 7370 df-1o 7424 df-2o 7425 df-oadd 7428 df-omul 7429 df-er 7606 df-ec 7608 df-qs 7612 df-map 7723 df-pm 7724 df-ixp 7772 df-en 7819 df-dom 7820 df-sdom 7821 df-fin 7822 df-fsupp 8136 df-fi 8177 df-sup 8208 df-inf 8209 df-oi 8275 df-card 8625 df-acn 8628 df-cda 8850 df-pnf 9932 df-mnf 9933 df-xr 9934 df-ltxr 9935 df-le 9936 df-sub 10119 df-neg 10120 df-div 10534 df-nn 10868 df-2 10926 df-3 10927 df-4 10928 df-5 10929 df-6 10930 df-7 10931 df-8 10932 df-9 10933 df-n0 11140 df-z 11211 df-dec 11326 df-uz 11520 df-q 11621 df-rp 11665 df-xneg 11778 df-xadd 11779 df-xmul 11780 df-ioo 12006 df-ioc 12007 df-ico 12008 df-icc 12009 df-fz 12153 df-fzo 12290 df-fl 12410 df-mod 12486 df-seq 12619 df-exp 12678 df-fac 12878 df-bc 12907 df-hash 12935 df-word 13100 df-concat 13102 df-s1 13103 df-shft 13601 df-cj 13633 df-re 13634 df-im 13635 df-sqrt 13769 df-abs 13770 df-limsup 13996 df-clim 14013 df-rlim 14014 df-o1 14015 df-lo1 14016 df-sum 14211 df-ef 14583 df-e 14584 df-sin 14585 df-cos 14586 df-pi 14588 df-dvds 14768 df-gcd 15001 df-prm 15170 df-numer 15227 df-denom 15228 df-phi 15255 df-pc 15326 df-struct 15643 df-ndx 15644 df-slot 15645 df-base 15646 df-sets 15647 df-ress 15648 df-plusg 15727 df-mulr 15728 df-starv 15729 df-sca 15730 df-vsca 15731 df-ip 15732 df-tset 15733 df-ple 15734 df-ds 15737 df-unif 15738 df-hom 15739 df-cco 15740 df-rest 15852 df-topn 15853 df-0g 15871 df-gsum 15872 df-topgen 15873 df-pt 15874 df-prds 15877 df-xrs 15931 df-qtop 15936 df-imas 15937 df-qus 15938 df-xps 15939 df-mre 16015 df-mrc 16016 df-acs 16018 df-mgm 17011 df-sgrp 17053 df-mnd 17064 df-mhm 17104 df-submnd 17105 df-grp 17194 df-minusg 17195 df-sbg 17196 df-mulg 17310 df-subg 17360 df-nsg 17361 df-eqg 17362 df-ghm 17427 df-gim 17470 df-ga 17492 df-cntz 17519 df-oppg 17545 df-od 17717 df-gex 17718 df-pgp 17719 df-lsm 17820 df-pj1 17821 df-cmn 17964 df-abl 17965 df-cyg 18049 df-dprd 18163 df-dpj 18164 df-mgp 18259 df-ur 18271 df-ring 18318 df-cring 18319 df-oppr 18392 df-dvdsr 18410 df-unit 18411 df-invr 18441 df-dvr 18452 df-rnghom 18484 df-drng 18518 df-subrg 18547 df-lmod 18634 df-lss 18700 df-lsp 18739 df-sra 18939 df-rgmod 18940 df-lidl 18941 df-rsp 18942 df-2idl 18999 df-psmet 19505 df-xmet 19506 df-met 19507 df-bl 19508 df-mopn 19509 df-fbas 19510 df-fg 19511 df-cnfld 19514 df-zring 19584 df-zrh 19616 df-zn 19619 df-top 20463 df-bases 20464 df-topon 20465 df-topsp 20466 df-cld 20575 df-ntr 20576 df-cls 20577 df-nei 20654 df-lp 20692 df-perf 20693 df-cn 20783 df-cnp 20784 df-haus 20871 df-cmp 20942 df-tx 21117 df-hmeo 21310 df-fil 21402 df-fm 21494 df-flim 21495 df-flf 21496 df-xms 21876 df-ms 21877 df-tms 21878 df-cncf 22420 df-0p 23160 df-limc 23353 df-dv 23354 df-ply 23665 df-idp 23666 df-coe 23667 df-dgr 23668 df-quot 23767 df-log 24024 df-cxp 24025 df-em 24436 df-cht 24540 df-vma 24541 df-chp 24542 df-ppi 24543 df-mu 24544 df-dchr 24675

This theorem is referenced by: rplogsum 24933

W3C validator