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