Theorem 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	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrvmasumlema.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) )
Assertion	dchrvmasumlema	⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrvmasumlema.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) )
10		fveq2	⊢ ( 𝑛 = 𝑥 → ( log ‘ 𝑛 ) = ( log ‘ 𝑥 ) )
11		id	⊢ ( 𝑛 = 𝑥 → 𝑛 = 𝑥 )
12	10 11	oveq12d	⊢ ( 𝑛 = 𝑥 → ( ( log ‘ 𝑛 ) / 𝑛 ) = ( ( log ‘ 𝑥 ) / 𝑥 ) )
13		3nn	⊢ 3 ∈ ℕ
14	13	a1i	⊢ ( 𝜑 → 3 ∈ ℕ )
15		relogcl	⊢ ( 𝑛 ∈ ℝ+ → ( log ‘ 𝑛 ) ∈ ℝ )
16		rerpdivcl	⊢ ( ( ( log ‘ 𝑛 ) ∈ ℝ ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
17	15 16	mpancom	⊢ ( 𝑛 ∈ ℝ+ → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
19		simp3r	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ≤ 𝑥 )
20		simp2l	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
21	20	rpred	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℝ )
22		ere	⊢ e ∈ ℝ
23	22	a1i	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → e ∈ ℝ )
24		3re	⊢ 3 ∈ ℝ
25	24	a1i	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 3 ∈ ℝ )
26		egt2lt3	⊢ ( 2 < e ∧ e < 3 )
27	26	simpri	⊢ e < 3
28	22 24 27	ltleii	⊢ e ≤ 3
29	28	a1i	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → e ≤ 3 )
30		simp3l	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 3 ≤ 𝑛 )
31	23 25 21 29 30	letrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → e ≤ 𝑛 )
32		simp2r	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
33	32	rpred	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
34	23 21 33 31 19	letrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → e ≤ 𝑥 )
35		logdivle	⊢ ( ( ( 𝑛 ∈ ℝ ∧ e ≤ 𝑛 ) ∧ ( 𝑥 ∈ ℝ ∧ e ≤ 𝑥 ) ) → ( 𝑛 ≤ 𝑥 ↔ ( ( log ‘ 𝑥 ) / 𝑥 ) ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
36	21 31 33 34 35	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑛 ≤ 𝑥 ↔ ( ( log ‘ 𝑥 ) / 𝑥 ) ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
37	19 36	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 3 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) / 𝑥 ) ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) )
38		rpcn	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℂ )
39	38	cxp1d	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ↑𝑐 1 ) = 𝑛 )
40	39	oveq2d	⊢ ( 𝑛 ∈ ℝ+ → ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 1 ) ) = ( ( log ‘ 𝑛 ) / 𝑛 ) )
41	40	mpteq2ia	⊢ ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 1 ) ) ) = ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / 𝑛 ) )
42		1rp	⊢ 1 ∈ ℝ+
43		cxploglim	⊢ ( 1 ∈ ℝ+ → ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 1 ) ) ) ⇝𝑟 0 )
44	42 43	mp1i	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 1 ) ) ) ⇝𝑟 0 )
45	41 44	eqbrtrrid	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / 𝑛 ) ) ⇝𝑟 0 )
46		2fveq3	⊢ ( 𝑎 = 𝑛 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
47		fveq2	⊢ ( 𝑎 = 𝑛 → ( log ‘ 𝑎 ) = ( log ‘ 𝑛 ) )
48		id	⊢ ( 𝑎 = 𝑛 → 𝑎 = 𝑛 )
49	47 48	oveq12d	⊢ ( 𝑎 = 𝑛 → ( ( log ‘ 𝑎 ) / 𝑎 ) = ( ( log ‘ 𝑛 ) / 𝑛 ) )
50	46 49	oveq12d	⊢ ( 𝑎 = 𝑛 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
51	50	cbvmptv	⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
52	9 51	eqtri	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
53	1 2 3 4 5 6 7 8 12 14 18 37 45 52	dchrisum	⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑥 ) / 𝑥 ) ) ) )
54		2fveq3	⊢ ( 𝑥 = 𝑦 → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) )
55	54	fvoveq1d	⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) )
56		fveq2	⊢ ( 𝑥 = 𝑦 → ( log ‘ 𝑥 ) = ( log ‘ 𝑦 ) )
57		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
58	56 57	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( log ‘ 𝑥 ) / 𝑥 ) = ( ( log ‘ 𝑦 ) / 𝑦 ) )
59	58	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑐 · ( ( log ‘ 𝑥 ) / 𝑥 ) ) = ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
60	55 59	breq12d	⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑥 ) / 𝑥 ) ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) )
61	60	cbvralvw	⊢ ( ∀ 𝑥 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑥 ) / 𝑥 ) ) ↔ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
62	61	anbi2i	⊢ ( ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑥 ) / 𝑥 ) ) ) ↔ ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) )
63	62	rexbii	⊢ ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑥 ) / 𝑥 ) ) ) ↔ ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) )
64	63	exbii	⊢ ( ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑥 ) / 𝑥 ) ) ) ↔ ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) )
65	53 64	sylib	⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) )