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 ⊢Z=ℤ/Nℤ
rpvmasum.l ⊢L=ℤRHom⁡Z
rpvmasum.a ⊢φ→N∈ℕ
rpvmasum.g ⊢G=DChr⁡N
rpvmasum.d ⊢D=BaseG
rpvmasum.1 ⊢1˙=0G
dchrisum.b ⊢φ→X∈D
dchrisum.n1 ⊢φ→X≠1˙
dchrvmasumif.f ⊢F=a∈ℕ⟼X⁡L⁡aa
dchrvmasumif.c ⊢φ→C∈0+∞
dchrvmasumif.s ⊢φ→seq1+F⇝S
dchrvmasumif.1 ⊢φ→∀y∈1+∞seq1+F⁡y−S≤Cy
Assertion dchrvmasumif ⊢φ→x∈ℝ+⟼∑n=1xX⁡L⁡n⁢Λ⁡nn+ifS=0log⁡x0∈𝑂⁡1

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢Z=ℤ/Nℤ
2 rpvmasum.l ⊢L=ℤRHom⁡Z
3 rpvmasum.a ⊢φ→N∈ℕ
4 rpvmasum.g ⊢G=DChr⁡N
5 rpvmasum.d ⊢D=BaseG
6 rpvmasum.1 ⊢1˙=0G
7 dchrisum.b ⊢φ→X∈D
8 dchrisum.n1 ⊢φ→X≠1˙
9 dchrvmasumif.f ⊢F=a∈ℕ⟼X⁡L⁡aa
10 dchrvmasumif.c ⊢φ→C∈0+∞
11 dchrvmasumif.s ⊢φ→seq1+F⇝S
12 dchrvmasumif.1 ⊢φ→∀y∈1+∞seq1+F⁡y−S≤Cy
13 eqid ⊢a∈ℕ⟼X⁡L⁡a⁢log⁡aa=a∈ℕ⟼X⁡L⁡a⁢log⁡aa
14 1 2 3 4 5 6 7 8 13 dchrvmasumlema ⊢φ→∃t∃c∈0+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy
15 3 adantr ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→N∈ℕ
16 7 adantr ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→X∈D
17 8 adantr ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→X≠1˙
18 10 adantr ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→C∈0+∞
19 11 adantr ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→seq1+F⇝S
20 12 adantr ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→∀y∈1+∞seq1+F⁡y−S≤Cy
21 simprl ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→c∈0+∞
22 simprrl ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t
23 simprrr ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy
24 1 2 15 4 5 6 16 17 9 18 19 20 13 21 22 23 dchrvmasumiflem2 ⊢φ∧c∈0+∞∧seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→x∈ℝ+⟼∑n=1xX⁡L⁡n⁢Λ⁡nn+ifS=0log⁡x0∈𝑂⁡1
25 24 rexlimdvaa ⊢φ→∃c∈0+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→x∈ℝ+⟼∑n=1xX⁡L⁡n⁢Λ⁡nn+ifS=0log⁡x0∈𝑂⁡1
26 25 exlimdv ⊢φ→∃t∃c∈0+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⇝t∧∀y∈3+∞seq1+a∈ℕ⟼X⁡L⁡a⁢log⁡aa⁡y−t≤c⁢log⁡yy→x∈ℝ+⟼∑n=1xX⁡L⁡n⁢Λ⁡nn+ifS=0log⁡x0∈𝑂⁡1
27 14 26 mpd ⊢φ→x∈ℝ+⟼∑n=1xX⁡L⁡n⁢Λ⁡nn+ifS=0log⁡x0∈𝑂⁡1