dchrisum0

Description: The sum sum_ n e. NN , X ( n ) / n is nonzero for all non-principal Dirichlet characters (i.e. the assumption X e. W is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 and dchrvmasumif . Lemma 9.4.4 of Shapiro, p. 382. (Contributed by Mario Carneiro, 12-May-2016)

	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$
Assertion	dchrisum0	$⊢ \neg φ$

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		eqid	$⊢ (b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) = (b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y)))$
10	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
11		difss	$⊢ D ∖ \{\underset{˙}{1}\} \subseteq D$
12	10 11	sstri	$⊢ W \subseteq D$
13	12 8	sseldi	$⊢ φ \to X \in D$
14	1 2 3 4 5 6 7 8	dchrisum0re	$⊢ φ \to X : {Base}_{Z} ⟶ ℝ$
15		fveq2	$⊢ k = m d \to \sqrt{k} = \sqrt{m d}$
16	15	oveq2d	$⊢ k = m d \to \frac{X (L (m))}{\sqrt{k}} = \frac{X (L (m))}{\sqrt{m d}}$
17		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
18	17	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
19	13	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \land m \in \{i \in ℕ \| i ∥ k\}) \to X \in D$
20		elrabi	$⊢ m \in \{i \in ℕ \| i ∥ k\} \to m \in ℕ$
21	20	nnzd	$⊢ m \in \{i \in ℕ \| i ∥ k\} \to m \in ℤ$
22	21	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \land m \in \{i \in ℕ \| i ∥ k\}) \to m \in ℤ$
23	4 1 5 2 19 22	dchrzrhcl	$⊢ (((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \land m \in \{i \in ℕ \| i ∥ k\}) \to X (L (m)) \in ℂ$
24		elfznn	$⊢ k \in (1 \dots ⌊x⌋) \to k \in ℕ$
25	24	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to k \in ℕ$
26	25	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to k \in ℝ^{+}$
27	26	rpsqrtcld	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \sqrt{k} \in ℝ^{+}$
28	27	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \sqrt{k} \in ℂ$
29	28	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \land m \in \{i \in ℕ \| i ∥ k\}) \to \sqrt{k} \in ℂ$
30	27	rpne0d	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \sqrt{k} \neq 0$
31	30	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \land m \in \{i \in ℕ \| i ∥ k\}) \to \sqrt{k} \neq 0$
32	23 29 31	divcld	$⊢ (((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \land m \in \{i \in ℕ \| i ∥ k\}) \to \frac{X (L (m))}{\sqrt{k}} \in ℂ$
33	32	anasss	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land m \in \{i \in ℕ \| i ∥ k\})) \to \frac{X (L (m))}{\sqrt{k}} \in ℂ$
34	16 18 33	dvdsflsumcom	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{k = 1}^{⌊x⌋} \sum_{m \in \{i \in ℕ \| i ∥ k\}} (\frac{X (L (m))}{\sqrt{k}}) = \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})$
35	1 2 3 4 5 6 9	dchrisum0fval	$⊢ k \in ℕ \to (b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k) = \sum_{m \in \{i \in ℕ \| i ∥ k\}} X (L (m))$
36	25 35	syl	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to (b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k) = \sum_{m \in \{i \in ℕ \| i ∥ k\}} X (L (m))$
37	36	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \frac{(b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k)}{\sqrt{k}} = \frac{\sum_{m \in \{i \in ℕ \| i ∥ k\}} X (L (m))}{\sqrt{k}}$
38		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to (1 \dots k) \in Fin$
39		dvdsssfz1	$⊢ k \in ℕ \to \{i \in ℕ \| i ∥ k\} \subseteq (1 \dots k)$
40	25 39	syl	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \{i \in ℕ \| i ∥ k\} \subseteq (1 \dots k)$
41	38 40	ssfid	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \{i \in ℕ \| i ∥ k\} \in Fin$
42	41 28 23 30	fsumdivc	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m \in \{i \in ℕ \| i ∥ k\}} X (L (m))}{\sqrt{k}} = \sum_{m \in \{i \in ℕ \| i ∥ k\}} (\frac{X (L (m))}{\sqrt{k}})$
43	37 42	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \frac{(b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k)}{\sqrt{k}} = \sum_{m \in \{i \in ℕ \| i ∥ k\}} (\frac{X (L (m))}{\sqrt{k}})$
44	43	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{k = 1}^{⌊x⌋} (\frac{(b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k)}{\sqrt{k}}) = \sum_{k = 1}^{⌊x⌋} \sum_{m \in \{i \in ℕ \| i ∥ k\}} (\frac{X (L (m))}{\sqrt{k}})$
45		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
46	45	adantl	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 \leq x)$
47		resqrtth	$⊢ (x \in ℝ \land 0 \leq x) \to {\sqrt{x}}^{2} = x$
48	46 47	syl	$⊢ (φ \land x \in ℝ^{+}) \to {\sqrt{x}}^{2} = x$
49	48	fveq2d	$⊢ (φ \land x \in ℝ^{+}) \to ⌊{\sqrt{x}}^{2}⌋ = ⌊x⌋$
50	49	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊{\sqrt{x}}^{2}⌋) = (1 \dots ⌊x⌋)$
51	48	fvoveq1d	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{{\sqrt{x}}^{2}}{m}⌋ = ⌊\frac{x}{m}⌋$
52	51	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊\frac{{\sqrt{x}}^{2}}{m}⌋) = (1 \dots ⌊\frac{x}{m}⌋)$
53	52	sumeq1d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{d = 1}^{⌊\frac{x}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})$
54	53	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊{\sqrt{x}}^{2}⌋)) \to \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{d = 1}^{⌊\frac{x}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})$
55	50 54	sumeq12dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊{\sqrt{x}}^{2}⌋} \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})$
56	34 44 55	3eqtr4d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{k = 1}^{⌊x⌋} (\frac{(b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k)}{\sqrt{k}}) = \sum_{m = 1}^{⌊{\sqrt{x}}^{2}⌋} \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})$
57	56	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{(b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k)}{\sqrt{k}})) = (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊{\sqrt{x}}^{2}⌋} \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}))$
58		rpsqrtcl	$⊢ x \in ℝ^{+} \to \sqrt{x} \in ℝ^{+}$
59	58	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \sqrt{x} \in ℝ^{+}$
60		eqidd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sqrt{x}) = (x \in ℝ^{+} ⟼ \sqrt{x})$
61		eqidd	$⊢ φ \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) = (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}))$
62		oveq1	$⊢ z = \sqrt{x} \to z^{2} = {\sqrt{x}}^{2}$
63	62	fveq2d	$⊢ z = \sqrt{x} \to ⌊z^{2}⌋ = ⌊{\sqrt{x}}^{2}⌋$
64	63	oveq2d	$⊢ z = \sqrt{x} \to (1 \dots ⌊z^{2}⌋) = (1 \dots ⌊{\sqrt{x}}^{2}⌋)$
65	62	fvoveq1d	$⊢ z = \sqrt{x} \to ⌊\frac{z^{2}}{m}⌋ = ⌊\frac{{\sqrt{x}}^{2}}{m}⌋$
66	65	oveq2d	$⊢ z = \sqrt{x} \to (1 \dots ⌊\frac{z^{2}}{m}⌋) = (1 \dots ⌊\frac{{\sqrt{x}}^{2}}{m}⌋)$
67	66	sumeq1d	$⊢ z = \sqrt{x} \to \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})$
68	67	adantr	$⊢ (z = \sqrt{x} \land m \in (1 \dots ⌊z^{2}⌋)) \to \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})$
69	64 68	sumeq12dv	$⊢ z = \sqrt{x} \to \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) = \sum_{m = 1}^{⌊{\sqrt{x}}^{2}⌋} \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})$
70	59 60 61 69	fmptco	$⊢ φ \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \circ (x \in ℝ^{+} ⟼ \sqrt{x}) = (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊{\sqrt{x}}^{2}⌋} \sum_{d = 1}^{⌊\frac{{\sqrt{x}}^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}))$
71	57 70	eqtr4d	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{(b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k)}{\sqrt{k}})) = (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \circ (x \in ℝ^{+} ⟼ \sqrt{x})$
72		eqid	$⊢ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}}) = (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})$
73	1 2 3 4 5 6 7 8 72	dchrisum0lema	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}})$
74	3	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}))) \to N \in ℕ$
75	8	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}))) \to X \in W$
76		simprl	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}))) \to c \in [0, +∞)$
77		simprrl	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}))) \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t$
78		simprrr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}))) \to \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}$
79	1 2 74 4 5 6 7 75 72 76 77 78	dchrisum0lem3	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}))) \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \in 𝑂 (1)$
80	79	rexlimdvaa	$⊢ φ \to (\exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}) \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \in 𝑂 (1))$
81	80	exlimdv	$⊢ φ \to (\exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}) \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \in 𝑂 (1))$
82	73 81	mpd	$⊢ φ \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \in 𝑂 (1)$
83		o1f	$⊢ (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \in 𝑂 (1) \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) : dom (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) ⟶ ℂ$
84	82 83	syl	$⊢ φ \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) : dom (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) ⟶ ℂ$
85		sumex	$⊢ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}) \in V$
86		eqid	$⊢ (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) = (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}}))$
87	85 86	dmmpti	$⊢ dom (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) = ℝ^{+}$
88	87	feq2i	$⊢ (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) : dom (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) ⟶ ℂ \leftrightarrow (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) : ℝ^{+} ⟶ ℂ$
89	84 88	sylib	$⊢ φ \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) : ℝ^{+} ⟶ ℂ$
90		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
91	90	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
92		resqcl	$⊢ t \in ℝ \to t^{2} \in ℝ$
93		0red	$⊢ ((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \to 0 \in ℝ$
94		simplr	$⊢ ((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \to t \in ℝ$
95		simplrr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to t^{2} \leq x$
96	45	ad2antrl	$⊢ ((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \to (x \in ℝ \land 0 \leq x)$
97	96	adantr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to (x \in ℝ \land 0 \leq x)$
98	97 47	syl	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to {\sqrt{x}}^{2} = x$
99	95 98	breqtrrd	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to t^{2} \leq {\sqrt{x}}^{2}$
100	94	adantr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to t \in ℝ$
101	59	rpred	$⊢ (φ \land x \in ℝ^{+}) \to \sqrt{x} \in ℝ$
102	101	ad2ant2r	$⊢ ((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \to \sqrt{x} \in ℝ$
103	102	adantr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to \sqrt{x} \in ℝ$
104		simpr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to 0 \leq t$
105		sqrtge0	$⊢ (x \in ℝ \land 0 \leq x) \to 0 \leq \sqrt{x}$
106	96 105	syl	$⊢ ((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \to 0 \leq \sqrt{x}$
107	106	adantr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to 0 \leq \sqrt{x}$
108	100 103 104 107	le2sqd	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to (t \leq \sqrt{x} \leftrightarrow t^{2} \leq {\sqrt{x}}^{2})$
109	99 108	mpbird	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land 0 \leq t) \to t \leq \sqrt{x}$
110	94	adantr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land t \leq 0) \to t \in ℝ$
111		0red	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land t \leq 0) \to 0 \in ℝ$
112	102	adantr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land t \leq 0) \to \sqrt{x} \in ℝ$
113		simpr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land t \leq 0) \to t \leq 0$
114	106	adantr	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land t \leq 0) \to 0 \leq \sqrt{x}$
115	110 111 112 113 114	letrd	$⊢ (((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \land t \leq 0) \to t \leq \sqrt{x}$
116	93 94 109 115	lecasei	$⊢ ((φ \land t \in ℝ) \land (x \in ℝ^{+} \land t^{2} \leq x)) \to t \leq \sqrt{x}$
117	116	expr	$⊢ ((φ \land t \in ℝ) \land x \in ℝ^{+}) \to (t^{2} \leq x \to t \leq \sqrt{x})$
118	117	ralrimiva	$⊢ (φ \land t \in ℝ) \to \forall x \in ℝ^{+} (t^{2} \leq x \to t \leq \sqrt{x})$
119		breq1	$⊢ c = t^{2} \to (c \leq x \leftrightarrow t^{2} \leq x)$
120	119	rspceaimv	$⊢ (t^{2} \in ℝ \land \forall x \in ℝ^{+} (t^{2} \leq x \to t \leq \sqrt{x})) \to \exists c \in ℝ \forall x \in ℝ^{+} (c \leq x \to t \leq \sqrt{x})$
121	92 118 120	syl2an2	$⊢ (φ \land t \in ℝ) \to \exists c \in ℝ \forall x \in ℝ^{+} (c \leq x \to t \leq \sqrt{x})$
122	89 82 59 91 121	o1compt	$⊢ φ \to (z \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊z^{2}⌋} \sum_{d = 1}^{⌊\frac{z^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m d}})) \circ (x \in ℝ^{+} ⟼ \sqrt{x}) \in 𝑂 (1)$
123	71 122	eqeltrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{(b \in ℕ ⟼ \sum_{y \in \{i \in ℕ \| i ∥ b\}} X (L (y))) (k)}{\sqrt{k}})) \in 𝑂 (1)$
124	1 2 3 4 5 6 9 13 14 123	dchrisum0fno1	$⊢ \neg φ$

Metamath Proof Explorer

Theorem dchrisum0

Proof