Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisum0re Structured version   Visualization version   GIF version

Theorem dchrisum0re 25247
 Description: Suppose 𝑋 is a non-principal Dirichlet character with Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 = 0. Then 𝑋 is a real character. Part of Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a (𝜑𝑁 ∈ ℕ)
rpvmasum2.g 𝐺 = (DChr‘𝑁)
rpvmasum2.d 𝐷 = (Base‘𝐺)
rpvmasum2.1 1 = (0g𝐺)
rpvmasum2.w 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0}
dchrisum0.b (𝜑𝑋𝑊)
Assertion
Ref Expression
dchrisum0re (𝜑𝑋:(Base‘𝑍)⟶ℝ)
Distinct variable groups:   𝑦,𝑚, 1   𝑚,𝑁,𝑦   𝜑,𝑚   𝑚,𝑍,𝑦   𝐷,𝑚,𝑦   𝑚,𝐿,𝑦   𝑚,𝑋,𝑦
Allowed substitution hints:   𝜑(𝑦)   𝐺(𝑦,𝑚)   𝑊(𝑦,𝑚)

Proof of Theorem dchrisum0re
Dummy variables 𝑘 𝑛 𝑥 𝑓 𝑐 𝑡 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpvmasum2.g . . . 4 𝐺 = (DChr‘𝑁)
2 rpvmasum.z . . . 4 𝑍 = (ℤ/nℤ‘𝑁)
3 rpvmasum2.d . . . 4 𝐷 = (Base‘𝐺)
4 eqid 2651 . . . 4 (Base‘𝑍) = (Base‘𝑍)
5 rpvmasum2.w . . . . . . 7 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0}
6 ssrab2 3720 . . . . . . 7 {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 })
75, 6eqsstri 3668 . . . . . 6 𝑊 ⊆ (𝐷 ∖ { 1 })
8 dchrisum0.b . . . . . 6 (𝜑𝑋𝑊)
97, 8sseldi 3634 . . . . 5 (𝜑𝑋 ∈ (𝐷 ∖ { 1 }))
109eldifad 3619 . . . 4 (𝜑𝑋𝐷)
111, 2, 3, 4, 10dchrf 25012 . . 3 (𝜑𝑋:(Base‘𝑍)⟶ℂ)
1211ffnd 6084 . 2 (𝜑𝑋 Fn (Base‘𝑍))
1311ffvelrnda 6399 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑍)) → (𝑋𝑥) ∈ ℂ)
14 fvco3 6314 . . . . . 6 ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋𝑥)))
1511, 14sylan 487 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋𝑥)))
16 logno1 24427 . . . . . . . 8 ¬ (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1)
17 1red 10093 . . . . . . . . . . 11 ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → 1 ∈ ℝ)
18 rpvmasum.l . . . . . . . . . . . . 13 𝐿 = (ℤRHom‘𝑍)
19 rpvmasum.a . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
20 rpvmasum2.1 . . . . . . . . . . . . 13 1 = (0g𝐺)
21 eqid 2651 . . . . . . . . . . . . 13 (Unit‘𝑍) = (Unit‘𝑍)
2219nnnn0d 11389 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ0)
232zncrng 19941 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ0𝑍 ∈ CRing)
2422, 23syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑍 ∈ CRing)
25 crngring 18604 . . . . . . . . . . . . . . 15 (𝑍 ∈ CRing → 𝑍 ∈ Ring)
2624, 25syl 17 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ Ring)
27 eqid 2651 . . . . . . . . . . . . . . 15 (1r𝑍) = (1r𝑍)
2821, 271unit 18704 . . . . . . . . . . . . . 14 (𝑍 ∈ Ring → (1r𝑍) ∈ (Unit‘𝑍))
2926, 28syl 17 . . . . . . . . . . . . 13 (𝜑 → (1r𝑍) ∈ (Unit‘𝑍))
30 eqid 2651 . . . . . . . . . . . . 13 (𝐿 “ {(1r𝑍)}) = (𝐿 “ {(1r𝑍)})
31 eqidd 2652 . . . . . . . . . . . . 13 ((𝜑𝑓𝑊) → (1r𝑍) = (1r𝑍))
322, 18, 19, 1, 3, 20, 5, 21, 29, 30, 31rpvmasum2 25246 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) ∈ 𝑂(1))
3332adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) ∈ 𝑂(1))
3419phicld 15524 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ϕ‘𝑁) ∈ ℕ)
3534nnnn0d 11389 . . . . . . . . . . . . . . . . 17 (𝜑 → (ϕ‘𝑁) ∈ ℕ0)
3635adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℕ0)
3736nn0red 11390 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℝ)
38 fzfid 12812 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
39 inss1 3866 . . . . . . . . . . . . . . . . 17 ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) ⊆ (1...(⌊‘𝑥))
40 ssfi 8221 . . . . . . . . . . . . . . . . 17 (((1...(⌊‘𝑥)) ∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) ⊆ (1...(⌊‘𝑥))) → ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) ∈ Fin)
4138, 39, 40sylancl 695 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) ∈ Fin)
42 elinel1 3832 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) → 𝑛 ∈ (1...(⌊‘𝑥)))
43 elfznn 12408 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
4443adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
4542, 44sylan2 490 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 𝑛 ∈ ℕ)
46 vmacl 24889 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
47 nndivre 11094 . . . . . . . . . . . . . . . . . 18 (((Λ‘𝑛) ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
4846, 47mpancom 704 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
4945, 48syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
5041, 49fsumrecl 14509 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛) ∈ ℝ)
5137, 50remulcld 10108 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ)
52 relogcl 24367 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
5352adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
54 1re 10077 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
551, 3dchrfi 25025 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
5619, 55syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ Fin)
57 difss 3770 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∖ { 1 }) ⊆ 𝐷
587, 57sstri 3645 . . . . . . . . . . . . . . . . . . . 20 𝑊𝐷
59 ssfi 8221 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ Fin ∧ 𝑊𝐷) → 𝑊 ∈ Fin)
6056, 58, 59sylancl 695 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑊 ∈ Fin)
61 hashcl 13185 . . . . . . . . . . . . . . . . . . 19 (𝑊 ∈ Fin → (#‘𝑊) ∈ ℕ0)
6260, 61syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (#‘𝑊) ∈ ℕ0)
6362nn0red 11390 . . . . . . . . . . . . . . . . 17 (𝜑 → (#‘𝑊) ∈ ℝ)
64 resubcl 10383 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → (1 − (#‘𝑊)) ∈ ℝ)
6554, 63, 64sylancr 696 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − (#‘𝑊)) ∈ ℝ)
6665adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → (1 − (#‘𝑊)) ∈ ℝ)
6753, 66remulcld 10108 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · (1 − (#‘𝑊))) ∈ ℝ)
6851, 67resubcld 10496 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) ∈ ℝ)
6968recnd 10106 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) ∈ ℂ)
7069adantlr 751 . . . . . . . . . . 11 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) ∈ ℂ)
7152adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
7271recnd 10106 . . . . . . . . . . 11 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
7352ad2antrl 764 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
7467ad2ant2r 798 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (1 − (#‘𝑊))) ∈ ℝ)
7573, 74readdcld 10107 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) + ((log‘𝑥) · (1 − (#‘𝑊)))) ∈ ℝ)
76 0red 10079 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ)
7751ad2ant2r 798 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ)
78 2re 11128 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
7978a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 2 ∈ ℝ)
8063ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (#‘𝑊) ∈ ℝ)
8179, 80resubcld 10496 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (2 − (#‘𝑊)) ∈ ℝ)
82 log1 24377 . . . . . . . . . . . . . . . . 17 (log‘1) = 0
83 simprr 811 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
84 1rp 11874 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ+
85 simprl 809 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
86 logleb 24394 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ+𝑥 ∈ ℝ+) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
8784, 85, 86sylancr 696 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
8883, 87mpbid 222 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥))
8982, 88syl5eqbrr 4721 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥))
90 simplr 807 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (∗ ∘ 𝑋) ≠ 𝑋)
91 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (invg𝐺) = (invg𝐺)
921, 3, 10, 91dchrinv 25031 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((invg𝐺)‘𝑋) = (∗ ∘ 𝑋))
931dchrabl 25024 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
9419, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐺 ∈ Abel)
95 ablgrp 18244 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐺 ∈ Grp)
973, 91grpinvcl 17514 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ Grp ∧ 𝑋𝐷) → ((invg𝐺)‘𝑋) ∈ 𝐷)
9896, 10, 97syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((invg𝐺)‘𝑋) ∈ 𝐷)
9992, 98eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (∗ ∘ 𝑋) ∈ 𝐷)
100 eldifsni 4353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋1 )
1019, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑋1 )
1023, 20grpidcl 17497 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐺 ∈ Grp → 1𝐷)
10396, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑1𝐷)
1043, 91, 96, 10, 103grpinv11 17531 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((invg𝐺)‘𝑋) = ((invg𝐺)‘ 1 ) ↔ 𝑋 = 1 ))
105104necon3bid 2867 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((invg𝐺)‘𝑋) ≠ ((invg𝐺)‘ 1 ) ↔ 𝑋1 ))
106101, 105mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((invg𝐺)‘𝑋) ≠ ((invg𝐺)‘ 1 ))
10720, 91grpinvid 17523 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺 ∈ Grp → ((invg𝐺)‘ 1 ) = 1 )
10896, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((invg𝐺)‘ 1 ) = 1 )
109106, 92, 1083netr3d 2899 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (∗ ∘ 𝑋) ≠ 1 )
110 eldifsn 4350 . . . . . . . . . . . . . . . . . . . . . . 23 ((∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 }) ↔ ((∗ ∘ 𝑋) ∈ 𝐷 ∧ (∗ ∘ 𝑋) ≠ 1 ))
11199, 109, 110sylanbrc 699 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 }))
112 nnuz 11761 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
113 1zzd 11446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ∈ ℤ)
114 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑚 → (𝐿𝑛) = (𝐿𝑚))
115114fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑚 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑚)))
116 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑚𝑛 = 𝑚)
117115, 116oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑚 → ((𝑋‘(𝐿𝑛)) / 𝑛) = ((𝑋‘(𝐿𝑚)) / 𝑚))
118117fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)) = (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
119 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛))) = (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))
120 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) ∈ V
121118, 119, 120fvmpt 6321 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
122121adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
123 nnre 11065 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
124123adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
125124cjred 14010 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ ℕ) → (∗‘𝑚) = 𝑚)
126125oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ ℕ) → ((∗‘(𝑋‘(𝐿𝑚))) / (∗‘𝑚)) = ((∗‘(𝑋‘(𝐿𝑚))) / 𝑚))
12711adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑚 ∈ ℕ) → 𝑋:(Base‘𝑍)⟶ℂ)
1282, 4, 18znzrhfo 19944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℕ0𝐿:ℤ–onto→(Base‘𝑍))
12922, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐿:ℤ–onto→(Base‘𝑍))
130 fof 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
131129, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐿:ℤ⟶(Base‘𝑍))
132 nnz 11437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
133 ffvelrn 6397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑚 ∈ ℤ) → (𝐿𝑚) ∈ (Base‘𝑍))
134131, 132, 133syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑚 ∈ ℕ) → (𝐿𝑚) ∈ (Base‘𝑍))
135127, 134ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ ℕ) → (𝑋‘(𝐿𝑚)) ∈ ℂ)
136 nncn 11066 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
137136adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
138 nnne0 11091 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
139138adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ ℕ) → 𝑚 ≠ 0)
140135, 137, 139cjdivd 14007 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ ℕ) → (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) = ((∗‘(𝑋‘(𝐿𝑚))) / (∗‘𝑚)))
141 fvco3 6314 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑋:(Base‘𝑍)⟶ℂ ∧ (𝐿𝑚) ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘(𝐿𝑚)) = (∗‘(𝑋‘(𝐿𝑚))))
142127, 134, 141syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ ℕ) → ((∗ ∘ 𝑋)‘(𝐿𝑚)) = (∗‘(𝑋‘(𝐿𝑚))))
143142oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ ℕ) → (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) = ((∗‘(𝑋‘(𝐿𝑚))) / 𝑚))
144126, 140, 1433eqtr4d 2695 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ ℕ) → (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) = (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚))
145122, 144eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))‘𝑚) = (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚))
146135cjcld 13980 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ ℕ) → (∗‘(𝑋‘(𝐿𝑚))) ∈ ℂ)
147146, 137, 139divcld 10839 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ ℕ) → ((∗‘(𝑋‘(𝐿𝑚))) / 𝑚) ∈ ℂ)
148143, 147eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ ℕ) → (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) ∈ ℂ)
149 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))
1502, 18, 19, 1, 3, 20, 10, 101, 149dchrmusumlema 25227 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))
151 simprrl 821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡)
1528adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋𝑊)
15319adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ)
15410adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋𝐷)
155101adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋1 )
156 simprl 809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞))
157 simprrr 822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))
1582, 18, 153, 1, 3, 20, 154, 155, 149, 156, 151, 157, 5dchrvmaeq0 25238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑋𝑊𝑡 = 0))
159152, 158mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑡 = 0)
160151, 159breqtrd 4711 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 0)
161160rexlimdvaa 3061 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 0))
162161exlimdv 1901 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 0))
163150, 162mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 0)
164 seqex 12843 . . . . . . . . . . . . . . . . . . . . . . . . . 26 seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))) ∈ V
165164a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))) ∈ V)
166 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = 𝑚 → (𝐿𝑎) = (𝐿𝑚))
167166fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑚 → (𝑋‘(𝐿𝑎)) = (𝑋‘(𝐿𝑚)))
168 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑚𝑎 = 𝑚)
169167, 168oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑚 → ((𝑋‘(𝐿𝑎)) / 𝑎) = ((𝑋‘(𝐿𝑚)) / 𝑚))
170 ovex 6718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑋‘(𝐿𝑚)) / 𝑚) ∈ V
171169, 149, 170fvmpt 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 ∈ ℕ → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿𝑚)) / 𝑚))
172171adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑚 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿𝑚)) / 𝑚))
173135, 137, 139divcld 10839 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑚 ∈ ℕ) → ((𝑋‘(𝐿𝑚)) / 𝑚) ∈ ℂ)
174172, 173eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑚 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))‘𝑚) ∈ ℂ)
175112, 113, 174serf 12869 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))):ℕ⟶ℂ)
176175ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ) → (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘𝑘) ∈ ℂ)
177 fzfid 12812 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
178 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘 ∈ ℕ) → 𝜑)
179 elfznn 12408 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ)
180178, 179, 173syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑋‘(𝐿𝑚)) / 𝑚) ∈ ℂ)
181177, 180fsumcj 14586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → (∗‘Σ𝑚 ∈ (1...𝑘)((𝑋‘(𝐿𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...𝑘)(∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
182178, 179, 172syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿𝑚)) / 𝑚))
183 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
184183, 112syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
185182, 184, 180fsumser 14505 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((𝑋‘(𝐿𝑚)) / 𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘𝑘))
186185fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → (∗‘Σ𝑚 ∈ (1...𝑘)((𝑋‘(𝐿𝑚)) / 𝑚)) = (∗‘(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘𝑘)))
187178, 179, 122syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
188173cjcld 13980 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑚 ∈ ℕ) → (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) ∈ ℂ)
189178, 179, 188syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) ∈ ℂ)
190187, 184, 189fsumser 14505 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) = (seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛))))‘𝑘))
191181, 186, 1903eqtr3rd 2694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ) → (seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛))))‘𝑘) = (∗‘(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘𝑘)))
192112, 163, 165, 113, 176, 191climcj 14379 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))) ⇝ (∗‘0))
193 cj0 13942 . . . . . . . . . . . . . . . . . . . . . . . 24 (∗‘0) = 0
194192, 193syl6breq 4726 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))) ⇝ 0)
195112, 113, 145, 148, 194isumclim 14532 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) = 0)
196 fveq1 6228 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = (∗ ∘ 𝑋) → (𝑦‘(𝐿𝑚)) = ((∗ ∘ 𝑋)‘(𝐿𝑚)))
197196oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (∗ ∘ 𝑋) → ((𝑦‘(𝐿𝑚)) / 𝑚) = (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚))
198197sumeq2sdv 14479 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (∗ ∘ 𝑋) → Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚))
199198eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (∗ ∘ 𝑋) → (Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0 ↔ Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) = 0))
200199, 5elrab2 3399 . . . . . . . . . . . . . . . . . . . . . 22 ((∗ ∘ 𝑋) ∈ 𝑊 ↔ ((∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 }) ∧ Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) = 0))
201111, 195, 200sylanbrc 699 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (∗ ∘ 𝑋) ∈ 𝑊)
202201ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (∗ ∘ 𝑋) ∈ 𝑊)
2038ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑋𝑊)
204 hashprg 13220 . . . . . . . . . . . . . . . . . . . 20 (((∗ ∘ 𝑋) ∈ 𝑊𝑋𝑊) → ((∗ ∘ 𝑋) ≠ 𝑋 ↔ (#‘{(∗ ∘ 𝑋), 𝑋}) = 2))
205202, 203, 204syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((∗ ∘ 𝑋) ≠ 𝑋 ↔ (#‘{(∗ ∘ 𝑋), 𝑋}) = 2))
20690, 205mpbid 222 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (#‘{(∗ ∘ 𝑋), 𝑋}) = 2)
20760ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑊 ∈ Fin)
208202, 203prssd 4386 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {(∗ ∘ 𝑋), 𝑋} ⊆ 𝑊)
209 ssdomg 8043 . . . . . . . . . . . . . . . . . . . 20 (𝑊 ∈ Fin → ({(∗ ∘ 𝑋), 𝑋} ⊆ 𝑊 → {(∗ ∘ 𝑋), 𝑋} ≼ 𝑊))
210207, 208, 209sylc 65 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {(∗ ∘ 𝑋), 𝑋} ≼ 𝑊)
211 hashdomi 13207 . . . . . . . . . . . . . . . . . . 19 ({(∗ ∘ 𝑋), 𝑋} ≼ 𝑊 → (#‘{(∗ ∘ 𝑋), 𝑋}) ≤ (#‘𝑊))
212210, 211syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (#‘{(∗ ∘ 𝑋), 𝑋}) ≤ (#‘𝑊))
213206, 212eqbrtrrd 4709 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 2 ≤ (#‘𝑊))
214 suble0 10580 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((2 − (#‘𝑊)) ≤ 0 ↔ 2 ≤ (#‘𝑊)))
21578, 80, 214sylancr 696 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 − (#‘𝑊)) ≤ 0 ↔ 2 ≤ (#‘𝑊)))
216213, 215mpbird 247 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (2 − (#‘𝑊)) ≤ 0)
21781, 76, 73, 89, 216lemul2ad 11002 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (2 − (#‘𝑊))) ≤ ((log‘𝑥) · 0))
218 df-2 11117 . . . . . . . . . . . . . . . . . . 19 2 = (1 + 1)
219218oveq1i 6700 . . . . . . . . . . . . . . . . . 18 (2 − (#‘𝑊)) = ((1 + 1) − (#‘𝑊))
220 1cnd 10094 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ)
22180recnd 10106 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (#‘𝑊) ∈ ℂ)
222220, 220, 221addsubassd 10450 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((1 + 1) − (#‘𝑊)) = (1 + (1 − (#‘𝑊))))
223219, 222syl5eq 2697 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (2 − (#‘𝑊)) = (1 + (1 − (#‘𝑊))))
224223oveq2d 6706 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (2 − (#‘𝑊))) = ((log‘𝑥) · (1 + (1 − (#‘𝑊)))))
22572adantrr 753 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ)
22665ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 − (#‘𝑊)) ∈ ℝ)
227226recnd 10106 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 − (#‘𝑊)) ∈ ℂ)
228225, 220, 227adddid 10102 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (1 + (1 − (#‘𝑊)))) = (((log‘𝑥) · 1) + ((log‘𝑥) · (1 − (#‘𝑊)))))
229225mulid1d 10095 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · 1) = (log‘𝑥))
230229oveq1d 6705 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥) · 1) + ((log‘𝑥) · (1 − (#‘𝑊)))) = ((log‘𝑥) + ((log‘𝑥) · (1 − (#‘𝑊)))))
231224, 228, 2303eqtrd 2689 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (2 − (#‘𝑊))) = ((log‘𝑥) + ((log‘𝑥) · (1 − (#‘𝑊)))))
232225mul01d 10273 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · 0) = 0)
233217, 231, 2323brtr3d 4716 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) + ((log‘𝑥) · (1 − (#‘𝑊)))) ≤ 0)
23434nnred 11073 . . . . . . . . . . . . . . . 16 (𝜑 → (ϕ‘𝑁) ∈ ℝ)
235234ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ϕ‘𝑁) ∈ ℝ)
23650ad2ant2r 798 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛) ∈ ℝ)
23735ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ϕ‘𝑁) ∈ ℕ0)
238237nn0ge0d 11392 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (ϕ‘𝑁))
23945, 46syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → (Λ‘𝑛) ∈ ℝ)
240 vmage0 24892 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
24145, 240syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 0 ≤ (Λ‘𝑛))
24245nnred 11073 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 𝑛 ∈ ℝ)
24345nngt0d 11102 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 0 < 𝑛)
244 divge0 10930 . . . . . . . . . . . . . . . . . 18 ((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤ (Λ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤ ((Λ‘𝑛) / 𝑛))
245239, 241, 242, 243, 244syl22anc 1367 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
24641, 49, 245fsumge0 14571 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → 0 ≤ Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛))
247246ad2ant2r 798 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛))
248235, 236, 238, 247mulge0d 10642 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)))
24975, 76, 77, 233, 248letrd 10232 . . . . . . . . . . . . 13 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) + ((log‘𝑥) · (1 − (#‘𝑊)))) ≤ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)))
250 leaddsub 10542 . . . . . . . . . . . . . 14 (((log‘𝑥) ∈ ℝ ∧ ((log‘𝑥) · (1 − (#‘𝑊))) ∈ ℝ ∧ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ) → (((log‘𝑥) + ((log‘𝑥) · (1 − (#‘𝑊)))) ≤ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ↔ (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))))
25173, 74, 77, 250syl3anc 1366 . . . . . . . . . . . . 13 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥) + ((log‘𝑥) · (1 − (#‘𝑊)))) ≤ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ↔ (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))))
252249, 251mpbid 222 . . . . . . . . . . . 12 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))))
25373, 89absidd 14205 . . . . . . . . . . . 12 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(log‘𝑥)) = (log‘𝑥))
25468ad2ant2r 798 . . . . . . . . . . . . 13 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) ∈ ℝ)
25576, 73, 254, 89, 252letrd 10232 . . . . . . . . . . . . 13 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))))
256254, 255absidd 14205 . . . . . . . . . . . 12 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) = (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))))
257252, 253, 2563brtr4d 4717 . . . . . . . . . . 11 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(log‘𝑥)) ≤ (abs‘(((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))))
25817, 33, 70, 72, 257o1le 14427 . . . . . . . . . 10 ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1))
259258ex 449 . . . . . . . . 9 (𝜑 → ((∗ ∘ 𝑋) ≠ 𝑋 → (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1)))
260259necon1bd 2841 . . . . . . . 8 (𝜑 → (¬ (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1) → (∗ ∘ 𝑋) = 𝑋))
26116, 260mpi 20 . . . . . . 7 (𝜑 → (∗ ∘ 𝑋) = 𝑋)
262261adantr 480 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑍)) → (∗ ∘ 𝑋) = 𝑋)
263262fveq1d 6231 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (𝑋𝑥))
26415, 263eqtr3d 2687 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑍)) → (∗‘(𝑋𝑥)) = (𝑋𝑥))
26513, 264cjrebd 13986 . . 3 ((𝜑𝑥 ∈ (Base‘𝑍)) → (𝑋𝑥) ∈ ℝ)
266265ralrimiva 2995 . 2 (𝜑 → ∀𝑥 ∈ (Base‘𝑍)(𝑋𝑥) ∈ ℝ)
267 ffnfv 6428 . 2 (𝑋:(Base‘𝑍)⟶ℝ ↔ (𝑋 Fn (Base‘𝑍) ∧ ∀𝑥 ∈ (Base‘𝑍)(𝑋𝑥) ∈ ℝ))
26812, 266, 267sylanbrc 699 1 (𝜑𝑋:(Base‘𝑍)⟶ℝ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  ∃wex 1744   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∩ cin 3606   ⊆ wss 3607  {csn 4210  {cpr 4212   class class class wbr 4685   ↦ cmpt 4762  ◡ccnv 5142   “ cima 5146   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924  ‘cfv 5926  (class class class)co 6690   ≼ cdom 7995  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  2c2 11108  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ℝ+crp 11870  [,)cico 12215  ...cfz 12364  ⌊cfl 12631  seqcseq 12841  #chash 13157  ∗ccj 13880  abscabs 14018   ⇝ cli 14259  𝑂(1)co1 14261  Σcsu 14460  ϕcphi 15516  Basecbs 15904  0gc0g 16147  Grpcgrp 17469  invgcminusg 17470  Abelcabl 18240  1rcur 18547  Ringcrg 18593  CRingccrg 18594  Unitcui 18685  ℤRHomczrh 19896  ℤ/nℤczn 19899  logclog 24346  Λcvma 24863  DChrcdchr 25002 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-rpss 6979  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-tpos 7397  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-omul 7610  df-er 7787  df-ec 7789  df-qs 7793  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-acn 8806  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-xnn0 11402  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-word 13331  df-concat 13333  df-s1 13334  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-o1 14265  df-lo1 14266  df-sum 14461  df-ef 14842  df-e 14843  df-sin 14844  df-cos 14845  df-pi 14847  df-dvds 15028  df-gcd 15264  df-prm 15433  df-phi 15518  df-pc 15589  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-qus 16216  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-mhm 17382  df-submnd 17383  df-grp 17472  df-minusg 17473  df-sbg 17474  df-mulg 17588  df-subg 17638  df-nsg 17639  df-eqg 17640  df-ghm 17705  df-gim 17748  df-ga 17769  df-cntz 17796  df-oppg 17822  df-od 17994  df-gex 17995  df-pgp 17996  df-lsm 18097  df-pj1 18098  df-cmn 18241  df-abl 18242  df-cyg 18326  df-dprd 18440  df-dpj 18441  df-mgp 18536  df-ur 18548  df-ring 18595  df-cring 18596  df-oppr 18669  df-dvdsr 18687  df-unit 18688  df-invr 18718  df-dvr 18729  df-rnghom 18763  df-drng 18797  df-subrg 18826  df-lmod 18913  df-lss 18981  df-lsp 19020  df-sra 19220  df-rgmod 19221  df-lidl 19222  df-rsp 19223  df-2idl 19280  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-zring 19867  df-zrh 19900  df-zn 19903  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-0p 23482  df-limc 23675  df-dv 23676  df-ply 23989  df-idp 23990  df-coe 23991  df-dgr 23992  df-quot 24091  df-log 24348  df-cxp 24349  df-em 24764  df-cht 24868  df-vma 24869  df-chp 24870  df-ppi 24871  df-mu 24872  df-dchr 25003 This theorem is referenced by:  dchrisum0  25254
 Copyright terms: Public domain W3C validator