dchrvmasumlema

Description: Lemma for dchrvmasum and dchrvmasumif . Apply dchrisum for the function log ( y ) / y , which is decreasing above _e (or above 3, the nearest integer bound). (Contributed by Mario Carneiro, 5-May-2016)

	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}$
	dchrvmasumlema.f	$⊢ F = (a \in ℕ ⟼ X (L (a)) (\frac{\log a}{a}))$
Assertion	dchrvmasumlema	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall y \in [3, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq c (\frac{\log y}{y}))$

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		dchrvmasumlema.f	$⊢ F = (a \in ℕ ⟼ X (L (a)) (\frac{\log a}{a}))$
10		fveq2	$⊢ n = x \to \log n = \log x$
11		id	$⊢ n = x \to n = x$
12	10 11	oveq12d	$⊢ n = x \to \frac{\log n}{n} = \frac{\log x}{x}$
13		3nn	$⊢ 3 \in ℕ$
14	13	a1i	$⊢ φ \to 3 \in ℕ$
15		relogcl	$⊢ n \in ℝ^{+} \to \log n \in ℝ$
16		rerpdivcl	$⊢ (\log n \in ℝ \land n \in ℝ^{+}) \to \frac{\log n}{n} \in ℝ$
17	15 16	mpancom	$⊢ n \in ℝ^{+} \to \frac{\log n}{n} \in ℝ$
18	17	adantl	$⊢ (φ \land n \in ℝ^{+}) \to \frac{\log n}{n} \in ℝ$
19		simp3r	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to n \leq x$
20		simp2l	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to n \in ℝ^{+}$
21	20	rpred	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to n \in ℝ$
22		ere	$⊢ e \in ℝ$
23	22	a1i	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to e \in ℝ$
24		3re	$⊢ 3 \in ℝ$
25	24	a1i	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to 3 \in ℝ$
26		egt2lt3	$⊢ (2 < e \land e < 3)$
27	26	simpri	$⊢ e < 3$
28	22 24 27	ltleii	$⊢ e \leq 3$
29	28	a1i	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to e \leq 3$
30		simp3l	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to 3 \leq n$
31	23 25 21 29 30	letrd	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to e \leq n$
32		simp2r	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to x \in ℝ^{+}$
33	32	rpred	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to x \in ℝ$
34	23 21 33 31 19	letrd	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to e \leq x$
35		logdivle	$⊢ ((n \in ℝ \land e \leq n) \land (x \in ℝ \land e \leq x)) \to (n \leq x \leftrightarrow \frac{\log x}{x} \leq \frac{\log n}{n})$
36	21 31 33 34 35	syl22anc	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to (n \leq x \leftrightarrow \frac{\log x}{x} \leq \frac{\log n}{n})$
37	19 36	mpbid	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (3 \leq n \land n \leq x)) \to \frac{\log x}{x} \leq \frac{\log n}{n}$
38		rpcn	$⊢ n \in ℝ^{+} \to n \in ℂ$
39	38	cxp1d	$⊢ n \in ℝ^{+} \to n^{1} = n$
40	39	oveq2d	$⊢ n \in ℝ^{+} \to \frac{\log n}{n^{1}} = \frac{\log n}{n}$
41	40	mpteq2ia	$⊢ (n \in ℝ^{+} ⟼ \frac{\log n}{n^{1}}) = (n \in ℝ^{+} ⟼ \frac{\log n}{n})$
42		1rp	$⊢ 1 \in ℝ^{+}$
43		cxploglim	$⊢ 1 \in ℝ^{+} \to (n \in ℝ^{+} ⟼ \frac{\log n}{n^{1}}) \underset{ℝ}{⇝} 0$
44	42 43	mp1i	$⊢ φ \to (n \in ℝ^{+} ⟼ \frac{\log n}{n^{1}}) \underset{ℝ}{⇝} 0$
45	41 44	eqbrtrrid	$⊢ φ \to (n \in ℝ^{+} ⟼ \frac{\log n}{n}) \underset{ℝ}{⇝} 0$
46		2fveq3	$⊢ a = n \to X (L (a)) = X (L (n))$
47		fveq2	$⊢ a = n \to \log a = \log n$
48		id	$⊢ a = n \to a = n$
49	47 48	oveq12d	$⊢ a = n \to \frac{\log a}{a} = \frac{\log n}{n}$
50	46 49	oveq12d	$⊢ a = n \to X (L (a)) (\frac{\log a}{a}) = X (L (n)) (\frac{\log n}{n})$
51	50	cbvmptv	$⊢ (a \in ℕ ⟼ X (L (a)) (\frac{\log a}{a})) = (n \in ℕ ⟼ X (L (n)) (\frac{\log n}{n}))$
52	9 51	eqtri	$⊢ F = (n \in ℕ ⟼ X (L (n)) (\frac{\log n}{n}))$
53	1 2 3 4 5 6 7 8 12 14 18 37 45 52	dchrisum	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [3, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c (\frac{\log x}{x}))$
54		2fveq3	$⊢ x = y \to seq 1 (+ F) (⌊x⌋) = seq 1 (+ F) (⌊y⌋)$
55	54	fvoveq1d	$⊢ x = y \to \|seq 1 (+ F) (⌊x⌋) - t\| = \|seq 1 (+ F) (⌊y⌋) - t\|$
56		fveq2	$⊢ x = y \to \log x = \log y$
57		id	$⊢ x = y \to x = y$
58	56 57	oveq12d	$⊢ x = y \to \frac{\log x}{x} = \frac{\log y}{y}$
59	58	oveq2d	$⊢ x = y \to c (\frac{\log x}{x}) = c (\frac{\log y}{y})$
60	55 59	breq12d	$⊢ x = y \to (\|seq 1 (+ F) (⌊x⌋) - t\| \leq c (\frac{\log x}{x}) \leftrightarrow \|seq 1 (+ F) (⌊y⌋) - t\| \leq c (\frac{\log y}{y}))$
61	60	cbvralvw	$⊢ \forall x \in [3, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c (\frac{\log x}{x}) \leftrightarrow \forall y \in [3, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq c (\frac{\log y}{y})$
62	61	anbi2i	$⊢ (seq 1 (+ F) ⇝ t \land \forall x \in [3, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c (\frac{\log x}{x})) \leftrightarrow (seq 1 (+ F) ⇝ t \land \forall y \in [3, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq c (\frac{\log y}{y}))$
63	62	rexbii	$⊢ \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [3, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c (\frac{\log x}{x})) \leftrightarrow \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall y \in [3, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq c (\frac{\log y}{y}))$
64	63	exbii	$⊢ \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [3, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c (\frac{\log x}{x})) \leftrightarrow \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall y \in [3, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq c (\frac{\log y}{y}))$
65	53 64	sylib	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall y \in [3, +∞) \|seq 1 (+ F) (⌊y⌋) - t\| \leq c (\frac{\log y}{y}))$

Metamath Proof Explorer

Theorem dchrvmasumlema

Proof