This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑦 ) / 𝑦 ) ) ) )