Metamath Proof Explorer

Theorem dchrvmasumif

Description: An asymptotic approximation for the sum of X ( n ) Lam ( n ) / n conditional on the value of the infinite sum S . (We will later show that the case S = 0 is impossible, and hence establish dchrvmasum .) (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 )
dchrvmasumif.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
dchrvmasumif.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
dchrvmasumif.s ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
dchrvmasumif.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
Assertion dchrvmasumif ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )

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 dchrvmasumif.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10 dchrvmasumif.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11 dchrvmasumif.s ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
12 dchrvmasumif.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
13 eqid ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) )
14 1 2 3 4 5 6 7 8 13 dchrvmasumlema ⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) )
15 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝑁 ∈ ℕ )
16 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝑋 ∈ 𝐷 )
17 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝑋 ≠ 1 )
18 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
19 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
20 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) )
22 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 )
23 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
24 1 2 15 4 5 6 16 17 9 18 19 20 13 21 22 23 dchrvmasumiflem2 ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )
25 24 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) )
26 25 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) )
27 14 26 mpd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )