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 = Base G
rpvmasum.1 ⊢ 1 ˙ = 0 G
dchrisum.b ⊢ φ → X ∈ D
dchrisum.n1 ⊢ φ → X ≠ 1 ˙
dchrvmasumif.f ⊢ F = a ∈ ℕ ⟼ X ⁡ L ⁡ a a
dchrvmasumif.c ⊢ φ → C ∈ 0 +∞
dchrvmasumif.s ⊢ φ → seq 1 + F ⇝ S
dchrvmasumif.1 ⊢ φ → ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − S ≤ C y
Assertion dchrvmasumif ⊢ φ → x ∈ ℝ + ⟼ ∑ n = 1 x X ⁡ L ⁡ n ⁢ Λ ⁡ n n + if S = 0 log ⁡ x 0 ∈ 𝑂⁡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 = Base G
6 rpvmasum.1 ⊢ 1 ˙ = 0 G
7 dchrisum.b ⊢ φ → X ∈ D
8 dchrisum.n1 ⊢ φ → X ≠ 1 ˙
9 dchrvmasumif.f ⊢ F = a ∈ ℕ ⟼ X ⁡ L ⁡ a a
10 dchrvmasumif.c ⊢ φ → C ∈ 0 +∞
11 dchrvmasumif.s ⊢ φ → seq 1 + F ⇝ S
12 dchrvmasumif.1 ⊢ φ → ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − S ≤ C y
13 eqid ⊢ a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a = a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a
14 1 2 3 4 5 6 7 8 13 dchrvmasumlema ⊢ φ → ∃ t ∃ c ∈ 0 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y
15 3 adantr ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → N ∈ ℕ
16 7 adantr ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → X ∈ D
17 8 adantr ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → X ≠ 1 ˙
18 10 adantr ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → C ∈ 0 +∞
19 11 adantr ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → seq 1 + F ⇝ S
20 12 adantr ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − S ≤ C y
21 simprl ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → c ∈ 0 +∞
22 simprrl ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t
23 simprrr ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y
24 1 2 15 4 5 6 16 17 9 18 19 20 13 21 22 23 dchrvmasumiflem2 ⊢ φ ∧ c ∈ 0 +∞ ∧ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → x ∈ ℝ + ⟼ ∑ n = 1 x X ⁡ L ⁡ n ⁢ Λ ⁡ n n + if S = 0 log ⁡ x 0 ∈ 𝑂⁡1
25 24 rexlimdvaa ⊢ φ → ∃ c ∈ 0 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → x ∈ ℝ + ⟼ ∑ n = 1 x X ⁡ L ⁡ n ⁢ Λ ⁡ n n + if S = 0 log ⁡ x 0 ∈ 𝑂⁡1
26 25 exlimdv ⊢ φ → ∃ t ∃ c ∈ 0 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⇝ t ∧ ∀ y ∈ 3 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ log ⁡ a a ⁡ y − t ≤ c ⁢ log ⁡ y y → x ∈ ℝ + ⟼ ∑ n = 1 x X ⁡ L ⁡ n ⁢ Λ ⁡ n n + if S = 0 log ⁡ x 0 ∈ 𝑂⁡1
27 14 26 mpd ⊢ φ → x ∈ ℝ + ⟼ ∑ n = 1 x X ⁡ L ⁡ n ⁢ Λ ⁡ n n + if S = 0 log ⁡ x 0 ∈ 𝑂⁡1