Step |
Hyp |
Ref |
Expression |
1 |
|
rpvmasum.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
2 |
|
rpvmasum.l |
⊢ 𝐿 = ( ℤRHom ‘ 𝑍 ) |
3 |
|
rpvmasum.a |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
4 |
|
rpvmasum.u |
⊢ 𝑈 = ( Unit ‘ 𝑍 ) |
5 |
|
rpvmasum.b |
⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) |
6 |
|
rpvmasum.t |
⊢ 𝑇 = ( ◡ 𝐿 “ { 𝐴 } ) |
7 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) → 𝑁 ∈ ℕ ) |
8 |
|
eqid |
⊢ ( DChr ‘ 𝑁 ) = ( DChr ‘ 𝑁 ) |
9 |
|
eqid |
⊢ ( Base ‘ ( DChr ‘ 𝑁 ) ) = ( Base ‘ ( DChr ‘ 𝑁 ) ) |
10 |
|
eqid |
⊢ ( 0g ‘ ( DChr ‘ 𝑁 ) ) = ( 0g ‘ ( DChr ‘ 𝑁 ) ) |
11 |
|
2fveq3 |
⊢ ( 𝑚 = 𝑛 → ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) = ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) ) |
12 |
|
id |
⊢ ( 𝑚 = 𝑛 → 𝑚 = 𝑛 ) |
13 |
11 12
|
oveq12d |
⊢ ( 𝑚 = 𝑛 → ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) |
14 |
13
|
cbvsumv |
⊢ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = Σ 𝑛 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) |
15 |
14
|
eqeq1i |
⊢ ( Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ↔ Σ 𝑛 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = 0 ) |
16 |
15
|
rabbii |
⊢ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } = { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑛 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = 0 } |
17 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) → 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) |
18 |
1 2 7 8 9 10 16 17
|
dchrisum0 |
⊢ ¬ ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) |
19 |
18
|
imnani |
⊢ ( 𝜑 → ¬ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) |
20 |
19
|
eq0rdv |
⊢ ( 𝜑 → { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } = ∅ ) |
21 |
20
|
fveq2d |
⊢ ( 𝜑 → ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) = ( ♯ ‘ ∅ ) ) |
22 |
|
hash0 |
⊢ ( ♯ ‘ ∅ ) = 0 |
23 |
21 22
|
eqtrdi |
⊢ ( 𝜑 → ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) = 0 ) |
24 |
23
|
oveq2d |
⊢ ( 𝜑 → ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) = ( 1 − 0 ) ) |
25 |
|
1m0e1 |
⊢ ( 1 − 0 ) = 1 |
26 |
24 25
|
eqtrdi |
⊢ ( 𝜑 → ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) = 1 ) |
27 |
26
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) = 1 ) |
28 |
27
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) = ( ( log ‘ 𝑥 ) · 1 ) ) |
29 |
|
relogcl |
⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ ) |
30 |
29
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
31 |
30
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
32 |
31
|
mulid1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · 1 ) = ( log ‘ 𝑥 ) ) |
33 |
28 32
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) = ( log ‘ 𝑥 ) ) |
34 |
33
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) ) = ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) |
35 |
34
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ) |
36 |
|
eqid |
⊢ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } = { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } |
37 |
18
|
pm2.21i |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) → 𝐴 = ( 1r ‘ 𝑍 ) ) |
38 |
1 2 3 8 9 10 36 4 5 6 37
|
rpvmasum2 |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) ) ) ∈ 𝑂(1) ) |
39 |
35 38
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |