dchrisum0lema

Description: Lemma for dchrisum0 . Apply dchrisum for the function 1 / sqrt y . (Contributed by Mario Carneiro, 10-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$
	dchrisum0lem1.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})$
Assertion	dchrisum0lema	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}})$

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	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
11	10 8	sseldi	$⊢ φ \to X \in (D ∖ \{\underset{˙}{1}\})$
12	11	eldifad	$⊢ φ \to X \in D$
13		eldifsni	$⊢ X \in (D ∖ \{\underset{˙}{1}\}) \to X \neq \underset{˙}{1}$
14	11 13	syl	$⊢ φ \to X \neq \underset{˙}{1}$
15		fveq2	$⊢ n = x \to \sqrt{n} = \sqrt{x}$
16	15	oveq2d	$⊢ n = x \to \frac{1}{\sqrt{n}} = \frac{1}{\sqrt{x}}$
17		1nn	$⊢ 1 \in ℕ$
18	17	a1i	$⊢ φ \to 1 \in ℕ$
19		rpsqrtcl	$⊢ n \in ℝ^{+} \to \sqrt{n} \in ℝ^{+}$
20	19	adantl	$⊢ (φ \land n \in ℝ^{+}) \to \sqrt{n} \in ℝ^{+}$
21	20	rprecred	$⊢ (φ \land n \in ℝ^{+}) \to \frac{1}{\sqrt{n}} \in ℝ$
22		simp3r	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to n \leq x$
23		simp2l	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to n \in ℝ^{+}$
24	23	rprege0d	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to (n \in ℝ \land 0 \leq n)$
25		simp2r	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to x \in ℝ^{+}$
26	25	rprege0d	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to (x \in ℝ \land 0 \leq x)$
27		sqrtle	$⊢ ((n \in ℝ \land 0 \leq n) \land (x \in ℝ \land 0 \leq x)) \to (n \leq x \leftrightarrow \sqrt{n} \leq \sqrt{x})$
28	24 26 27	syl2anc	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to (n \leq x \leftrightarrow \sqrt{n} \leq \sqrt{x})$
29	22 28	mpbid	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to \sqrt{n} \leq \sqrt{x}$
30	23	rpsqrtcld	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to \sqrt{n} \in ℝ^{+}$
31	25	rpsqrtcld	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to \sqrt{x} \in ℝ^{+}$
32	30 31	lerecd	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to (\sqrt{n} \leq \sqrt{x} \leftrightarrow \frac{1}{\sqrt{x}} \leq \frac{1}{\sqrt{n}})$
33	29 32	mpbid	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (1 \leq n \land n \leq x)) \to \frac{1}{\sqrt{x}} \leq \frac{1}{\sqrt{n}}$
34		sqrtlim	$⊢ (n \in ℝ^{+} ⟼ \frac{1}{\sqrt{n}}) \underset{ℝ}{⇝} 0$
35	34	a1i	$⊢ φ \to (n \in ℝ^{+} ⟼ \frac{1}{\sqrt{n}}) \underset{ℝ}{⇝} 0$
36		2fveq3	$⊢ a = n \to X (L (a)) = X (L (n))$
37		fveq2	$⊢ a = n \to \sqrt{a} = \sqrt{n}$
38	37	oveq2d	$⊢ a = n \to \frac{1}{\sqrt{a}} = \frac{1}{\sqrt{n}}$
39	36 38	oveq12d	$⊢ a = n \to X (L (a)) (\frac{1}{\sqrt{a}}) = X (L (n)) (\frac{1}{\sqrt{n}})$
40	39	cbvmptv	$⊢ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}})) = (n \in ℕ ⟼ X (L (n)) (\frac{1}{\sqrt{n}}))$
41	1 2 3 4 5 6 12 14 16 18 21 33 35 40	dchrisum	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) ⇝ t \land \forall x \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋) - t\| \leq c (\frac{1}{\sqrt{x}}))$
42	12	adantr	$⊢ (φ \land n \in ℕ) \to X \in D$
43		nnz	$⊢ n \in ℕ \to n \in ℤ$
44	43	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℤ$
45	4 1 5 2 42 44	dchrzrhcl	$⊢ (φ \land n \in ℕ) \to X (L (n)) \in ℂ$
46		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
47	46	nnrpd	$⊢ (φ \land n \in ℕ) \to n \in ℝ^{+}$
48	47	rpsqrtcld	$⊢ (φ \land n \in ℕ) \to \sqrt{n} \in ℝ^{+}$
49	48	rpcnd	$⊢ (φ \land n \in ℕ) \to \sqrt{n} \in ℂ$
50	48	rpne0d	$⊢ (φ \land n \in ℕ) \to \sqrt{n} \neq 0$
51	45 49 50	divrecd	$⊢ (φ \land n \in ℕ) \to \frac{X (L (n))}{\sqrt{n}} = X (L (n)) (\frac{1}{\sqrt{n}})$
52	51	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ \frac{X (L (n))}{\sqrt{n}}) = (n \in ℕ ⟼ X (L (n)) (\frac{1}{\sqrt{n}}))$
53	36 37	oveq12d	$⊢ a = n \to \frac{X (L (a))}{\sqrt{a}} = \frac{X (L (n))}{\sqrt{n}}$
54	53	cbvmptv	$⊢ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}}) = (n \in ℕ ⟼ \frac{X (L (n))}{\sqrt{n}})$
55	9 54	eqtri	$⊢ F = (n \in ℕ ⟼ \frac{X (L (n))}{\sqrt{n}})$
56	52 55 40	3eqtr4g	$⊢ φ \to F = (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))$
57	56	seqeq3d	$⊢ φ \to seq 1 (+ F) = seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}})))$
58	57	breq1d	$⊢ φ \to (seq 1 (+ F) ⇝ t \leftrightarrow seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) ⇝ t)$
59	58	adantr	$⊢ (φ \land c \in [0, +∞)) \to (seq 1 (+ F) ⇝ t \leftrightarrow seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) ⇝ t)$
60		2fveq3	$⊢ y = x \to seq 1 (+ F) (⌊y⌋) = seq 1 (+ F) (⌊x⌋)$
61	60	fvoveq1d	$⊢ y = x \to \|seq 1 (+ F) (⌊y⌋) - t\| = \|seq 1 (+ F) (⌊x⌋) - t\|$
62		fveq2	$⊢ y = x \to \sqrt{y} = \sqrt{x}$
63	62	oveq2d	$⊢ y = x \to \frac{c}{\sqrt{y}} = \frac{c}{\sqrt{x}}$
64	61 63	breq12d	$⊢ y = x \to (\|seq 1 (+ F) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}} \leftrightarrow \|seq 1 (+ F) (⌊x⌋) - t\| \leq \frac{c}{\sqrt{x}})$
65	64	cbvralvw	$⊢ \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}} \leftrightarrow \forall x \in [1, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq \frac{c}{\sqrt{x}}$
66	56	ad2antrr	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to F = (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))$
67	66	seqeq3d	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to seq 1 (+ F) = seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}})))$
68	67	fveq1d	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to seq 1 (+ F) (⌊x⌋) = seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋)$
69	68	fvoveq1d	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to \|seq 1 (+ F) (⌊x⌋) - t\| = \|seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋) - t\|$
70		elrege0	$⊢ c \in [0, +∞) \leftrightarrow (c \in ℝ \land 0 \leq c)$
71	70	simplbi	$⊢ c \in [0, +∞) \to c \in ℝ$
72	71	ad2antlr	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to c \in ℝ$
73	72	recnd	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to c \in ℂ$
74		1re	$⊢ 1 \in ℝ$
75		elicopnf	$⊢ 1 \in ℝ \to (x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x))$
76	74 75	ax-mp	$⊢ x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x)$
77	76	simplbi	$⊢ x \in [1, +∞) \to x \in ℝ$
78	77	adantl	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to x \in ℝ$
79		0red	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to 0 \in ℝ$
80		1red	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to 1 \in ℝ$
81		0lt1	$⊢ 0 < 1$
82	81	a1i	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to 0 < 1$
83	76	simprbi	$⊢ x \in [1, +∞) \to 1 \leq x$
84	83	adantl	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to 1 \leq x$
85	79 80 78 82 84	ltletrd	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to 0 < x$
86	78 85	elrpd	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to x \in ℝ^{+}$
87	86	rpsqrtcld	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to \sqrt{x} \in ℝ^{+}$
88	87	rpcnd	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to \sqrt{x} \in ℂ$
89	87	rpne0d	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to \sqrt{x} \neq 0$
90	73 88 89	divrecd	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to \frac{c}{\sqrt{x}} = c (\frac{1}{\sqrt{x}})$
91	69 90	breq12d	$⊢ ((φ \land c \in [0, +∞)) \land x \in [1, +∞)) \to (\|seq 1 (+ F) (⌊x⌋) - t\| \leq \frac{c}{\sqrt{x}} \leftrightarrow \|seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋) - t\| \leq c (\frac{1}{\sqrt{x}}))$
92	91	ralbidva	$⊢ (φ \land c \in [0, +∞)) \to (\forall x \in [1, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq \frac{c}{\sqrt{x}} \leftrightarrow \forall x \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋) - t\| \leq c (\frac{1}{\sqrt{x}}))$
93	65 92	syl5bb	$⊢ (φ \land c \in [0, +∞)) \to (\forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}} \leftrightarrow \forall x \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋) - t\| \leq c (\frac{1}{\sqrt{x}}))$
94	59 93	anbi12d	$⊢ (φ \land c \in [0, +∞)) \to ((seq 1 (+ F) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}) \leftrightarrow (seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) ⇝ t \land \forall x \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋) - t\| \leq c (\frac{1}{\sqrt{x}})))$
95	94	rexbidva	$⊢ φ \to (\exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}) \leftrightarrow \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) ⇝ t \land \forall x \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋) - t\| \leq c (\frac{1}{\sqrt{x}})))$
96	95	exbidv	$⊢ φ \to (\exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}}) \leftrightarrow \exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) ⇝ t \land \forall x \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ X (L (a)) (\frac{1}{\sqrt{a}}))) (⌊x⌋) - t\| \leq c (\frac{1}{\sqrt{x}})))$
97	41 96	mpbird	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq \frac{c}{\sqrt{y}})$

Metamath Proof Explorer

Theorem dchrisum0lema

Proof