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

Theorem dchrisum0re 26196
 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 2758 . . . 4 (Base‘𝑍) = (Base‘𝑍)
5 rpvmasum2.w . . . . . . 7 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0}
65ssrab3 3986 . . . . . 6 𝑊 ⊆ (𝐷 ∖ { 1 })
7 dchrisum0.b . . . . . 6 (𝜑𝑋𝑊)
86, 7sseldi 3890 . . . . 5 (𝜑𝑋 ∈ (𝐷 ∖ { 1 }))
98eldifad 3870 . . . 4 (𝜑𝑋𝐷)
101, 2, 3, 4, 9dchrf 25925 . . 3 (𝜑𝑋:(Base‘𝑍)⟶ℂ)
1110ffnd 6499 . 2 (𝜑𝑋 Fn (Base‘𝑍))
1210ffvelrnda 6842 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑍)) → (𝑋𝑥) ∈ ℂ)
13 fvco3 6751 . . . . . 6 ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋𝑥)))
1410, 13sylan 583 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋𝑥)))
15 logno1 25326 . . . . . . . 8 ¬ (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1)
16 1red 10680 . . . . . . . . . . 11 ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → 1 ∈ ℝ)
17 rpvmasum.l . . . . . . . . . . . . 13 𝐿 = (ℤRHom‘𝑍)
18 rpvmasum.a . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
19 rpvmasum2.1 . . . . . . . . . . . . 13 1 = (0g𝐺)
20 eqid 2758 . . . . . . . . . . . . 13 (Unit‘𝑍) = (Unit‘𝑍)
2118nnnn0d 11994 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ0)
222zncrng 20312 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ0𝑍 ∈ CRing)
2321, 22syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑍 ∈ CRing)
24 crngring 19377 . . . . . . . . . . . . . . 15 (𝑍 ∈ CRing → 𝑍 ∈ Ring)
2523, 24syl 17 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ Ring)
26 eqid 2758 . . . . . . . . . . . . . . 15 (1r𝑍) = (1r𝑍)
2720, 261unit 19479 . . . . . . . . . . . . . 14 (𝑍 ∈ Ring → (1r𝑍) ∈ (Unit‘𝑍))
2825, 27syl 17 . . . . . . . . . . . . 13 (𝜑 → (1r𝑍) ∈ (Unit‘𝑍))
29 eqid 2758 . . . . . . . . . . . . 13 (𝐿 “ {(1r𝑍)}) = (𝐿 “ {(1r𝑍)})
30 eqidd 2759 . . . . . . . . . . . . 13 ((𝜑𝑓𝑊) → (1r𝑍) = (1r𝑍))
312, 17, 18, 1, 3, 19, 5, 20, 28, 29, 30rpvmasum2 26195 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈ 𝑂(1))
3231adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈ 𝑂(1))
3318phicld 16164 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ϕ‘𝑁) ∈ ℕ)
3433nnnn0d 11994 . . . . . . . . . . . . . . . . 17 (𝜑 → (ϕ‘𝑁) ∈ ℕ0)
3534adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℕ0)
3635nn0red 11995 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℝ)
37 fzfid 13390 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
38 inss1 4133 . . . . . . . . . . . . . . . . 17 ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) ⊆ (1...(⌊‘𝑥))
39 ssfi 8742 . . . . . . . . . . . . . . . . 17 (((1...(⌊‘𝑥)) ∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) ⊆ (1...(⌊‘𝑥))) → ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) ∈ Fin)
4037, 38, 39sylancl 589 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) ∈ Fin)
41 elinel1 4100 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)})) → 𝑛 ∈ (1...(⌊‘𝑥)))
42 elfznn 12985 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
4342adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
4441, 43sylan2 595 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 𝑛 ∈ ℕ)
45 vmacl 25802 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
46 nndivre 11715 . . . . . . . . . . . . . . . . . 18 (((Λ‘𝑛) ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
4745, 46mpancom 687 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
4844, 47syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
4940, 48fsumrecl 15139 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛) ∈ ℝ)
5036, 49remulcld 10709 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ)
51 relogcl 25266 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
5251adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
53 1re 10679 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
541, 3dchrfi 25938 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
5518, 54syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ Fin)
56 difss 4037 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∖ { 1 }) ⊆ 𝐷
576, 56sstri 3901 . . . . . . . . . . . . . . . . . . . 20 𝑊𝐷
58 ssfi 8742 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ Fin ∧ 𝑊𝐷) → 𝑊 ∈ Fin)
5955, 57, 58sylancl 589 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑊 ∈ Fin)
60 hashcl 13767 . . . . . . . . . . . . . . . . . . 19 (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ0)
6159, 60syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘𝑊) ∈ ℕ0)
6261nn0red 11995 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘𝑊) ∈ ℝ)
63 resubcl 10988 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → (1 − (♯‘𝑊)) ∈ ℝ)
6453, 62, 63sylancr 590 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − (♯‘𝑊)) ∈ ℝ)
6564adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → (1 − (♯‘𝑊)) ∈ ℝ)
6652, 65remulcld 10709 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · (1 − (♯‘𝑊))) ∈ ℝ)
6750, 66resubcld 11106 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))) ∈ ℝ)
6867recnd 10707 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))) ∈ ℂ)
6968adantlr 714 . . . . . . . . . . 11 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))) ∈ ℂ)
7051adantl 485 . . . . . . . . . . . 12 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
7170recnd 10707 . . . . . . . . . . 11 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
7251ad2antrl 727 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
7366ad2ant2r 746 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (1 − (♯‘𝑊))) ∈ ℝ)
7472, 73readdcld 10708 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) + ((log‘𝑥) · (1 − (♯‘𝑊)))) ∈ ℝ)
75 0red 10682 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ)
7650ad2ant2r 746 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ)
77 2re 11748 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
7877a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 2 ∈ ℝ)
7962ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (♯‘𝑊) ∈ ℝ)
8078, 79resubcld 11106 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (2 − (♯‘𝑊)) ∈ ℝ)
81 log1 25276 . . . . . . . . . . . . . . . . 17 (log‘1) = 0
82 simprr 772 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
83 1rp 12434 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ+
84 simprl 770 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
85 logleb 25293 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ+𝑥 ∈ ℝ+) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
8683, 84, 85sylancr 590 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
8782, 86mpbid 235 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥))
8881, 87eqbrtrrid 5068 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥))
8959ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑊 ∈ Fin)
90 eqid 2758 . . . . . . . . . . . . . . . . . . . . . . 23 (invg𝐺) = (invg𝐺)
911, 3, 9, 90dchrinv 25944 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((invg𝐺)‘𝑋) = (∗ ∘ 𝑋))
921dchrabl 25937 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
9318, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 ∈ Abel)
94 ablgrp 18978 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
9593, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐺 ∈ Grp)
963, 90grpinvcl 18218 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ Grp ∧ 𝑋𝐷) → ((invg𝐺)‘𝑋) ∈ 𝐷)
9795, 9, 96syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((invg𝐺)‘𝑋) ∈ 𝐷)
9891, 97eqeltrrd 2853 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (∗ ∘ 𝑋) ∈ 𝐷)
99 eldifsni 4680 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋1 )
1008, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋1 )
1013, 19grpidcl 18198 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ Grp → 1𝐷)
10295, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑1𝐷)
1033, 90, 95, 9, 102grpinv11 18235 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((invg𝐺)‘𝑋) = ((invg𝐺)‘ 1 ) ↔ 𝑋 = 1 ))
104103necon3bid 2995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((invg𝐺)‘𝑋) ≠ ((invg𝐺)‘ 1 ) ↔ 𝑋1 ))
105100, 104mpbird 260 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((invg𝐺)‘𝑋) ≠ ((invg𝐺)‘ 1 ))
10619, 90grpinvid 18227 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 ∈ Grp → ((invg𝐺)‘ 1 ) = 1 )
10795, 106syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((invg𝐺)‘ 1 ) = 1 )
108105, 91, 1073netr3d 3027 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (∗ ∘ 𝑋) ≠ 1 )
109 eldifsn 4677 . . . . . . . . . . . . . . . . . . . . 21 ((∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 }) ↔ ((∗ ∘ 𝑋) ∈ 𝐷 ∧ (∗ ∘ 𝑋) ≠ 1 ))
11098, 108, 109sylanbrc 586 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 }))
111 nnuz 12321 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
112 1zzd 12052 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℤ)
113 2fveq3 6663 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑚)))
114 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚𝑛 = 𝑚)
115113, 114oveq12d 7168 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ((𝑋‘(𝐿𝑛)) / 𝑛) = ((𝑋‘(𝐿𝑚)) / 𝑚))
116115fveq2d 6662 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)) = (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
117 eqid 2758 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛))) = (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))
118 fvex 6671 . . . . . . . . . . . . . . . . . . . . . . . 24 (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) ∈ V
119116, 117, 118fvmpt 6759 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
120119adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
121 nnre 11681 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
122121adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
123122cjred 14633 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ ℕ) → (∗‘𝑚) = 𝑚)
124123oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ ℕ) → ((∗‘(𝑋‘(𝐿𝑚))) / (∗‘𝑚)) = ((∗‘(𝑋‘(𝐿𝑚))) / 𝑚))
12510adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ ℕ) → 𝑋:(Base‘𝑍)⟶ℂ)
1262, 4, 17znzrhfo 20315 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℕ0𝐿:ℤ–onto→(Base‘𝑍))
12721, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐿:ℤ–onto→(Base‘𝑍))
128 fof 6576 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐿:ℤ⟶(Base‘𝑍))
130 nnz 12043 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
131 ffvelrn 6840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑚 ∈ ℤ) → (𝐿𝑚) ∈ (Base‘𝑍))
132129, 130, 131syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ ℕ) → (𝐿𝑚) ∈ (Base‘𝑍))
133125, 132ffvelrnd 6843 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ ℕ) → (𝑋‘(𝐿𝑚)) ∈ ℂ)
134 nncn 11682 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
135134adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
136 nnne0 11708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
137136adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ ℕ) → 𝑚 ≠ 0)
138133, 135, 137cjdivd 14630 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ ℕ) → (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) = ((∗‘(𝑋‘(𝐿𝑚))) / (∗‘𝑚)))
139 fvco3 6751 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋:(Base‘𝑍)⟶ℂ ∧ (𝐿𝑚) ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘(𝐿𝑚)) = (∗‘(𝑋‘(𝐿𝑚))))
140125, 132, 139syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ ℕ) → ((∗ ∘ 𝑋)‘(𝐿𝑚)) = (∗‘(𝑋‘(𝐿𝑚))))
141140oveq1d 7165 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ ℕ) → (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) = ((∗‘(𝑋‘(𝐿𝑚))) / 𝑚))
142124, 138, 1413eqtr4d 2803 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ ℕ) → (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) = (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚))
143120, 142eqtrd 2793 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))‘𝑚) = (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚))
144133cjcld 14603 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ ℕ) → (∗‘(𝑋‘(𝐿𝑚))) ∈ ℂ)
145144, 135, 137divcld 11454 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ ℕ) → ((∗‘(𝑋‘(𝐿𝑚))) / 𝑚) ∈ ℂ)
146141, 145eqeltrd 2852 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ ℕ) → (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) ∈ ℂ)
147 eqid 2758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))
1482, 17, 18, 1, 3, 19, 9, 100, 147dchrmusumlema 26176 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))
149 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡)
1507adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋𝑊)
15118adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ)
1529adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋𝐷)
153100adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋1 )
154 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞))
155 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))
1562, 17, 151, 1, 3, 19, 152, 153, 147, 154, 149, 155, 5dchrvmaeq0 26187 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑋𝑊𝑡 = 0))
157150, 156mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑡 = 0)
158149, 157breqtrd 5058 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 0)
159158rexlimdvaa 3209 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 0))
160159exlimdv 1934 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 0))
161148, 160mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))) ⇝ 0)
162 seqex 13420 . . . . . . . . . . . . . . . . . . . . . . . 24 seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))) ∈ V
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))) ∈ V)
164 2fveq3 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = 𝑚 → (𝑋‘(𝐿𝑎)) = (𝑋‘(𝐿𝑚)))
165 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = 𝑚𝑎 = 𝑚)
166164, 165oveq12d 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = 𝑚 → ((𝑋‘(𝐿𝑎)) / 𝑎) = ((𝑋‘(𝐿𝑚)) / 𝑚))
167 ovex 7183 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑋‘(𝐿𝑚)) / 𝑚) ∈ V
168166, 147, 167fvmpt 6759 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℕ → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿𝑚)) / 𝑚))
169168adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿𝑚)) / 𝑚))
170133, 135, 137divcld 11454 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ ℕ) → ((𝑋‘(𝐿𝑚)) / 𝑚) ∈ ℂ)
171169, 170eqeltrd 2852 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))‘𝑚) ∈ ℂ)
172111, 112, 171serf 13448 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))):ℕ⟶ℂ)
173172ffvelrnda 6842 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘𝑘) ∈ ℂ)
174 fzfid 13390 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
175 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → 𝜑)
176 elfznn 12985 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ)
177175, 176, 170syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑋‘(𝐿𝑚)) / 𝑚) ∈ ℂ)
178174, 177fsumcj 15213 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → (∗‘Σ𝑚 ∈ (1...𝑘)((𝑋‘(𝐿𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...𝑘)(∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
179175, 176, 169syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿𝑚)) / 𝑚))
180 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
181180, 111eleqtrdi 2862 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
182179, 181, 177fsumser 15135 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((𝑋‘(𝐿𝑚)) / 𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘𝑘))
183182fveq2d 6662 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → (∗‘Σ𝑚 ∈ (1...𝑘)((𝑋‘(𝐿𝑚)) / 𝑚)) = (∗‘(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘𝑘)))
184175, 176, 120syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)))
185170cjcld 14603 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ ℕ) → (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) ∈ ℂ)
186175, 176, 185syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) ∈ ℂ)
187184, 181, 186fsumser 15135 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(∗‘((𝑋‘(𝐿𝑚)) / 𝑚)) = (seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛))))‘𝑘))
188178, 183, 1873eqtr3rd 2802 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → (seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛))))‘𝑘) = (∗‘(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)))‘𝑘)))
189111, 161, 163, 112, 173, 188climcj 15009 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))) ⇝ (∗‘0))
190 cj0 14565 . . . . . . . . . . . . . . . . . . . . . 22 (∗‘0) = 0
191189, 190breqtrdi 5073 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (∗‘((𝑋‘(𝐿𝑛)) / 𝑛)))) ⇝ 0)
192111, 112, 143, 146, 191isumclim 15160 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) = 0)
193 fveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (∗ ∘ 𝑋) → (𝑦‘(𝐿𝑚)) = ((∗ ∘ 𝑋)‘(𝐿𝑚)))
194193oveq1d 7165 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (∗ ∘ 𝑋) → ((𝑦‘(𝐿𝑚)) / 𝑚) = (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚))
195194sumeq2sdv 15109 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (∗ ∘ 𝑋) → Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚))
196195eqeq1d 2760 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (∗ ∘ 𝑋) → (Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0 ↔ Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) = 0))
197196, 5elrab2 3605 . . . . . . . . . . . . . . . . . . . 20 ((∗ ∘ 𝑋) ∈ 𝑊 ↔ ((∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 }) ∧ Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿𝑚)) / 𝑚) = 0))
198110, 192, 197sylanbrc 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∗ ∘ 𝑋) ∈ 𝑊)
199198ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (∗ ∘ 𝑋) ∈ 𝑊)
2007ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑋𝑊)
201 simplr 768 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (∗ ∘ 𝑋) ≠ 𝑋)
20289, 199, 200, 201nehash2 13884 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 2 ≤ (♯‘𝑊))
203 suble0 11192 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → ((2 − (♯‘𝑊)) ≤ 0 ↔ 2 ≤ (♯‘𝑊)))
20477, 79, 203sylancr 590 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 − (♯‘𝑊)) ≤ 0 ↔ 2 ≤ (♯‘𝑊)))
205202, 204mpbird 260 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (2 − (♯‘𝑊)) ≤ 0)
20680, 75, 72, 88, 205lemul2ad 11618 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (2 − (♯‘𝑊))) ≤ ((log‘𝑥) · 0))
207 df-2 11737 . . . . . . . . . . . . . . . . . . 19 2 = (1 + 1)
208207oveq1i 7160 . . . . . . . . . . . . . . . . . 18 (2 − (♯‘𝑊)) = ((1 + 1) − (♯‘𝑊))
209 1cnd 10674 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ)
21079recnd 10707 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (♯‘𝑊) ∈ ℂ)
211209, 209, 210addsubassd 11055 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((1 + 1) − (♯‘𝑊)) = (1 + (1 − (♯‘𝑊))))
212208, 211syl5eq 2805 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (2 − (♯‘𝑊)) = (1 + (1 − (♯‘𝑊))))
213212oveq2d 7166 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (2 − (♯‘𝑊))) = ((log‘𝑥) · (1 + (1 − (♯‘𝑊)))))
21471adantrr 716 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ)
21564ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 − (♯‘𝑊)) ∈ ℝ)
216215recnd 10707 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 − (♯‘𝑊)) ∈ ℂ)
217214, 209, 216adddid 10703 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (1 + (1 − (♯‘𝑊)))) = (((log‘𝑥) · 1) + ((log‘𝑥) · (1 − (♯‘𝑊)))))
218214mulid1d 10696 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · 1) = (log‘𝑥))
219218oveq1d 7165 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥) · 1) + ((log‘𝑥) · (1 − (♯‘𝑊)))) = ((log‘𝑥) + ((log‘𝑥) · (1 − (♯‘𝑊)))))
220213, 217, 2193eqtrd 2797 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · (2 − (♯‘𝑊))) = ((log‘𝑥) + ((log‘𝑥) · (1 − (♯‘𝑊)))))
221214mul01d 10877 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) · 0) = 0)
222206, 220, 2213brtr3d 5063 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) + ((log‘𝑥) · (1 − (♯‘𝑊)))) ≤ 0)
22333nnred 11689 . . . . . . . . . . . . . . . 16 (𝜑 → (ϕ‘𝑁) ∈ ℝ)
224223ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ϕ‘𝑁) ∈ ℝ)
22549ad2ant2r 746 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛) ∈ ℝ)
22634ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ϕ‘𝑁) ∈ ℕ0)
227226nn0ge0d 11997 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (ϕ‘𝑁))
22844, 45syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → (Λ‘𝑛) ∈ ℝ)
229 vmage0 25805 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
23044, 229syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 0 ≤ (Λ‘𝑛))
23144nnred 11689 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 𝑛 ∈ ℝ)
23244nngt0d 11723 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 0 < 𝑛)
233 divge0 11547 . . . . . . . . . . . . . . . . . 18 ((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤ (Λ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤ ((Λ‘𝑛) / 𝑛))
234228, 230, 231, 232, 233syl22anc 837 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
23540, 48, 234fsumge0 15198 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → 0 ≤ Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛))
236235ad2ant2r 746 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛))
237224, 225, 227, 236mulge0d 11255 . . . . . . . . . . . . . 14 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)))
23874, 75, 76, 222, 237letrd 10835 . . . . . . . . . . . . 13 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) + ((log‘𝑥) · (1 − (♯‘𝑊)))) ≤ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)))
239 leaddsub 11154 . . . . . . . . . . . . . 14 (((log‘𝑥) ∈ ℝ ∧ ((log‘𝑥) · (1 − (♯‘𝑊))) ∈ ℝ ∧ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ) → (((log‘𝑥) + ((log‘𝑥) · (1 − (♯‘𝑊)))) ≤ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ↔ (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))))
24072, 73, 76, 239syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥) + ((log‘𝑥) · (1 − (♯‘𝑊)))) ≤ ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) ↔ (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))))
241238, 240mpbid 235 . . . . . . . . . . . 12 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))))
24272, 88absidd 14830 . . . . . . . . . . . 12 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(log‘𝑥)) = (log‘𝑥))
24367ad2ant2r 746 . . . . . . . . . . . . 13 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))) ∈ ℝ)
24475, 72, 243, 88, 241letrd 10835 . . . . . . . . . . . . 13 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))))
245243, 244absidd 14830 . . . . . . . . . . . 12 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) = (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))))
246241, 242, 2453brtr4d 5064 . . . . . . . . . . 11 (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(log‘𝑥)) ≤ (abs‘(((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (𝐿 “ {(1r𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))))
24716, 32, 69, 71, 246o1le 15057 . . . . . . . . . 10 ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1))
248247ex 416 . . . . . . . . 9 (𝜑 → ((∗ ∘ 𝑋) ≠ 𝑋 → (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1)))
249248necon1bd 2969 . . . . . . . 8 (𝜑 → (¬ (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1) → (∗ ∘ 𝑋) = 𝑋))
25015, 249mpi 20 . . . . . . 7 (𝜑 → (∗ ∘ 𝑋) = 𝑋)
251250adantr 484 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑍)) → (∗ ∘ 𝑋) = 𝑋)
252251fveq1d 6660 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (𝑋𝑥))
25314, 252eqtr3d 2795 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑍)) → (∗‘(𝑋𝑥)) = (𝑋𝑥))
25412, 253cjrebd 14609 . . 3 ((𝜑𝑥 ∈ (Base‘𝑍)) → (𝑋𝑥) ∈ ℝ)
255254ralrimiva 3113 . 2 (𝜑 → ∀𝑥 ∈ (Base‘𝑍)(𝑋𝑥) ∈ ℝ)
256 ffnfv 6873 . 2 (𝑋:(Base‘𝑍)⟶ℝ ↔ (𝑋 Fn (Base‘𝑍) ∧ ∀𝑥 ∈ (Base‘𝑍)(𝑋𝑥) ∈ ℝ))
25711, 255, 256sylanbrc 586 1 (𝜑𝑋:(Base‘𝑍)⟶ℝ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  {crab 3074  Vcvv 3409   ∖ cdif 3855   ∩ cin 3857   ⊆ wss 3858  {csn 4522   class class class wbr 5032   ↦ cmpt 5112  ◡ccnv 5523   “ cima 5527   ∘ ccom 5528   Fn wfn 6330  ⟶wf 6331  –onto→wfo 6333  ‘cfv 6335  (class class class)co 7150  Fincfn 8527  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576   + caddc 10578   · cmul 10580  +∞cpnf 10710   < clt 10713   ≤ cle 10714   − cmin 10908   / cdiv 11335  ℕcn 11674  2c2 11729  ℕ0cn0 11934  ℤcz 12020  ℤ≥cuz 12282  ℝ+crp 12430  [,)cico 12781  ...cfz 12939  ⌊cfl 13209  seqcseq 13418  ♯chash 13740  ∗ccj 14503  abscabs 14641   ⇝ cli 14889  𝑂(1)co1 14891  Σcsu 15090  ϕcphi 16156  Basecbs 16541  0gc0g 16771  Grpcgrp 18169  invgcminusg 18170  Abelcabl 18974  1rcur 19319  Ringcrg 19365  CRingccrg 19366  Unitcui 19460  ℤRHomczrh 20269  ℤ/nℤczn 20272  logclog 25245  Λcvma 25776  DChrcdchr 25915 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653  ax-addf 10654  ax-mulf 10655 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-iin 4886  df-disj 4998  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-rpss 7447  df-om 7580  df-1st 7693  df-2nd 7694  df-supp 7836  df-tpos 7902  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-oadd 8116  df-omul 8117  df-er 8299  df-ec 8301  df-qs 8305  df-map 8418  df-pm 8419  df-ixp 8480  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-fsupp 8867  df-fi 8908  df-sup 8939  df-inf 8940  df-oi 9007  df-dju 9363  df-card 9401  df-acn 9404  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-7 11742  df-8 11743  df-9 11744  df-n0 11935  df-xnn0 12007  df-z 12021  df-dec 12138  df-uz 12283  df-q 12389  df-rp 12431  df-xneg 12548  df-xadd 12549  df-xmul 12550  df-ioo 12783  df-ioc 12784  df-ico 12785  df-icc 12786  df-fz 12940  df-fzo 13083  df-fl 13211  df-mod 13287  df-seq 13419  df-exp 13480  df-fac 13684  df-bc 13713  df-hash 13741  df-word 13914  df-concat 13970  df-s1 13997  df-shft 14474  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-limsup 14876  df-clim 14893  df-rlim 14894  df-o1 14895  df-lo1 14896  df-sum 15091  df-ef 15469  df-e 15470  df-sin 15471  df-cos 15472  df-tan 15473  df-pi 15474  df-dvds 15656  df-gcd 15894  df-prm 16068  df-phi 16158  df-pc 16229  df-struct 16543  df-ndx 16544  df-slot 16545  df-base 16547  df-sets 16548  df-ress 16549  df-plusg 16636  df-mulr 16637  df-starv 16638  df-sca 16639  df-vsca 16640  df-ip 16641  df-tset 16642  df-ple 16643  df-ds 16645  df-unif 16646  df-hom 16647  df-cco 16648  df-rest 16754  df-topn 16755  df-0g 16773  df-gsum 16774  df-topgen 16775  df-pt 16776  df-prds 16779  df-xrs 16833  df-qtop 16838  df-imas 16839  df-qus 16840  df-xps 16841  df-mre 16915  df-mrc 16916  df-acs 16918  df-mgm 17918  df-sgrp 17967  df-mnd 17978  df-mhm 18022  df-submnd 18023  df-grp 18172  df-minusg 18173  df-sbg 18174  df-mulg 18292  df-subg 18343  df-nsg 18344  df-eqg 18345  df-ghm 18423  df-gim 18466  df-ga 18487  df-cntz 18514  df-oppg 18541  df-od 18723  df-gex 18724  df-pgp 18725  df-lsm 18828  df-pj1 18829  df-cmn 18975  df-abl 18976  df-cyg 19065  df-dprd 19185  df-dpj 19186  df-mgp 19308  df-ur 19320  df-ring 19367  df-cring 19368  df-oppr 19444  df-dvdsr 19462  df-unit 19463  df-invr 19493  df-dvr 19504  df-rnghom 19538  df-drng 19572  df-subrg 19601  df-lmod 19704  df-lss 19772  df-lsp 19812  df-sra 20012  df-rgmod 20013  df-lidl 20014  df-rsp 20015  df-2idl 20073  df-psmet 20158  df-xmet 20159  df-met 20160  df-bl 20161  df-mopn 20162  df-fbas 20163  df-fg 20164  df-cnfld 20167  df-zring 20239  df-zrh 20273  df-zn 20276  df-top 21594  df-topon 21611  df-topsp 21633  df-bases 21646  df-cld 21719  df-ntr 21720  df-cls 21721  df-nei 21798  df-lp 21836  df-perf 21837  df-cn 21927  df-cnp 21928  df-haus 22015  df-cmp 22087  df-tx 22262  df-hmeo 22455  df-fil 22546  df-fm 22638  df-flim 22639  df-flf 22640  df-xms 23022  df-ms 23023  df-tms 23024  df-cncf 23579  df-0p 24370  df-limc 24565  df-dv 24566  df-ply 24884  df-idp 24885  df-coe 24886  df-dgr 24887  df-quot 24986  df-ulm 25071  df-log 25247  df-cxp 25248  df-atan 25552  df-em 25677  df-cht 25781  df-vma 25782  df-chp 25783  df-ppi 25784  df-mu 25785  df-dchr 25916 This theorem is referenced by:  dchrisum0  26203
 Copyright terms: Public domain W3C validator