dchrvmasumlem3

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.g	$⊢ G = DChr (N)$
	rpvmasum.d	$⊢ D = {Base}_{G}$
	rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum.b	$⊢ φ \to X \in D$
	dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrvmasum.f	$⊢ (φ \land m \in ℝ^{+}) \to F \in ℂ$
	dchrvmasum.g	$⊢ m = \frac{x}{d} \to F = K$
	dchrvmasum.c	$⊢ φ \to C \in [0, +∞)$
	dchrvmasum.t	$⊢ φ \to T \in ℂ$
	dchrvmasum.1	$⊢ (φ \land m \in [3, +∞)) \to \|F - T\| \leq C (\frac{\log m}{m})$
	dchrvmasum.r	$⊢ φ \to R \in ℝ$
	dchrvmasum.2	$⊢ φ \to \forall m \in [1, 3) \|F - T\| \leq R$
Assertion	dchrvmasumlem3	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (K - T)) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum.g	$⊢ G = DChr (N)$
5		rpvmasum.d	$⊢ D = {Base}_{G}$
6		rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum.b	$⊢ φ \to X \in D$
8		dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrvmasum.f	$⊢ (φ \land m \in ℝ^{+}) \to F \in ℂ$
10		dchrvmasum.g	$⊢ m = \frac{x}{d} \to F = K$
11		dchrvmasum.c	$⊢ φ \to C \in [0, +∞)$
12		dchrvmasum.t	$⊢ φ \to T \in ℂ$
13		dchrvmasum.1	$⊢ (φ \land m \in [3, +∞)) \to \|F - T\| \leq C (\frac{\log m}{m})$
14		dchrvmasum.r	$⊢ φ \to R \in ℝ$
15		dchrvmasum.2	$⊢ φ \to \forall m \in [1, 3) \|F - T\| \leq R$
16		1red	$⊢ φ \to 1 \in ℝ$
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	dchrvmasumlem2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})) \in 𝑂 (1)$
18		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
19	10	eleq1d	$⊢ m = \frac{x}{d} \to (F \in ℂ \leftrightarrow K \in ℂ)$
20	9	ralrimiva	$⊢ φ \to \forall m \in ℝ^{+} F \in ℂ$
21	20	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \forall m \in ℝ^{+} F \in ℂ$
22		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
23		elfznn	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℕ$
24	23	nnrpd	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℝ^{+}$
25		rpdivcl	$⊢ (x \in ℝ^{+} \land d \in ℝ^{+}) \to \frac{x}{d} \in ℝ^{+}$
26	22 24 25	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{x}{d} \in ℝ^{+}$
27	19 21 26	rspcdva	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to K \in ℂ$
28	12	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to T \in ℂ$
29	27 28	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to K - T \in ℂ$
30	29	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|K - T\| \in ℝ$
31	23	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℕ$
32	30 31	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|K - T\|}{d} \in ℝ$
33	18 32	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d}) \in ℝ$
34	7	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X \in D$
35		elfzelz	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℤ$
36	35	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℤ$
37	4 1 5 2 34 36	dchrzrhcl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) \in ℂ$
38		mucl	$⊢ d \in ℕ \to μ (d) \in ℤ$
39	31 38	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to μ (d) \in ℤ$
40	39	zred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to μ (d) \in ℝ$
41	40 31	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{μ (d)}{d} \in ℝ$
42	41	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{μ (d)}{d} \in ℂ$
43	37 42	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
44	43 29	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) (K - T) \in ℂ$
45	18 44	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (K - T) \in ℂ$
46	45	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \in ℝ$
47	33	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d}) \in ℂ$
48	47	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\| \in ℝ$
49	44	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \in ℝ$
50	18 49	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} \|X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \in ℝ$
51	18 44	fsumabs	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \leq \sum_{d = 1}^{⌊x⌋} \|X (L (d)) (\frac{μ (d)}{d}) (K - T)\|$
52	43	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d})\| \in ℝ$
53	31	nnrecred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{1}{d} \in ℝ$
54	29	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \|K - T\|$
55	37 42	absmuld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d})\| = \|X (L (d))\| \|\frac{μ (d)}{d}\|$
56	37	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d))\| \in ℝ$
57		1red	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
58	42	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{μ (d)}{d}\| \in ℝ$
59	37	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \|X (L (d))\|$
60	42	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \|\frac{μ (d)}{d}\|$
61		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
62	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
63	1 61 2	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
64	62 63	syl	$⊢ φ \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
65		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Z} \to L : ℤ ⟶ {Base}_{Z}$
66	64 65	syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Z}$
67	66	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to L : ℤ ⟶ {Base}_{Z}$
68	67 36	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to L (d) \in {Base}_{Z}$
69	4 5 1 61 34 68	dchrabs2	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d))\| \leq 1$
70	40	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to μ (d) \in ℂ$
71	31	nncnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℂ$
72	31	nnne0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \neq 0$
73	70 71 72	absdivd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{μ (d)}{d}\| = \frac{\|μ (d)\|}{\|d\|}$
74	31	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℝ^{+}$
75	74	rprege0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (d \in ℝ \land 0 \leq d)$
76		absid	$⊢ (d \in ℝ \land 0 \leq d) \to \|d\| = d$
77	75 76	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|d\| = d$
78	77	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|μ (d)\|}{\|d\|} = \frac{\|μ (d)\|}{d}$
79	73 78	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{μ (d)}{d}\| = \frac{\|μ (d)\|}{d}$
80	70	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|μ (d)\| \in ℝ$
81		mule1	$⊢ d \in ℕ \to \|μ (d)\| \leq 1$
82	31 81	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|μ (d)\| \leq 1$
83	80 57 74 82	lediv1dd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|μ (d)\|}{d} \leq \frac{1}{d}$
84	79 83	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{μ (d)}{d}\| \leq \frac{1}{d}$
85	56 57 58 53 59 60 69 84	lemul12ad	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d))\| \|\frac{μ (d)}{d}\| \leq 1 (\frac{1}{d})$
86	53	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{1}{d} \in ℂ$
87	86	mullidd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 (\frac{1}{d}) = \frac{1}{d}$
88	85 87	breqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d))\| \|\frac{μ (d)}{d}\| \leq \frac{1}{d}$
89	55 88	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d})\| \leq \frac{1}{d}$
90	52 53 30 54 89	lemul1ad	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d})\| \|K - T\| \leq (\frac{1}{d}) \|K - T\|$
91	43 29	absmuld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d}) (K - T)\| = \|X (L (d)) (\frac{μ (d)}{d})\| \|K - T\|$
92	30	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|K - T\| \in ℂ$
93	92 71 72	divrec2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|K - T\|}{d} = (\frac{1}{d}) \|K - T\|$
94	90 91 93	3brtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \leq \frac{\|K - T\|}{d}$
95	18 49 32 94	fsumle	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} \|X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \leq \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})$
96	46 50 33 51 95	letrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \leq \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})$
97	33	leabsd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d}) \leq \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\|$
98	46 33 48 96 97	letrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \leq \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\|$
99	98	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (K - T)\| \leq \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\|$
100	16 17 33 45 99	o1le	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (K - T)) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrvmasumlem3

Proof