dchrisum0lem3

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum2.g	$⊢ G = DChr (N)$
	rpvmasum2.d	$⊢ D = {Base}_{G}$
	rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
	rpvmasum2.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
	dchrisum0.b	$⊢ φ \to X \in W$
	dchrisum0lem1.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})$
	dchrisum0.c	$⊢ φ \to C \in [0, +∞)$
	dchrisum0.s	$⊢ φ \to seq 1 (+ F) ⇝ S$
	dchrisum0.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{\sqrt{y}}$
Assertion	dchrisum0lem3	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \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		rpvmasum2.g	$⊢ G = DChr (N)$
5		rpvmasum2.d	$⊢ D = {Base}_{G}$
6		rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
7		rpvmasum2.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
8		dchrisum0.b	$⊢ φ \to X \in W$
9		dchrisum0lem1.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})$
10		dchrisum0.c	$⊢ φ \to C \in [0, +∞)$
11		dchrisum0.s	$⊢ φ \to seq 1 (+ F) ⇝ S$
12		dchrisum0.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{\sqrt{y}}$
13		1red	$⊢ φ \to 1 \in ℝ$
14		sumex	$⊢ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in V$
15	14	a1i	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in V$
16		sumex	$⊢ \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in V$
17	16	a1i	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in V$
18	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
19		difss	$⊢ D ∖ \{\underset{˙}{1}\} \subseteq D$
20	18 19	sstri	$⊢ W \subseteq D$
21	20 8	sseldi	$⊢ φ \to X \in D$
22	18 8	sseldi	$⊢ φ \to X \in (D ∖ \{\underset{˙}{1}\})$
23		eldifsni	$⊢ X \in (D ∖ \{\underset{˙}{1}\}) \to X \neq \underset{˙}{1}$
24	22 23	syl	$⊢ φ \to X \neq \underset{˙}{1}$
25		eqid	$⊢ (a \in ℕ ⟼ \frac{X (L (a))}{a}) = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
26	1 2 3 4 5 6 21 24 25	dchrmusumlema	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y})$
27	3	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to N \in ℕ$
28	8	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to X \in W$
29	10	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to C \in [0, +∞)$
30	11	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to seq 1 (+ F) ⇝ S$
31	12	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{\sqrt{y}}$
32		eqid	$⊢ (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) = (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y})$
33	32	divsqrsum	$⊢ (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) \in dom \underset{ℝ}{⇝}$
34	32	divsqrsumf	$⊢ (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) : ℝ^{+} ⟶ ℝ$
35		ax-resscn	$⊢ ℝ \subseteq ℂ$
36		fss	$⊢ ((y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) : ℝ^{+} ⟶ ℝ \land ℝ \subseteq ℂ) \to (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) : ℝ^{+} ⟶ ℂ$
37	34 35 36	mp2an	$⊢ (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) : ℝ^{+} ⟶ ℂ$
38	37	a1i	$⊢ φ \to (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) : ℝ^{+} ⟶ ℂ$
39		rpsup	$⊢ sup (ℝ^{+} ℝ^{*} <) = +∞$
40	39	a1i	$⊢ φ \to sup (ℝ^{+} ℝ^{*} <) = +∞$
41	38 40	rlimdm	$⊢ φ \to ((y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) \in dom \underset{ℝ}{⇝} \leftrightarrow (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) \underset{ℝ}{⇝} \underset{ℝ}{⇝} ((y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y})))$
42	33 41	mpbii	$⊢ φ \to (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) \underset{ℝ}{⇝} \underset{ℝ}{⇝} ((y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}))$
43	42	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}) \underset{ℝ}{⇝} \underset{ℝ}{⇝} ((y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y}))$
44		simprl	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to c \in [0, +∞)$
45		simprrl	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t$
46		simprrr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}$
47	1 2 27 4 5 6 7 28 9 29 30 31 32 43 25 44 45 46	dchrisum0lem2	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1)$
48	47	rexlimdvaa	$⊢ φ \to (\exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}) \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1))$
49	48	exlimdv	$⊢ φ \to (\exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}) \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1))$
50	26 49	mpd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1)$
51	1 2 3 4 5 6 7 8 9 10 11 12	dchrisum0lem1	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1)$
52	15 17 50 51	o1add2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) + \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1)$
53		ovexd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) + \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in V$
54		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x^{2}⌋) \in Fin$
55		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to (1 \dots ⌊\frac{x^{2}}{m}⌋) \in Fin$
56	21	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to X \in D$
57		elfzelz	$⊢ m \in (1 \dots ⌊x^{2}⌋) \to m \in ℤ$
58	57	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to m \in ℤ$
59	4 1 5 2 56 58	dchrzrhcl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to X (L (m)) \in ℂ$
60	59	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to X (L (m)) \in ℂ$
61		elfznn	$⊢ m \in (1 \dots ⌊x^{2}⌋) \to m \in ℕ$
62	61	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to m \in ℕ$
63	62	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to m \in ℝ^{+}$
64		elfznn	$⊢ d \in (1 \dots ⌊\frac{x^{2}}{m}⌋) \to d \in ℕ$
65	64	nnrpd	$⊢ d \in (1 \dots ⌊\frac{x^{2}}{m}⌋) \to d \in ℝ^{+}$
66		rpmulcl	$⊢ (m \in ℝ^{+} \land d \in ℝ^{+}) \to m d \in ℝ^{+}$
67	63 65 66	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to m d \in ℝ^{+}$
68	67	rpsqrtcld	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{m d} \in ℝ^{+}$
69	68	rpcnd	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{m d} \in ℂ$
70	68	rpne0d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{m d} \neq 0$
71	60 69 70	divcld	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \frac{X (L (m))}{\sqrt{m d}} \in ℂ$
72	55 71	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) \in ℂ$
73	54 72	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) \in ℂ$
74	73	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})\| \in ℝ$
75	74	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})\| \in ℝ$
76	62	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to m \in ℕ$
77	76	nnrpd	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to m \in ℝ^{+}$
78	77	rprege0d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to (m \in ℝ \land 0 \leq m)$
79	64	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to d \in ℕ$
80	79	nnrpd	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to d \in ℝ^{+}$
81	80	rprege0d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to (d \in ℝ \land 0 \leq d)$
82		sqrtmul	$⊢ ((m \in ℝ \land 0 \leq m) \land (d \in ℝ \land 0 \leq d)) \to \sqrt{m d} = \sqrt{m} \sqrt{d}$
83	78 81 82	syl2anc	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{m d} = \sqrt{m} \sqrt{d}$
84	83	oveq2d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \frac{X (L (m))}{\sqrt{m d}} = \frac{X (L (m))}{\sqrt{m} \sqrt{d}}$
85	77	rpsqrtcld	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{m} \in ℝ^{+}$
86	85	rpcnne0d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0)$
87	80	rpsqrtcld	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{d} \in ℝ^{+}$
88	87	rpcnne0d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to (\sqrt{d} \in ℂ \land \sqrt{d} \neq 0)$
89		divdiv1	$⊢ (X (L (m)) \in ℂ \land (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0) \land (\sqrt{d} \in ℂ \land \sqrt{d} \neq 0)) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}} = \frac{X (L (m))}{\sqrt{m} \sqrt{d}}$
90	60 86 88 89	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}} = \frac{X (L (m))}{\sqrt{m} \sqrt{d}}$
91	84 90	eqtr4d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \frac{X (L (m))}{\sqrt{m d}} = \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}$
92	91	sumeq2dv	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})$
93	92	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})$
94	93	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})$
95		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
96	95	rpred	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
97		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
98	96 97	syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ \in ℝ$
99	98	ltp1d	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ < ⌊x⌋ + 1$
100		fzdisj	$⊢ ⌊x⌋ < ⌊x⌋ + 1 \to (1 \dots ⌊x⌋) \cap (⌊x⌋ + 1 \dots ⌊x^{2}⌋) = \emptyset$
101	99 100	syl	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \cap (⌊x⌋ + 1 \dots ⌊x^{2}⌋) = \emptyset$
102	101	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x⌋) \cap (⌊x⌋ + 1 \dots ⌊x^{2}⌋) = \emptyset$
103	95	rprege0d	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 \leq x)$
104		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
105		nn0p1nn	$⊢ ⌊x⌋ \in ℕ_{0} \to ⌊x⌋ + 1 \in ℕ$
106	103 104 105	3syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ + 1 \in ℕ$
107		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
108	106 107	eleqtrdi	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ + 1 \in ℤ_{\geq 1}$
109	108	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ + 1 \in ℤ_{\geq 1}$
110	96	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ$
111		2z	$⊢ 2 \in ℤ$
112		rpexpcl	$⊢ (x \in ℝ^{+} \land 2 \in ℤ) \to x^{2} \in ℝ^{+}$
113	95 111 112	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} \in ℝ^{+}$
114	113	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x^{2} \in ℝ^{+}$
115	114	rpred	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x^{2} \in ℝ$
116	110	recnd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℂ$
117	116	mulid1d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \cdot 1 = x$
118		simprr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
119		1red	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in ℝ$
120		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
121	120	ad2antrl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \in ℝ \land 0 < x)$
122		lemul2	$⊢ (1 \in ℝ \land x \in ℝ \land (x \in ℝ \land 0 < x)) \to (1 \leq x \leftrightarrow x \cdot 1 \leq x x)$
123	119 110 121 122	syl3anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \leq x \leftrightarrow x \cdot 1 \leq x x)$
124	118 123	mpbid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \cdot 1 \leq x x$
125	117 124	eqbrtrrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \leq x x$
126	116	sqvald	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x^{2} = x x$
127	125 126	breqtrrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \leq x^{2}$
128		flword2	$⊢ (x \in ℝ \land x^{2} \in ℝ \land x \leq x^{2}) \to ⌊x^{2}⌋ \in ℤ_{\geq ⌊x⌋}$
129	110 115 127 128	syl3anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x^{2}⌋ \in ℤ_{\geq ⌊x⌋}$
130		fzsplit2	$⊢ (⌊x⌋ + 1 \in ℤ_{\geq 1} \land ⌊x^{2}⌋ \in ℤ_{\geq ⌊x⌋}) \to (1 \dots ⌊x^{2}⌋) = (1 \dots ⌊x⌋) \cup (⌊x⌋ + 1 \dots ⌊x^{2}⌋)$
131	109 129 130	syl2anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x^{2}⌋) = (1 \dots ⌊x⌋) \cup (⌊x⌋ + 1 \dots ⌊x^{2}⌋)$
132		fzfid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x^{2}⌋) \in Fin$
133	92 72	eqeltrrd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x^{2}⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in ℂ$
134	133	adantlrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊x^{2}⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in ℂ$
135	102 131 132 134	fsumsplit	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) = \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) + \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})$
136	94 135	eqtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) + \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})$
137	136	fveq2d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})\| = \|\sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) + \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\|$
138	75 137	eqled	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})\| \leq \|\sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) + \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\|$
139	13 52 53 73 138	o1le	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrisum0lem3

Proof