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

Theorem dvfsumlem3 24312
 Description: Lemma for dvfsumrlim 24315. (Contributed by Mario Carneiro, 17-May-2016.)
Hypotheses
Ref Expression
dvfsum.s 𝑆 = (𝑇(,)+∞)
dvfsum.z 𝑍 = (ℤ𝑀)
dvfsum.m (𝜑𝑀 ∈ ℤ)
dvfsum.d (𝜑𝐷 ∈ ℝ)
dvfsum.md (𝜑𝑀 ≤ (𝐷 + 1))
dvfsum.t (𝜑𝑇 ∈ ℝ)
dvfsum.a ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
dvfsum.b1 ((𝜑𝑥𝑆) → 𝐵𝑉)
dvfsum.b2 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
dvfsum.b3 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
dvfsum.c (𝑥 = 𝑘𝐵 = 𝐶)
dvfsum.u (𝜑𝑈 ∈ ℝ*)
dvfsum.l ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵)
dvfsum.h 𝐻 = (𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴)))
dvfsumlem1.1 (𝜑𝑋𝑆)
dvfsumlem1.2 (𝜑𝑌𝑆)
dvfsumlem1.3 (𝜑𝐷𝑋)
dvfsumlem1.4 (𝜑𝑋𝑌)
dvfsumlem1.5 (𝜑𝑌𝑈)
Assertion
Ref Expression
dvfsumlem3 (𝜑 → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
Distinct variable groups:   𝐵,𝑘   𝑥,𝐶   𝑥,𝑘,𝐷   𝜑,𝑘,𝑥   𝑆,𝑘,𝑥   𝑘,𝑀,𝑥   𝑥,𝑇   𝑘,𝑌,𝑥   𝑥,𝑍   𝑈,𝑘,𝑥   𝑘,𝑋,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥)   𝐶(𝑘)   𝑇(𝑘)   𝐻(𝑥,𝑘)   𝑉(𝑥,𝑘)   𝑍(𝑘)

Proof of Theorem dvfsumlem3
Dummy variables 𝑦 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . 4 𝑆 = (𝑇(,)+∞)
2 ioossre 12652 . . . 4 (𝑇(,)+∞) ⊆ ℝ
31, 2eqsstri 3928 . . 3 𝑆 ⊆ ℝ
4 dvfsumlem1.2 . . 3 (𝜑𝑌𝑆)
53, 4sseldi 3893 . 2 (𝜑𝑌 ∈ ℝ)
6 dvfsumlem1.1 . . . 4 (𝜑𝑋𝑆)
73, 6sseldi 3893 . . 3 (𝜑𝑋 ∈ ℝ)
8 reflcl 13020 . . 3 (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
9 peano2re 10666 . . 3 ((⌊‘𝑋) ∈ ℝ → ((⌊‘𝑋) + 1) ∈ ℝ)
107, 8, 93syl 18 . 2 (𝜑 → ((⌊‘𝑋) + 1) ∈ ℝ)
11 dvfsum.z . . 3 𝑍 = (ℤ𝑀)
12 dvfsum.m . . . 4 (𝜑𝑀 ∈ ℤ)
1312adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑀 ∈ ℤ)
14 dvfsum.d . . . 4 (𝜑𝐷 ∈ ℝ)
1514adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝐷 ∈ ℝ)
16 dvfsum.md . . . 4 (𝜑𝑀 ≤ (𝐷 + 1))
1716adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑀 ≤ (𝐷 + 1))
18 dvfsum.t . . . 4 (𝜑𝑇 ∈ ℝ)
1918adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑇 ∈ ℝ)
20 dvfsum.a . . . 4 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
2120adantlr 711 . . 3 (((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) ∧ 𝑥𝑆) → 𝐴 ∈ ℝ)
22 dvfsum.b1 . . . 4 ((𝜑𝑥𝑆) → 𝐵𝑉)
2322adantlr 711 . . 3 (((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) ∧ 𝑥𝑆) → 𝐵𝑉)
24 dvfsum.b2 . . . 4 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
2524adantlr 711 . . 3 (((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) ∧ 𝑥𝑍) → 𝐵 ∈ ℝ)
26 dvfsum.b3 . . . 4 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
2726adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
28 dvfsum.c . . 3 (𝑥 = 𝑘𝐵 = 𝐶)
29 dvfsum.u . . . 4 (𝜑𝑈 ∈ ℝ*)
3029adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑈 ∈ ℝ*)
31 dvfsum.l . . . 4 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵)
32313adant1r 1170 . . 3 (((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵)
33 dvfsum.h . . 3 𝐻 = (𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴)))
346adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑋𝑆)
354adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑌𝑆)
36 dvfsumlem1.3 . . . 4 (𝜑𝐷𝑋)
3736adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝐷𝑋)
38 dvfsumlem1.4 . . . 4 (𝜑𝑋𝑌)
3938adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑋𝑌)
40 dvfsumlem1.5 . . . 4 (𝜑𝑌𝑈)
4140adantr 481 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑌𝑈)
42 simpr 485 . . 3 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → 𝑌 ≤ ((⌊‘𝑋) + 1))
431, 11, 13, 15, 17, 19, 21, 23, 25, 27, 28, 30, 32, 33, 34, 35, 37, 39, 41, 42dvfsumlem2 24311 . 2 ((𝜑𝑌 ≤ ((⌊‘𝑋) + 1)) → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
443a1i 11 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ℝ)
4544sselda 3895 . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝑥 ∈ ℝ)
46 reflcl 13020 . . . . . . . . . . 11 (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
4745, 46syl 17 . . . . . . . . . 10 ((𝜑𝑥𝑆) → (⌊‘𝑥) ∈ ℝ)
4845, 47resubcld 10922 . . . . . . . . 9 ((𝜑𝑥𝑆) → (𝑥 − (⌊‘𝑥)) ∈ ℝ)
4944, 20, 22, 26dvmptrecl 24308 . . . . . . . . 9 ((𝜑𝑥𝑆) → 𝐵 ∈ ℝ)
5048, 49remulcld 10524 . . . . . . . 8 ((𝜑𝑥𝑆) → ((𝑥 − (⌊‘𝑥)) · 𝐵) ∈ ℝ)
51 fzfid 13195 . . . . . . . . . 10 ((𝜑𝑥𝑆) → (𝑀...(⌊‘𝑥)) ∈ Fin)
5224ralrimiva 3151 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑍 𝐵 ∈ ℝ)
5352adantr 481 . . . . . . . . . . 11 ((𝜑𝑥𝑆) → ∀𝑥𝑍 𝐵 ∈ ℝ)
54 elfzuz 12758 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...(⌊‘𝑥)) → 𝑘 ∈ (ℤ𝑀))
5554, 11syl6eleqr 2896 . . . . . . . . . . 11 (𝑘 ∈ (𝑀...(⌊‘𝑥)) → 𝑘𝑍)
5628eleq1d 2869 . . . . . . . . . . . 12 (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
5756rspccva 3560 . . . . . . . . . . 11 ((∀𝑥𝑍 𝐵 ∈ ℝ ∧ 𝑘𝑍) → 𝐶 ∈ ℝ)
5853, 55, 57syl2an 595 . . . . . . . . . 10 (((𝜑𝑥𝑆) ∧ 𝑘 ∈ (𝑀...(⌊‘𝑥))) → 𝐶 ∈ ℝ)
5951, 58fsumrecl 14928 . . . . . . . . 9 ((𝜑𝑥𝑆) → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 ∈ ℝ)
6059, 20resubcld 10922 . . . . . . . 8 ((𝜑𝑥𝑆) → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴) ∈ ℝ)
6150, 60readdcld 10523 . . . . . . 7 ((𝜑𝑥𝑆) → (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴)) ∈ ℝ)
6261, 33fmptd 6748 . . . . . 6 (𝜑𝐻:𝑆⟶ℝ)
6362adantr 481 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝐻:𝑆⟶ℝ)
644adantr 481 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑌𝑆)
6563, 64ffvelrnd 6724 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻𝑌) ∈ ℝ)
665adantr 481 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑌 ∈ ℝ)
67 reflcl 13020 . . . . . . . 8 (𝑌 ∈ ℝ → (⌊‘𝑌) ∈ ℝ)
6866, 67syl 17 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) ∈ ℝ)
6918adantr 481 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑇 ∈ ℝ)
707adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑋 ∈ ℝ)
7170, 8, 93syl 18 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) ∈ ℝ)
726, 1syl6eleq 2895 . . . . . . . . . . . 12 (𝜑𝑋 ∈ (𝑇(,)+∞))
7318rexrd 10544 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℝ*)
74 elioopnf 12685 . . . . . . . . . . . . 13 (𝑇 ∈ ℝ* → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
7573, 74syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
7672, 75mpbid 233 . . . . . . . . . . 11 (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))
7776simprd 496 . . . . . . . . . 10 (𝜑𝑇 < 𝑋)
78 fllep1 13025 . . . . . . . . . . 11 (𝑋 ∈ ℝ → 𝑋 ≤ ((⌊‘𝑋) + 1))
797, 78syl 17 . . . . . . . . . 10 (𝜑𝑋 ≤ ((⌊‘𝑋) + 1))
8018, 7, 10, 77, 79ltletrd 10653 . . . . . . . . 9 (𝜑𝑇 < ((⌊‘𝑋) + 1))
8180adantr 481 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑇 < ((⌊‘𝑋) + 1))
82 simpr 485 . . . . . . . . 9 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) ≤ 𝑌)
8370flcld 13022 . . . . . . . . . . 11 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑋) ∈ ℤ)
8483peano2zd 11944 . . . . . . . . . 10 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) ∈ ℤ)
85 flge 13029 . . . . . . . . . 10 ((𝑌 ∈ ℝ ∧ ((⌊‘𝑋) + 1) ∈ ℤ) → (((⌊‘𝑋) + 1) ≤ 𝑌 ↔ ((⌊‘𝑋) + 1) ≤ (⌊‘𝑌)))
8666, 84, 85syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (((⌊‘𝑋) + 1) ≤ 𝑌 ↔ ((⌊‘𝑋) + 1) ≤ (⌊‘𝑌)))
8782, 86mpbid 233 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) ≤ (⌊‘𝑌))
8869, 71, 68, 81, 87ltletrd 10653 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑇 < (⌊‘𝑌))
8973adantr 481 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑇 ∈ ℝ*)
90 elioopnf 12685 . . . . . . . 8 (𝑇 ∈ ℝ* → ((⌊‘𝑌) ∈ (𝑇(,)+∞) ↔ ((⌊‘𝑌) ∈ ℝ ∧ 𝑇 < (⌊‘𝑌))))
9189, 90syl 17 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑌) ∈ (𝑇(,)+∞) ↔ ((⌊‘𝑌) ∈ ℝ ∧ 𝑇 < (⌊‘𝑌))))
9268, 88, 91mpbir2and 709 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) ∈ (𝑇(,)+∞))
9392, 1syl6eleqr 2896 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) ∈ 𝑆)
9463, 93ffvelrnd 6724 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻‘(⌊‘𝑌)) ∈ ℝ)
956adantr 481 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑋𝑆)
9663, 95ffvelrnd 6724 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻𝑋) ∈ ℝ)
9712adantr 481 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑀 ∈ ℤ)
9814adantr 481 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝐷 ∈ ℝ)
9916adantr 481 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑀 ≤ (𝐷 + 1))
10020adantlr 711 . . . . . 6 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑥𝑆) → 𝐴 ∈ ℝ)
10122adantlr 711 . . . . . 6 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑥𝑆) → 𝐵𝑉)
10224adantlr 711 . . . . . 6 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑥𝑍) → 𝐵 ∈ ℝ)
10326adantr 481 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
10429adantr 481 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑈 ∈ ℝ*)
105313adant1r 1170 . . . . . 6 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵)
10636adantr 481 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝐷𝑋)
10770, 78syl 17 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑋 ≤ ((⌊‘𝑋) + 1))
10898, 70, 71, 106, 107letrd 10650 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝐷 ≤ ((⌊‘𝑋) + 1))
10998, 71, 68, 108, 87letrd 10650 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝐷 ≤ (⌊‘𝑌))
110 flle 13023 . . . . . . 7 (𝑌 ∈ ℝ → (⌊‘𝑌) ≤ 𝑌)
11166, 110syl 17 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) ≤ 𝑌)
11240adantr 481 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑌𝑈)
113 fllep1 13025 . . . . . . . 8 (𝑌 ∈ ℝ → 𝑌 ≤ ((⌊‘𝑌) + 1))
11466, 113syl 17 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑌 ≤ ((⌊‘𝑌) + 1))
115 flidm 13033 . . . . . . . . 9 (𝑌 ∈ ℝ → (⌊‘(⌊‘𝑌)) = (⌊‘𝑌))
11666, 115syl 17 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘(⌊‘𝑌)) = (⌊‘𝑌))
117116oveq1d 7038 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘(⌊‘𝑌)) + 1) = ((⌊‘𝑌) + 1))
118114, 117breqtrrd 4996 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑌 ≤ ((⌊‘(⌊‘𝑌)) + 1))
1191, 11, 97, 98, 99, 69, 100, 101, 102, 103, 28, 104, 105, 33, 93, 64, 109, 111, 112, 118dvfsumlem2 24311 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻𝑌) ≤ (𝐻‘(⌊‘𝑌)) ∧ ((𝐻‘(⌊‘𝑌)) − (⌊‘𝑌) / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
120119simpld 495 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻𝑌) ≤ (𝐻‘(⌊‘𝑌)))
121 elioopnf 12685 . . . . . . . . . 10 (𝑇 ∈ ℝ* → (((⌊‘𝑋) + 1) ∈ (𝑇(,)+∞) ↔ (((⌊‘𝑋) + 1) ∈ ℝ ∧ 𝑇 < ((⌊‘𝑋) + 1))))
12273, 121syl 17 . . . . . . . . 9 (𝜑 → (((⌊‘𝑋) + 1) ∈ (𝑇(,)+∞) ↔ (((⌊‘𝑋) + 1) ∈ ℝ ∧ 𝑇 < ((⌊‘𝑋) + 1))))
12310, 80, 122mpbir2and 709 . . . . . . . 8 (𝜑 → ((⌊‘𝑋) + 1) ∈ (𝑇(,)+∞))
124123, 1syl6eleqr 2896 . . . . . . 7 (𝜑 → ((⌊‘𝑋) + 1) ∈ 𝑆)
125124adantr 481 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) ∈ 𝑆)
12663, 125ffvelrnd 6724 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻‘((⌊‘𝑋) + 1)) ∈ ℝ)
12766flcld 13022 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) ∈ ℤ)
128 eluz2 12103 . . . . . . 7 ((⌊‘𝑌) ∈ (ℤ‘((⌊‘𝑋) + 1)) ↔ (((⌊‘𝑋) + 1) ∈ ℤ ∧ (⌊‘𝑌) ∈ ℤ ∧ ((⌊‘𝑋) + 1) ≤ (⌊‘𝑌)))
12984, 127, 87, 128syl3anbrc 1336 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) ∈ (ℤ‘((⌊‘𝑋) + 1)))
13063adantr 481 . . . . . . 7 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝐻:𝑆⟶ℝ)
131 elfzelz 12762 . . . . . . . . . . 11 (𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌)) → 𝑚 ∈ ℤ)
132131adantl 482 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑚 ∈ ℤ)
133132zred 11941 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑚 ∈ ℝ)
13469adantr 481 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑇 ∈ ℝ)
13571adantr 481 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → ((⌊‘𝑋) + 1) ∈ ℝ)
13680ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑇 < ((⌊‘𝑋) + 1))
137 elfzle1 12764 . . . . . . . . . . 11 (𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌)) → ((⌊‘𝑋) + 1) ≤ 𝑚)
138137adantl 482 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → ((⌊‘𝑋) + 1) ≤ 𝑚)
139134, 135, 133, 136, 138ltletrd 10653 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑇 < 𝑚)
14073ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑇 ∈ ℝ*)
141 elioopnf 12685 . . . . . . . . . 10 (𝑇 ∈ ℝ* → (𝑚 ∈ (𝑇(,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑇 < 𝑚)))
142140, 141syl 17 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → (𝑚 ∈ (𝑇(,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑇 < 𝑚)))
143133, 139, 142mpbir2and 709 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑚 ∈ (𝑇(,)+∞))
144143, 1syl6eleqr 2896 . . . . . . 7 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑚𝑆)
145130, 144ffvelrnd 6724 . . . . . 6 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → (𝐻𝑚) ∈ ℝ)
14697adantr 481 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑀 ∈ ℤ)
14798adantr 481 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝐷 ∈ ℝ)
14816ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑀 ≤ (𝐷 + 1))
14969adantr 481 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑇 ∈ ℝ)
150100adantlr 711 . . . . . . . 8 ((((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) ∧ 𝑥𝑆) → 𝐴 ∈ ℝ)
151101adantlr 711 . . . . . . . 8 ((((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) ∧ 𝑥𝑆) → 𝐵𝑉)
152102adantlr 711 . . . . . . . 8 ((((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) ∧ 𝑥𝑍) → 𝐵 ∈ ℝ)
153103adantr 481 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
154104adantr 481 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑈 ∈ ℝ*)
1551053adant1r 1170 . . . . . . . 8 ((((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵)
156 elfzelz 12762 . . . . . . . . . . . 12 (𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1)) → 𝑚 ∈ ℤ)
157156adantl 482 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑚 ∈ ℤ)
158157zred 11941 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑚 ∈ ℝ)
15971adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → ((⌊‘𝑋) + 1) ∈ ℝ)
16080ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑇 < ((⌊‘𝑋) + 1))
161 elfzle1 12764 . . . . . . . . . . . 12 (𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1)) → ((⌊‘𝑋) + 1) ≤ 𝑚)
162161adantl 482 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → ((⌊‘𝑋) + 1) ≤ 𝑚)
163149, 159, 158, 160, 162ltletrd 10653 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑇 < 𝑚)
164149rexrd 10544 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑇 ∈ ℝ*)
165164, 141syl 17 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 ∈ (𝑇(,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑇 < 𝑚)))
166158, 163, 165mpbir2and 709 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑚 ∈ (𝑇(,)+∞))
167166, 1syl6eleqr 2896 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑚𝑆)
168 peano2re 10666 . . . . . . . . . . 11 (𝑚 ∈ ℝ → (𝑚 + 1) ∈ ℝ)
169158, 168syl 17 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 + 1) ∈ ℝ)
170158lep1d 11425 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑚 ≤ (𝑚 + 1))
171149, 158, 169, 163, 170ltletrd 10653 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑇 < (𝑚 + 1))
172 elioopnf 12685 . . . . . . . . . . 11 (𝑇 ∈ ℝ* → ((𝑚 + 1) ∈ (𝑇(,)+∞) ↔ ((𝑚 + 1) ∈ ℝ ∧ 𝑇 < (𝑚 + 1))))
173164, 172syl 17 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → ((𝑚 + 1) ∈ (𝑇(,)+∞) ↔ ((𝑚 + 1) ∈ ℝ ∧ 𝑇 < (𝑚 + 1))))
174169, 171, 173mpbir2and 709 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 + 1) ∈ (𝑇(,)+∞))
175174, 1syl6eleqr 2896 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 + 1) ∈ 𝑆)
176108adantr 481 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝐷 ≤ ((⌊‘𝑋) + 1))
177147, 159, 158, 176, 162letrd 10650 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝐷𝑚)
178169rexrd 10544 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 + 1) ∈ ℝ*)
17968rexrd 10544 . . . . . . . . . 10 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) ∈ ℝ*)
180179adantr 481 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (⌊‘𝑌) ∈ ℝ*)
181 elfzle2 12765 . . . . . . . . . . 11 (𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1)) → 𝑚 ≤ ((⌊‘𝑌) − 1))
182181adantl 482 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑚 ≤ ((⌊‘𝑌) − 1))
183 1red 10495 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 1 ∈ ℝ)
18466adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑌 ∈ ℝ)
185184, 67syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (⌊‘𝑌) ∈ ℝ)
186 leaddsub 10970 . . . . . . . . . . 11 ((𝑚 ∈ ℝ ∧ 1 ∈ ℝ ∧ (⌊‘𝑌) ∈ ℝ) → ((𝑚 + 1) ≤ (⌊‘𝑌) ↔ 𝑚 ≤ ((⌊‘𝑌) − 1)))
187158, 183, 185, 186syl3anc 1364 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → ((𝑚 + 1) ≤ (⌊‘𝑌) ↔ 𝑚 ≤ ((⌊‘𝑌) − 1)))
188182, 187mpbird 258 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 + 1) ≤ (⌊‘𝑌))
18966rexrd 10544 . . . . . . . . . . 11 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑌 ∈ ℝ*)
190179, 189, 104, 111, 112xrletrd 12409 . . . . . . . . . 10 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) ≤ 𝑈)
191190adantr 481 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (⌊‘𝑌) ≤ 𝑈)
192178, 180, 154, 188, 191xrletrd 12409 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 + 1) ≤ 𝑈)
193 flid 13032 . . . . . . . . . . . 12 (𝑚 ∈ ℤ → (⌊‘𝑚) = 𝑚)
194157, 193syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (⌊‘𝑚) = 𝑚)
195194eqcomd 2803 . . . . . . . . . 10 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → 𝑚 = (⌊‘𝑚))
196195oveq1d 7038 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 + 1) = ((⌊‘𝑚) + 1))
197169, 196eqled 10596 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝑚 + 1) ≤ ((⌊‘𝑚) + 1))
1981, 11, 146, 147, 148, 149, 150, 151, 152, 153, 28, 154, 155, 33, 167, 175, 177, 170, 192, 197dvfsumlem2 24311 . . . . . . 7 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → ((𝐻‘(𝑚 + 1)) ≤ (𝐻𝑚) ∧ ((𝐻𝑚) − 𝑚 / 𝑥𝐵) ≤ ((𝐻‘(𝑚 + 1)) − (𝑚 + 1) / 𝑥𝐵)))
199198simpld 495 . . . . . 6 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → (𝐻‘(𝑚 + 1)) ≤ (𝐻𝑚))
200129, 145, 199monoord2 13255 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻‘(⌊‘𝑌)) ≤ (𝐻‘((⌊‘𝑋) + 1)))
20171rexrd 10544 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) ∈ ℝ*)
202201, 179, 104, 87, 190xrletrd 12409 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) ≤ 𝑈)
20371leidd 11060 . . . . . . 7 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) ≤ ((⌊‘𝑋) + 1))
2041, 11, 97, 98, 99, 69, 100, 101, 102, 103, 28, 104, 105, 33, 95, 125, 106, 107, 202, 203dvfsumlem2 24311 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻‘((⌊‘𝑋) + 1)) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻‘((⌊‘𝑋) + 1)) − ((⌊‘𝑋) + 1) / 𝑥𝐵)))
205204simpld 495 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻‘((⌊‘𝑋) + 1)) ≤ (𝐻𝑋))
20694, 126, 96, 200, 205letrd 10650 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻‘(⌊‘𝑌)) ≤ (𝐻𝑋))
20765, 94, 96, 120, 206letrd 10650 . . 3 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (𝐻𝑌) ≤ (𝐻𝑋))
208 csbeq1 3820 . . . . . . 7 (𝑚 = 𝑋𝑚 / 𝑥𝐵 = 𝑋 / 𝑥𝐵)
209208eleq1d 2869 . . . . . 6 (𝑚 = 𝑋 → (𝑚 / 𝑥𝐵 ∈ ℝ ↔ 𝑋 / 𝑥𝐵 ∈ ℝ))
21049ralrimiva 3151 . . . . . . . . 9 (𝜑 → ∀𝑥𝑆 𝐵 ∈ ℝ)
211210adantr 481 . . . . . . . 8 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ∀𝑥𝑆 𝐵 ∈ ℝ)
212 nfcsb1v 3839 . . . . . . . . . 10 𝑥𝑚 / 𝑥𝐵
213212nfel1 2965 . . . . . . . . 9 𝑥𝑚 / 𝑥𝐵 ∈ ℝ
214 csbeq1a 3830 . . . . . . . . . 10 (𝑥 = 𝑚𝐵 = 𝑚 / 𝑥𝐵)
215214eleq1d 2869 . . . . . . . . 9 (𝑥 = 𝑚 → (𝐵 ∈ ℝ ↔ 𝑚 / 𝑥𝐵 ∈ ℝ))
216213, 215rspc 3555 . . . . . . . 8 (𝑚𝑆 → (∀𝑥𝑆 𝐵 ∈ ℝ → 𝑚 / 𝑥𝐵 ∈ ℝ))
217211, 216mpan9 507 . . . . . . 7 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚𝑆) → 𝑚 / 𝑥𝐵 ∈ ℝ)
218217ralrimiva 3151 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ∀𝑚𝑆 𝑚 / 𝑥𝐵 ∈ ℝ)
219209, 218, 95rspcdva 3567 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑋 / 𝑥𝐵 ∈ ℝ)
22096, 219resubcld 10922 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ∈ ℝ)
221 csbeq1 3820 . . . . . . 7 (𝑚 = (⌊‘𝑌) → 𝑚 / 𝑥𝐵 = (⌊‘𝑌) / 𝑥𝐵)
222221eleq1d 2869 . . . . . 6 (𝑚 = (⌊‘𝑌) → (𝑚 / 𝑥𝐵 ∈ ℝ ↔ (⌊‘𝑌) / 𝑥𝐵 ∈ ℝ))
223222, 218, 93rspcdva 3567 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → (⌊‘𝑌) / 𝑥𝐵 ∈ ℝ)
22494, 223resubcld 10922 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻‘(⌊‘𝑌)) − (⌊‘𝑌) / 𝑥𝐵) ∈ ℝ)
225 csbeq1 3820 . . . . . . 7 (𝑚 = 𝑌𝑚 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
226225eleq1d 2869 . . . . . 6 (𝑚 = 𝑌 → (𝑚 / 𝑥𝐵 ∈ ℝ ↔ 𝑌 / 𝑥𝐵 ∈ ℝ))
227226, 218, 64rspcdva 3567 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → 𝑌 / 𝑥𝐵 ∈ ℝ)
22865, 227resubcld 10922 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻𝑌) − 𝑌 / 𝑥𝐵) ∈ ℝ)
229 csbeq1 3820 . . . . . . . 8 (𝑚 = ((⌊‘𝑋) + 1) → 𝑚 / 𝑥𝐵 = ((⌊‘𝑋) + 1) / 𝑥𝐵)
230229eleq1d 2869 . . . . . . 7 (𝑚 = ((⌊‘𝑋) + 1) → (𝑚 / 𝑥𝐵 ∈ ℝ ↔ ((⌊‘𝑋) + 1) / 𝑥𝐵 ∈ ℝ))
231230, 218, 125rspcdva 3567 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((⌊‘𝑋) + 1) / 𝑥𝐵 ∈ ℝ)
232126, 231resubcld 10922 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻‘((⌊‘𝑋) + 1)) − ((⌊‘𝑋) + 1) / 𝑥𝐵) ∈ ℝ)
233204simprd 496 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻‘((⌊‘𝑋) + 1)) − ((⌊‘𝑋) + 1) / 𝑥𝐵))
234 fveq2 6545 . . . . . . . . . . 11 (𝑦 = 𝑚 → (𝐻𝑦) = (𝐻𝑚))
235 csbeq1 3820 . . . . . . . . . . 11 (𝑦 = 𝑚𝑦 / 𝑥𝐵 = 𝑚 / 𝑥𝐵)
236234, 235oveq12d 7041 . . . . . . . . . 10 (𝑦 = 𝑚 → ((𝐻𝑦) − 𝑦 / 𝑥𝐵) = ((𝐻𝑚) − 𝑚 / 𝑥𝐵))
237 eqid 2797 . . . . . . . . . 10 (𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵)) = (𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))
238 ovex 7055 . . . . . . . . . 10 ((𝐻𝑦) − 𝑦 / 𝑥𝐵) ∈ V
239236, 237, 238fvmpt3i 6647 . . . . . . . . 9 (𝑚 ∈ V → ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘𝑚) = ((𝐻𝑚) − 𝑚 / 𝑥𝐵))
240239elv 3445 . . . . . . . 8 ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘𝑚) = ((𝐻𝑚) − 𝑚 / 𝑥𝐵)
241144, 217syldan 591 . . . . . . . . 9 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → 𝑚 / 𝑥𝐵 ∈ ℝ)
242145, 241resubcld 10922 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → ((𝐻𝑚) − 𝑚 / 𝑥𝐵) ∈ ℝ)
243240, 242syl5eqel 2889 . . . . . . 7 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...(⌊‘𝑌))) → ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘𝑚) ∈ ℝ)
244198simprd 496 . . . . . . . 8 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → ((𝐻𝑚) − 𝑚 / 𝑥𝐵) ≤ ((𝐻‘(𝑚 + 1)) − (𝑚 + 1) / 𝑥𝐵))
245 ovex 7055 . . . . . . . . 9 (𝑚 + 1) ∈ V
246 fveq2 6545 . . . . . . . . . . 11 (𝑦 = (𝑚 + 1) → (𝐻𝑦) = (𝐻‘(𝑚 + 1)))
247 csbeq1 3820 . . . . . . . . . . 11 (𝑦 = (𝑚 + 1) → 𝑦 / 𝑥𝐵 = (𝑚 + 1) / 𝑥𝐵)
248246, 247oveq12d 7041 . . . . . . . . . 10 (𝑦 = (𝑚 + 1) → ((𝐻𝑦) − 𝑦 / 𝑥𝐵) = ((𝐻‘(𝑚 + 1)) − (𝑚 + 1) / 𝑥𝐵))
249248, 237, 238fvmpt3i 6647 . . . . . . . . 9 ((𝑚 + 1) ∈ V → ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘(𝑚 + 1)) = ((𝐻‘(𝑚 + 1)) − (𝑚 + 1) / 𝑥𝐵))
250245, 249ax-mp 5 . . . . . . . 8 ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘(𝑚 + 1)) = ((𝐻‘(𝑚 + 1)) − (𝑚 + 1) / 𝑥𝐵)
251244, 240, 2503brtr4g 5002 . . . . . . 7 (((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) ∧ 𝑚 ∈ (((⌊‘𝑋) + 1)...((⌊‘𝑌) − 1))) → ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘𝑚) ≤ ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘(𝑚 + 1)))
252129, 243, 251monoord 13254 . . . . . 6 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘((⌊‘𝑋) + 1)) ≤ ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘(⌊‘𝑌)))
253 ovex 7055 . . . . . . 7 ((⌊‘𝑋) + 1) ∈ V
254 fveq2 6545 . . . . . . . . 9 (𝑦 = ((⌊‘𝑋) + 1) → (𝐻𝑦) = (𝐻‘((⌊‘𝑋) + 1)))
255 csbeq1 3820 . . . . . . . . 9 (𝑦 = ((⌊‘𝑋) + 1) → 𝑦 / 𝑥𝐵 = ((⌊‘𝑋) + 1) / 𝑥𝐵)
256254, 255oveq12d 7041 . . . . . . . 8 (𝑦 = ((⌊‘𝑋) + 1) → ((𝐻𝑦) − 𝑦 / 𝑥𝐵) = ((𝐻‘((⌊‘𝑋) + 1)) − ((⌊‘𝑋) + 1) / 𝑥𝐵))
257256, 237, 238fvmpt3i 6647 . . . . . . 7 (((⌊‘𝑋) + 1) ∈ V → ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘((⌊‘𝑋) + 1)) = ((𝐻‘((⌊‘𝑋) + 1)) − ((⌊‘𝑋) + 1) / 𝑥𝐵))
258253, 257ax-mp 5 . . . . . 6 ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘((⌊‘𝑋) + 1)) = ((𝐻‘((⌊‘𝑋) + 1)) − ((⌊‘𝑋) + 1) / 𝑥𝐵)
259 fvex 6558 . . . . . . 7 (⌊‘𝑌) ∈ V
260 fveq2 6545 . . . . . . . . 9 (𝑦 = (⌊‘𝑌) → (𝐻𝑦) = (𝐻‘(⌊‘𝑌)))
261 csbeq1 3820 . . . . . . . . 9 (𝑦 = (⌊‘𝑌) → 𝑦 / 𝑥𝐵 = (⌊‘𝑌) / 𝑥𝐵)
262260, 261oveq12d 7041 . . . . . . . 8 (𝑦 = (⌊‘𝑌) → ((𝐻𝑦) − 𝑦 / 𝑥𝐵) = ((𝐻‘(⌊‘𝑌)) − (⌊‘𝑌) / 𝑥𝐵))
263262, 237, 238fvmpt3i 6647 . . . . . . 7 ((⌊‘𝑌) ∈ V → ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘(⌊‘𝑌)) = ((𝐻‘(⌊‘𝑌)) − (⌊‘𝑌) / 𝑥𝐵))
264259, 263ax-mp 5 . . . . . 6 ((𝑦 ∈ V ↦ ((𝐻𝑦) − 𝑦 / 𝑥𝐵))‘(⌊‘𝑌)) = ((𝐻‘(⌊‘𝑌)) − (⌊‘𝑌) / 𝑥𝐵)
265252, 258, 2643brtr3g 5001 . . . . 5 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻‘((⌊‘𝑋) + 1)) − ((⌊‘𝑋) + 1) / 𝑥𝐵) ≤ ((𝐻‘(⌊‘𝑌)) − (⌊‘𝑌) / 𝑥𝐵))
266220, 232, 224, 233, 265letrd 10650 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻‘(⌊‘𝑌)) − (⌊‘𝑌) / 𝑥𝐵))
267119simprd 496 . . . 4 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻‘(⌊‘𝑌)) − (⌊‘𝑌) / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵))
268220, 224, 228, 266, 267letrd 10650 . . 3 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵))
269207, 268jca 512 . 2 ((𝜑 ∧ ((⌊‘𝑋) + 1) ≤ 𝑌) → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
2705, 10, 43, 269lecasei 10599 1 (𝜑 → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083  ∀wral 3107  Vcvv 3440  ⦋csb 3817   ⊆ wss 3865   class class class wbr 4968   ↦ cmpt 5047  ⟶wf 6228  ‘cfv 6232  (class class class)co 7023  ℝcr 10389  1c1 10391   + caddc 10393   · cmul 10395  +∞cpnf 10525  ℝ*cxr 10527   < clt 10528   ≤ cle 10529   − cmin 10723  ℤcz 11835  ℤ≥cuz 12097  (,)cioo 12592  ...cfz 12746  ⌊cfl 13014  Σcsu 14880   D cdv 24148 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468  ax-addf 10469  ax-mulf 10470 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-of 7274  df-om 7444  df-1st 7552  df-2nd 7553  df-supp 7689  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-er 8146  df-map 8265  df-pm 8266  df-ixp 8318  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-fsupp 8687  df-fi 8728  df-sup 8759  df-inf 8760  df-oi 8827  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558  df-7 11559  df-8 11560  df-9 11561  df-n0 11752  df-z 11836  df-dec 11953  df-uz 12098  df-q 12202  df-rp 12244  df-xneg 12361  df-xadd 12362  df-xmul 12363  df-ioo 12596  df-ico 12598  df-icc 12599  df-fz 12747  df-fzo 12888  df-fl 13016  df-seq 13224  df-exp 13284  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-clim 14683  df-sum 14881  df-struct 16318  df-ndx 16319  df-slot 16320  df-base 16322  df-sets 16323  df-ress 16324  df-plusg 16411  df-mulr 16412  df-starv 16413  df-sca 16414  df-vsca 16415  df-ip 16416  df-tset 16417  df-ple 16418  df-ds 16420  df-unif 16421  df-hom 16422  df-cco 16423  df-rest 16529  df-topn 16530  df-0g 16548  df-gsum 16549  df-topgen 16550  df-pt 16551  df-prds 16554  df-xrs 16608  df-qtop 16613  df-imas 16614  df-xps 16616  df-mre 16690  df-mrc 16691  df-acs 16693  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-submnd 17779  df-mulg 17986  df-cntz 18192  df-cmn 18639  df-psmet 20223  df-xmet 20224  df-met 20225  df-bl 20226  df-mopn 20227  df-fbas 20228  df-fg 20229  df-cnfld 20232  df-top 21190  df-topon 21207  df-topsp 21229  df-bases 21242  df-cld 21315  df-ntr 21316  df-cls 21317  df-nei 21394  df-lp 21432  df-perf 21433  df-cn 21523  df-cnp 21524  df-haus 21611  df-cmp 21683  df-tx 21858  df-hmeo 22051  df-fil 22142  df-fm 22234  df-flim 22235  df-flf 22236  df-xms 22617  df-ms 22618  df-tms 22619  df-cncf 23173  df-limc 24151  df-dv 24152 This theorem is referenced by:  dvfsumlem4  24313  dvfsum2  24318
 Copyright terms: Public domain W3C validator