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

Theorem dvfsum2 26075
Description: The reverse of dvfsumrlim 26072, when comparing a finite sum of increasing terms to an integral. In this case there is no point in stating the limit properties, because the terms of the sum aren't approaching zero, but there is nevertheless still a natural asymptotic statement that can be made. (Contributed by Mario Carneiro, 20-May-2016.)
Hypotheses
Ref Expression
dvfsum2.s 𝑆 = (𝑇(,)+∞)
dvfsum2.z 𝑍 = (ℤ𝑀)
dvfsum2.m (𝜑𝑀 ∈ ℤ)
dvfsum2.d (𝜑𝐷 ∈ ℝ)
dvfsum2.u (𝜑𝑈 ∈ ℝ*)
dvfsum2.md (𝜑𝑀 ≤ (𝐷 + 1))
dvfsum2.t (𝜑𝑇 ∈ ℝ)
dvfsum2.a ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
dvfsum2.b1 ((𝜑𝑥𝑆) → 𝐵𝑉)
dvfsum2.b2 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
dvfsum2.b3 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
dvfsum2.c (𝑥 = 𝑘𝐵 = 𝐶)
dvfsum2.l ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐵𝐶)
dvfsum2.g 𝐺 = (𝑥𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴))
dvfsum2.0 ((𝜑 ∧ (𝑥𝑆𝐷𝑥)) → 0 ≤ 𝐵)
dvfsum2.1 (𝜑𝑋𝑆)
dvfsum2.2 (𝜑𝑌𝑆)
dvfsum2.3 (𝜑𝐷𝑋)
dvfsum2.4 (𝜑𝑋𝑌)
dvfsum2.5 (𝜑𝑌𝑈)
dvfsum2.e (𝑥 = 𝑌𝐵 = 𝐸)
Assertion
Ref Expression
dvfsum2 (𝜑 → (abs‘((𝐺𝑌) − (𝐺𝑋))) ≤ 𝐸)
Distinct variable groups:   𝐵,𝑘   𝑥,𝐶   𝑥,𝑘,𝐷   𝜑,𝑘,𝑥   𝑥,𝐸   𝑘,𝑀,𝑥   𝑆,𝑘,𝑥   𝑘,𝑋,𝑥   𝑘,𝑌,𝑥   𝑥,𝑇   𝑈,𝑘,𝑥   𝑥,𝑉   𝑥,𝑍
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥)   𝐶(𝑘)   𝑇(𝑘)   𝐸(𝑘)   𝐺(𝑥,𝑘)   𝑉(𝑘)   𝑍(𝑘)

Proof of Theorem dvfsum2
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 dvfsum2.2 . . . . . 6 (𝜑𝑌𝑆)
2 fzfid 14014 . . . . . . . 8 (𝜑 → (𝑀...(⌊‘𝑌)) ∈ Fin)
3 dvfsum2.b2 . . . . . . . . . 10 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
43ralrimiva 3146 . . . . . . . . 9 (𝜑 → ∀𝑥𝑍 𝐵 ∈ ℝ)
5 elfzuz 13560 . . . . . . . . . 10 (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ (ℤ𝑀))
6 dvfsum2.z . . . . . . . . . 10 𝑍 = (ℤ𝑀)
75, 6eleqtrrdi 2852 . . . . . . . . 9 (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘𝑍)
8 dvfsum2.c . . . . . . . . . . 11 (𝑥 = 𝑘𝐵 = 𝐶)
98eleq1d 2826 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
109rspccva 3621 . . . . . . . . 9 ((∀𝑥𝑍 𝐵 ∈ ℝ ∧ 𝑘𝑍) → 𝐶 ∈ ℝ)
114, 7, 10syl2an 596 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℝ)
122, 11fsumrecl 15770 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℝ)
13 dvfsum2.a . . . . . . . . 9 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
1413ralrimiva 3146 . . . . . . . 8 (𝜑 → ∀𝑥𝑆 𝐴 ∈ ℝ)
15 nfcsb1v 3923 . . . . . . . . . 10 𝑥𝑌 / 𝑥𝐴
1615nfel1 2922 . . . . . . . . 9 𝑥𝑌 / 𝑥𝐴 ∈ ℝ
17 csbeq1a 3913 . . . . . . . . . 10 (𝑥 = 𝑌𝐴 = 𝑌 / 𝑥𝐴)
1817eleq1d 2826 . . . . . . . . 9 (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ 𝑌 / 𝑥𝐴 ∈ ℝ))
1916, 18rspc 3610 . . . . . . . 8 (𝑌𝑆 → (∀𝑥𝑆 𝐴 ∈ ℝ → 𝑌 / 𝑥𝐴 ∈ ℝ))
201, 14, 19sylc 65 . . . . . . 7 (𝜑𝑌 / 𝑥𝐴 ∈ ℝ)
2112, 20resubcld 11691 . . . . . 6 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) ∈ ℝ)
22 nfcv 2905 . . . . . . 7 𝑥𝑌
23 nfcv 2905 . . . . . . . 8 𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶
24 nfcv 2905 . . . . . . . 8 𝑥
2523, 24, 15nfov 7461 . . . . . . 7 𝑥𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)
26 fveq2 6906 . . . . . . . . . 10 (𝑥 = 𝑌 → (⌊‘𝑥) = (⌊‘𝑌))
2726oveq2d 7447 . . . . . . . . 9 (𝑥 = 𝑌 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑌)))
2827sumeq1d 15736 . . . . . . . 8 (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
2928, 17oveq12d 7449 . . . . . . 7 (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))
30 dvfsum2.g . . . . . . 7 𝐺 = (𝑥𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴))
3122, 25, 29, 30fvmptf 7037 . . . . . 6 ((𝑌𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) ∈ ℝ) → (𝐺𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))
321, 21, 31syl2anc 584 . . . . 5 (𝜑 → (𝐺𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))
33 dvfsum2.1 . . . . . 6 (𝜑𝑋𝑆)
34 fzfid 14014 . . . . . . . 8 (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin)
35 elfzuz 13560 . . . . . . . . . 10 (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ𝑀))
3635, 6eleqtrrdi 2852 . . . . . . . . 9 (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘𝑍)
374, 36, 10syl2an 596 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ)
3834, 37fsumrecl 15770 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ)
39 nfcsb1v 3923 . . . . . . . . . 10 𝑥𝑋 / 𝑥𝐴
4039nfel1 2922 . . . . . . . . 9 𝑥𝑋 / 𝑥𝐴 ∈ ℝ
41 csbeq1a 3913 . . . . . . . . . 10 (𝑥 = 𝑋𝐴 = 𝑋 / 𝑥𝐴)
4241eleq1d 2826 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ 𝑋 / 𝑥𝐴 ∈ ℝ))
4340, 42rspc 3610 . . . . . . . 8 (𝑋𝑆 → (∀𝑥𝑆 𝐴 ∈ ℝ → 𝑋 / 𝑥𝐴 ∈ ℝ))
4433, 14, 43sylc 65 . . . . . . 7 (𝜑𝑋 / 𝑥𝐴 ∈ ℝ)
4538, 44resubcld 11691 . . . . . 6 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ∈ ℝ)
46 nfcv 2905 . . . . . . 7 𝑥𝑋
47 nfcv 2905 . . . . . . . 8 𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶
4847, 24, 39nfov 7461 . . . . . . 7 𝑥𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)
49 fveq2 6906 . . . . . . . . . 10 (𝑥 = 𝑋 → (⌊‘𝑥) = (⌊‘𝑋))
5049oveq2d 7447 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑋)))
5150sumeq1d 15736 . . . . . . . 8 (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
5251, 41oveq12d 7449 . . . . . . 7 (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))
5346, 48, 52, 30fvmptf 7037 . . . . . 6 ((𝑋𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ∈ ℝ) → (𝐺𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))
5433, 45, 53syl2anc 584 . . . . 5 (𝜑 → (𝐺𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))
5532, 54oveq12d 7449 . . . 4 (𝜑 → ((𝐺𝑌) − (𝐺𝑋)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)))
5655fveq2d 6910 . . 3 (𝜑 → (abs‘((𝐺𝑌) − (𝐺𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))))
5721recnd 11289 . . . 4 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) ∈ ℂ)
5845recnd 11289 . . . 4 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ∈ ℂ)
5957, 58abssubd 15492 . . 3 (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))))
6056, 59eqtrd 2777 . 2 (𝜑 → (abs‘((𝐺𝑌) − (𝐺𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))))
61 dvfsum2.s . . . . . . . . . 10 𝑆 = (𝑇(,)+∞)
62 ioossre 13448 . . . . . . . . . 10 (𝑇(,)+∞) ⊆ ℝ
6361, 62eqsstri 4030 . . . . . . . . 9 𝑆 ⊆ ℝ
6463a1i 11 . . . . . . . 8 (𝜑𝑆 ⊆ ℝ)
65 dvfsum2.b1 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐵𝑉)
66 dvfsum2.b3 . . . . . . . 8 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
6764, 13, 65, 66dvmptrecl 26064 . . . . . . 7 ((𝜑𝑥𝑆) → 𝐵 ∈ ℝ)
6867ralrimiva 3146 . . . . . 6 (𝜑 → ∀𝑥𝑆 𝐵 ∈ ℝ)
69 dvfsum2.e . . . . . . . 8 (𝑥 = 𝑌𝐵 = 𝐸)
7069eleq1d 2826 . . . . . . 7 (𝑥 = 𝑌 → (𝐵 ∈ ℝ ↔ 𝐸 ∈ ℝ))
7170rspcv 3618 . . . . . 6 (𝑌𝑆 → (∀𝑥𝑆 𝐵 ∈ ℝ → 𝐸 ∈ ℝ))
721, 68, 71sylc 65 . . . . 5 (𝜑𝐸 ∈ ℝ)
7321, 72resubcld 11691 . . . 4 (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) − 𝐸) ∈ ℝ)
7463, 33sselid 3981 . . . . . . . 8 (𝜑𝑋 ∈ ℝ)
75 reflcl 13836 . . . . . . . . 9 (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
7674, 75syl 17 . . . . . . . 8 (𝜑 → (⌊‘𝑋) ∈ ℝ)
7774, 76resubcld 11691 . . . . . . 7 (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ)
78 nfv 1914 . . . . . . . . . 10 𝑚 𝐵 ∈ ℝ
79 nfcsb1v 3923 . . . . . . . . . . 11 𝑥𝑚 / 𝑥𝐵
8079nfel1 2922 . . . . . . . . . 10 𝑥𝑚 / 𝑥𝐵 ∈ ℝ
81 csbeq1a 3913 . . . . . . . . . . 11 (𝑥 = 𝑚𝐵 = 𝑚 / 𝑥𝐵)
8281eleq1d 2826 . . . . . . . . . 10 (𝑥 = 𝑚 → (𝐵 ∈ ℝ ↔ 𝑚 / 𝑥𝐵 ∈ ℝ))
8378, 80, 82cbvralw 3306 . . . . . . . . 9 (∀𝑥𝑆 𝐵 ∈ ℝ ↔ ∀𝑚𝑆 𝑚 / 𝑥𝐵 ∈ ℝ)
8468, 83sylib 218 . . . . . . . 8 (𝜑 → ∀𝑚𝑆 𝑚 / 𝑥𝐵 ∈ ℝ)
85 csbeq1 3902 . . . . . . . . . 10 (𝑚 = 𝑋𝑚 / 𝑥𝐵 = 𝑋 / 𝑥𝐵)
8685eleq1d 2826 . . . . . . . . 9 (𝑚 = 𝑋 → (𝑚 / 𝑥𝐵 ∈ ℝ ↔ 𝑋 / 𝑥𝐵 ∈ ℝ))
8786rspcv 3618 . . . . . . . 8 (𝑋𝑆 → (∀𝑚𝑆 𝑚 / 𝑥𝐵 ∈ ℝ → 𝑋 / 𝑥𝐵 ∈ ℝ))
8833, 84, 87sylc 65 . . . . . . 7 (𝜑𝑋 / 𝑥𝐵 ∈ ℝ)
8977, 88remulcld 11291 . . . . . 6 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ∈ ℝ)
9089, 45readdcld 11290 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) ∈ ℝ)
9190, 88resubcld 11691 . . . 4 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵) ∈ ℝ)
9263, 1sselid 3981 . . . . . . . . 9 (𝜑𝑌 ∈ ℝ)
93 reflcl 13836 . . . . . . . . . 10 (𝑌 ∈ ℝ → (⌊‘𝑌) ∈ ℝ)
9492, 93syl 17 . . . . . . . . 9 (𝜑 → (⌊‘𝑌) ∈ ℝ)
9592, 94resubcld 11691 . . . . . . . 8 (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℝ)
9695, 72remulcld 11291 . . . . . . 7 (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℝ)
9796, 21readdcld 11290 . . . . . 6 (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) ∈ ℝ)
9897, 72resubcld 11691 . . . . 5 (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − 𝐸) ∈ ℝ)
99 fracge0 13844 . . . . . . . . 9 (𝑌 ∈ ℝ → 0 ≤ (𝑌 − (⌊‘𝑌)))
10092, 99syl 17 . . . . . . . 8 (𝜑 → 0 ≤ (𝑌 − (⌊‘𝑌)))
101 dvfsum2.0 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑆𝐷𝑥)) → 0 ≤ 𝐵)
102101expr 456 . . . . . . . . . 10 ((𝜑𝑥𝑆) → (𝐷𝑥 → 0 ≤ 𝐵))
103102ralrimiva 3146 . . . . . . . . 9 (𝜑 → ∀𝑥𝑆 (𝐷𝑥 → 0 ≤ 𝐵))
104 dvfsum2.d . . . . . . . . . 10 (𝜑𝐷 ∈ ℝ)
105 dvfsum2.3 . . . . . . . . . 10 (𝜑𝐷𝑋)
106 dvfsum2.4 . . . . . . . . . 10 (𝜑𝑋𝑌)
107104, 74, 92, 105, 106letrd 11418 . . . . . . . . 9 (𝜑𝐷𝑌)
108 breq2 5147 . . . . . . . . . . 11 (𝑥 = 𝑌 → (𝐷𝑥𝐷𝑌))
10969breq2d 5155 . . . . . . . . . . 11 (𝑥 = 𝑌 → (0 ≤ 𝐵 ↔ 0 ≤ 𝐸))
110108, 109imbi12d 344 . . . . . . . . . 10 (𝑥 = 𝑌 → ((𝐷𝑥 → 0 ≤ 𝐵) ↔ (𝐷𝑌 → 0 ≤ 𝐸)))
111110rspcv 3618 . . . . . . . . 9 (𝑌𝑆 → (∀𝑥𝑆 (𝐷𝑥 → 0 ≤ 𝐵) → (𝐷𝑌 → 0 ≤ 𝐸)))
1121, 103, 107, 111syl3c 66 . . . . . . . 8 (𝜑 → 0 ≤ 𝐸)
11395, 72, 100, 112mulge0d 11840 . . . . . . 7 (𝜑 → 0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸))
11421, 96addge02d 11852 . . . . . . 7 (𝜑 → (0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))))
115113, 114mpbid 232 . . . . . 6 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)))
11621, 97, 72, 115lesub1dd 11879 . . . . 5 (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) − 𝐸) ≤ ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − 𝐸))
117 dvfsum2.m . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
118 dvfsum2.md . . . . . . . . . . 11 (𝜑𝑀 ≤ (𝐷 + 1))
119 dvfsum2.t . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
12013renegcld 11690 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → -𝐴 ∈ ℝ)
12167renegcld 11690 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → -𝐵 ∈ ℝ)
1223renegcld 11690 . . . . . . . . . . 11 ((𝜑𝑥𝑍) → -𝐵 ∈ ℝ)
123 reelprrecn 11247 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, ℂ}
124123a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ {ℝ, ℂ})
12513recnd 11289 . . . . . . . . . . . 12 ((𝜑𝑥𝑆) → 𝐴 ∈ ℂ)
126124, 125, 65, 66dvmptneg 26004 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑥𝑆 ↦ -𝐴)) = (𝑥𝑆 ↦ -𝐵))
1278negeqd 11502 . . . . . . . . . . 11 (𝑥 = 𝑘 → -𝐵 = -𝐶)
128 dvfsum2.u . . . . . . . . . . 11 (𝜑𝑈 ∈ ℝ*)
129 dvfsum2.l . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐵𝐶)
13067adantrr 717 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑆𝑘𝑆)) → 𝐵 ∈ ℝ)
1311303adant3 1133 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐵 ∈ ℝ)
132 simp2r 1201 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝑘𝑆)
133683ad2ant1 1134 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → ∀𝑥𝑆 𝐵 ∈ ℝ)
1349rspcv 3618 . . . . . . . . . . . . . 14 (𝑘𝑆 → (∀𝑥𝑆 𝐵 ∈ ℝ → 𝐶 ∈ ℝ))
135132, 133, 134sylc 65 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶 ∈ ℝ)
136131, 135lenegd 11842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → (𝐵𝐶 ↔ -𝐶 ≤ -𝐵))
137129, 136mpbid 232 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → -𝐶 ≤ -𝐵)
138 eqid 2737 . . . . . . . . . . 11 (𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴))) = (𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))
139 dvfsum2.5 . . . . . . . . . . 11 (𝜑𝑌𝑈)
14061, 6, 117, 104, 118, 119, 120, 121, 122, 126, 127, 128, 137, 138, 33, 1, 105, 106, 139dvfsumlem3 26069 . . . . . . . . . 10 (𝜑 → (((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) ∧ (((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − 𝑋 / 𝑥-𝐵) ≤ (((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − 𝑌 / 𝑥-𝐵)))
141140simprd 495 . . . . . . . . 9 (𝜑 → (((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − 𝑋 / 𝑥-𝐵) ≤ (((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − 𝑌 / 𝑥-𝐵))
14277recnd 11289 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ)
14388recnd 11289 . . . . . . . . . . . . . . . 16 (𝜑𝑋 / 𝑥𝐵 ∈ ℂ)
144142, 143mulneg2d 11717 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) = -((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵))
14538recnd 11289 . . . . . . . . . . . . . . . . 17 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ)
14644recnd 11289 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 / 𝑥𝐴 ∈ ℂ)
147145, 146neg2subd 11637 . . . . . . . . . . . . . . . 16 (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -𝑋 / 𝑥𝐴) = (𝑋 / 𝑥𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
14837recnd 11289 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℂ)
14934, 148fsumneg 15823 . . . . . . . . . . . . . . . . 17 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
150149oveq1d 7446 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -𝑋 / 𝑥𝐴))
151145, 146negsubdi2d 11636 . . . . . . . . . . . . . . . 16 (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) = (𝑋 / 𝑥𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
152147, 150, 1513eqtr4d 2787 . . . . . . . . . . . . . . 15 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))
153144, 152oveq12d 7449 . . . . . . . . . . . . . 14 (𝜑 → (((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴)) = (-((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)))
15489recnd 11289 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ∈ ℂ)
155154, 58negdid 11633 . . . . . . . . . . . . . 14 (𝜑 → -(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) = (-((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)))
156153, 155eqtr4d 2780 . . . . . . . . . . . . 13 (𝜑 → (((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴)) = -(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)))
15790renegcld 11690 . . . . . . . . . . . . 13 (𝜑 → -(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) ∈ ℝ)
158156, 157eqeltrd 2841 . . . . . . . . . . . 12 (𝜑 → (((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴)) ∈ ℝ)
159 nfcv 2905 . . . . . . . . . . . . . . 15 𝑥(𝑋 − (⌊‘𝑋))
160 nfcv 2905 . . . . . . . . . . . . . . 15 𝑥 ·
161 nfcsb1v 3923 . . . . . . . . . . . . . . . 16 𝑥𝑋 / 𝑥𝐵
162161nfneg 11504 . . . . . . . . . . . . . . 15 𝑥-𝑋 / 𝑥𝐵
163159, 160, 162nfov 7461 . . . . . . . . . . . . . 14 𝑥((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵)
164 nfcv 2905 . . . . . . . . . . . . . 14 𝑥 +
165 nfcv 2905 . . . . . . . . . . . . . . 15 𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶
16639nfneg 11504 . . . . . . . . . . . . . . 15 𝑥-𝑋 / 𝑥𝐴
167165, 24, 166nfov 7461 . . . . . . . . . . . . . 14 𝑥𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴)
168163, 164, 167nfov 7461 . . . . . . . . . . . . 13 𝑥(((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴))
169 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋𝑥 = 𝑋)
170169, 49oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝑥 − (⌊‘𝑥)) = (𝑋 − (⌊‘𝑋)))
171 csbeq1a 3913 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋𝐵 = 𝑋 / 𝑥𝐵)
172171negeqd 11502 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → -𝐵 = -𝑋 / 𝑥𝐵)
173170, 172oveq12d 7449 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵))
17450sumeq1d 15736 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶)
17541negeqd 11502 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → -𝐴 = -𝑋 / 𝑥𝐴)
176174, 175oveq12d 7449 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴))
177173, 176oveq12d 7449 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴)))
17846, 168, 177, 138fvmptf 7037 . . . . . . . . . . . 12 ((𝑋𝑆 ∧ (((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴)) ∈ ℝ) → ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴)))
17933, 158, 178syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -𝑋 / 𝑥𝐴)))
180179, 156eqtrd 2777 . . . . . . . . . 10 (𝜑 → ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = -(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)))
181 csbnegg 11505 . . . . . . . . . . 11 (𝑋𝑆𝑋 / 𝑥-𝐵 = -𝑋 / 𝑥𝐵)
18233, 181syl 17 . . . . . . . . . 10 (𝜑𝑋 / 𝑥-𝐵 = -𝑋 / 𝑥𝐵)
183180, 182oveq12d 7449 . . . . . . . . 9 (𝜑 → (((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − 𝑋 / 𝑥-𝐵) = (-(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − -𝑋 / 𝑥𝐵))
18495recnd 11289 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℂ)
18572recnd 11289 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ ℂ)
186184, 185mulneg2d 11717 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (⌊‘𝑌)) · -𝐸) = -((𝑌 − (⌊‘𝑌)) · 𝐸))
18712recnd 11289 . . . . . . . . . . . . . . . . 17 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℂ)
18820recnd 11289 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 / 𝑥𝐴 ∈ ℂ)
189187, 188neg2subd 11637 . . . . . . . . . . . . . . . 16 (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -𝑌 / 𝑥𝐴) = (𝑌 / 𝑥𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
19011recnd 11289 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℂ)
1912, 190fsumneg 15823 . . . . . . . . . . . . . . . . 17 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
192191oveq1d 7446 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -𝑌 / 𝑥𝐴))
193187, 188negsubdi2d 11636 . . . . . . . . . . . . . . . 16 (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) = (𝑌 / 𝑥𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
194189, 192, 1933eqtr4d 2787 . . . . . . . . . . . . . . 15 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))
195186, 194oveq12d 7449 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)))
19696recnd 11289 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℂ)
197196, 57negdid 11633 . . . . . . . . . . . . . 14 (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)))
198195, 197eqtr4d 2780 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴)) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)))
19997renegcld 11690 . . . . . . . . . . . . 13 (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) ∈ ℝ)
200198, 199eqeltrd 2841 . . . . . . . . . . . 12 (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴)) ∈ ℝ)
201 nfcv 2905 . . . . . . . . . . . . . 14 𝑥((𝑌 − (⌊‘𝑌)) · -𝐸)
202 nfcv 2905 . . . . . . . . . . . . . . 15 𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶
20315nfneg 11504 . . . . . . . . . . . . . . 15 𝑥-𝑌 / 𝑥𝐴
204202, 24, 203nfov 7461 . . . . . . . . . . . . . 14 𝑥𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴)
205201, 164, 204nfov 7461 . . . . . . . . . . . . 13 𝑥(((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴))
206 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌𝑥 = 𝑌)
207206, 26oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → (𝑥 − (⌊‘𝑥)) = (𝑌 − (⌊‘𝑌)))
20869negeqd 11502 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → -𝐵 = -𝐸)
209207, 208oveq12d 7449 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑌 − (⌊‘𝑌)) · -𝐸))
21027sumeq1d 15736 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶)
21117negeqd 11502 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → -𝐴 = -𝑌 / 𝑥𝐴)
212210, 211oveq12d 7449 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴))
213209, 212oveq12d 7449 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴)))
21422, 205, 213, 138fvmptf 7037 . . . . . . . . . . . 12 ((𝑌𝑆 ∧ (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴)) ∈ ℝ) → ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴)))
2151, 200, 214syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -𝑌 / 𝑥𝐴)))
216215, 198eqtrd 2777 . . . . . . . . . 10 (𝜑 → ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)))
217208adantl 481 . . . . . . . . . . 11 ((𝜑𝑥 = 𝑌) → -𝐵 = -𝐸)
2181, 217csbied 3935 . . . . . . . . . 10 (𝜑𝑌 / 𝑥-𝐵 = -𝐸)
219216, 218oveq12d 7449 . . . . . . . . 9 (𝜑 → (((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − 𝑌 / 𝑥-𝐵) = (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − -𝐸))
220141, 183, 2193brtr3d 5174 . . . . . . . 8 (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − -𝑋 / 𝑥𝐵) ≤ (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − -𝐸))
22190recnd 11289 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) ∈ ℂ)
222221, 143neg2subd 11637 . . . . . . . 8 (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − -𝑋 / 𝑥𝐵) = (𝑋 / 𝑥𝐵 − (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))))
22397recnd 11289 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) ∈ ℂ)
224223, 185neg2subd 11637 . . . . . . . 8 (𝜑 → (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − -𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))))
225220, 222, 2243brtr3d 5174 . . . . . . 7 (𝜑 → (𝑋 / 𝑥𝐵 − (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))) ≤ (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))))
226221, 143negsubdi2d 11636 . . . . . . 7 (𝜑 → -((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵) = (𝑋 / 𝑥𝐵 − (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))))
227223, 185negsubdi2d 11636 . . . . . . 7 (𝜑 → -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − 𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))))
228225, 226, 2273brtr4d 5175 . . . . . 6 (𝜑 → -((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − 𝐸))
22998, 91lenegd 11842 . . . . . 6 (𝜑 → (((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵) ↔ -((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − 𝐸)))
230228, 229mpbird 257 . . . . 5 (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵))
23173, 98, 91, 116, 230letrd 11418 . . . 4 (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵))
232 1red 11262 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
233 nfv 1914 . . . . . . . . . . 11 𝑥 𝐷𝑋
234 nfcv 2905 . . . . . . . . . . . 12 𝑥0
235 nfcv 2905 . . . . . . . . . . . 12 𝑥
236234, 235, 161nfbr 5190 . . . . . . . . . . 11 𝑥0 ≤ 𝑋 / 𝑥𝐵
237233, 236nfim 1896 . . . . . . . . . 10 𝑥(𝐷𝑋 → 0 ≤ 𝑋 / 𝑥𝐵)
238 breq2 5147 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝐷𝑥𝐷𝑋))
239171breq2d 5155 . . . . . . . . . . 11 (𝑥 = 𝑋 → (0 ≤ 𝐵 ↔ 0 ≤ 𝑋 / 𝑥𝐵))
240238, 239imbi12d 344 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝐷𝑥 → 0 ≤ 𝐵) ↔ (𝐷𝑋 → 0 ≤ 𝑋 / 𝑥𝐵)))
241237, 240rspc 3610 . . . . . . . . 9 (𝑋𝑆 → (∀𝑥𝑆 (𝐷𝑥 → 0 ≤ 𝐵) → (𝐷𝑋 → 0 ≤ 𝑋 / 𝑥𝐵)))
24233, 103, 105, 241syl3c 66 . . . . . . . 8 (𝜑 → 0 ≤ 𝑋 / 𝑥𝐵)
243 fracle1 13843 . . . . . . . . 9 (𝑋 ∈ ℝ → (𝑋 − (⌊‘𝑋)) ≤ 1)
24474, 243syl 17 . . . . . . . 8 (𝜑 → (𝑋 − (⌊‘𝑋)) ≤ 1)
24577, 232, 88, 242, 244lemul1ad 12207 . . . . . . 7 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ≤ (1 · 𝑋 / 𝑥𝐵))
246143mullidd 11279 . . . . . . 7 (𝜑 → (1 · 𝑋 / 𝑥𝐵) = 𝑋 / 𝑥𝐵)
247245, 246breqtrd 5169 . . . . . 6 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ≤ 𝑋 / 𝑥𝐵)
24889, 88, 45, 247leadd1dd 11877 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) ≤ (𝑋 / 𝑥𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)))
24990, 88, 45lesubadd2d 11862 . . . . 5 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ↔ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) ≤ (𝑋 / 𝑥𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))))
250248, 249mpbird 257 . . . 4 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) − 𝑋 / 𝑥𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))
25173, 91, 45, 231, 250letrd 11418 . . 3 (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))
25221, 72readdcld 11290 . . . 4 (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) + 𝐸) ∈ ℝ)
253 fracge0 13844 . . . . . . 7 (𝑋 ∈ ℝ → 0 ≤ (𝑋 − (⌊‘𝑋)))
25474, 253syl 17 . . . . . 6 (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋)))
25577, 88, 254, 242mulge0d 11840 . . . . 5 (𝜑 → 0 ≤ ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵))
25645, 89addge02d 11852 . . . . 5 (𝜑 → (0 ≤ ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))))
257255, 256mpbid 232 . . . 4 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)))
258140simpld 494 . . . . . . 7 (𝜑 → ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋))
259258, 216, 1803brtr3d 5174 . . . . . 6 (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)))
26090, 97lenegd 11842 . . . . . 6 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) ↔ -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴))))
261259, 260mpbird 257 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)))
262 fracle1 13843 . . . . . . . . . 10 (𝑌 ∈ ℝ → (𝑌 − (⌊‘𝑌)) ≤ 1)
26392, 262syl 17 . . . . . . . . 9 (𝜑 → (𝑌 − (⌊‘𝑌)) ≤ 1)
26495, 232, 72, 112, 263lemul1ad 12207 . . . . . . . 8 (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ (1 · 𝐸))
265185mullidd 11279 . . . . . . . 8 (𝜑 → (1 · 𝐸) = 𝐸)
266264, 265breqtrd 5169 . . . . . . 7 (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ 𝐸)
26796, 72, 21, 266leadd1dd 11877 . . . . . 6 (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) ≤ (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)))
268185, 57addcomd 11463 . . . . . 6 (𝜑 → (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) + 𝐸))
269267, 268breqtrd 5169 . . . . 5 (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) + 𝐸))
27090, 97, 252, 261, 269letrd 11418 . . . 4 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) + 𝐸))
27145, 90, 252, 257, 270letrd 11418 . . 3 (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) + 𝐸))
27245, 21, 72absdifled 15473 . . 3 (𝜑 → ((abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))) ≤ 𝐸 ↔ (((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴) + 𝐸))))
273251, 271, 272mpbir2and 713 . 2 (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶𝑋 / 𝑥𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶𝑌 / 𝑥𝐴))) ≤ 𝐸)
27460, 273eqbrtrd 5165 1 (𝜑 → (abs‘((𝐺𝑌) − (𝐺𝑋))) ≤ 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  csb 3899  wss 3951  {cpr 4628   class class class wbr 5143  cmpt 5225  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  +∞cpnf 11292  *cxr 11294  cle 11296  cmin 11492  -cneg 11493  cz 12613  cuz 12878  (,)cioo 13387  ...cfz 13547  cfl 13830  abscabs 15273  Σcsu 15722   D cdv 25898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-cmp 23395  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902
This theorem is referenced by:  logfacbnd3  27267  log2sumbnd  27588
  Copyright terms: Public domain W3C validator