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

Theorem dvfsumlem2 24003
Description: Lemma for dvfsumrlim 24007. (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 (𝜑𝑌𝑈)
dvfsumlem1.6 (𝜑𝑌 ≤ ((⌊‘𝑋) + 1))
Assertion
Ref Expression
dvfsumlem2 (𝜑 → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
Distinct variable groups:   𝐵,𝑘   𝑥,𝐶   𝑥,𝑘,𝐷   𝜑,𝑘,𝑥   𝑆,𝑘,𝑥   𝑘,𝑀,𝑥   𝑥,𝑇   𝑘,𝑌,𝑥   𝑥,𝑍   𝑈,𝑘,𝑥   𝑘,𝑋,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥)   𝐶(𝑘)   𝑇(𝑘)   𝐻(𝑥,𝑘)   𝑉(𝑥,𝑘)   𝑍(𝑘)

Proof of Theorem dvfsumlem2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . . . . . . 9 𝑆 = (𝑇(,)+∞)
2 ioossre 12449 . . . . . . . . 9 (𝑇(,)+∞) ⊆ ℝ
31, 2eqsstri 3832 . . . . . . . 8 𝑆 ⊆ ℝ
4 dvfsumlem1.2 . . . . . . . 8 (𝜑𝑌𝑆)
53, 4sseldi 3796 . . . . . . 7 (𝜑𝑌 ∈ ℝ)
6 dvfsumlem1.1 . . . . . . . . . . 11 (𝜑𝑋𝑆)
76, 1syl6eleq 2895 . . . . . . . . . 10 (𝜑𝑋 ∈ (𝑇(,)+∞))
8 dvfsum.t . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ)
98rexrd 10370 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ*)
10 elioopnf 12482 . . . . . . . . . . 11 (𝑇 ∈ ℝ* → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
119, 10syl 17 . . . . . . . . . 10 (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
127, 11mpbid 223 . . . . . . . . 9 (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))
1312simpld 484 . . . . . . . 8 (𝜑𝑋 ∈ ℝ)
14 reflcl 12817 . . . . . . . 8 (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
1513, 14syl 17 . . . . . . 7 (𝜑 → (⌊‘𝑋) ∈ ℝ)
165, 15resubcld 10739 . . . . . 6 (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℝ)
17 csbeq1 3731 . . . . . . . 8 (𝑦 = 𝑌𝑦 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
1817eleq1d 2870 . . . . . . 7 (𝑦 = 𝑌 → (𝑦 / 𝑥𝐵 ∈ ℝ ↔ 𝑌 / 𝑥𝐵 ∈ ℝ))
193a1i 11 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℝ)
20 dvfsum.a . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
21 dvfsum.b1 . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝐵𝑉)
22 dvfsum.b3 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
2319, 20, 21, 22dvmptrecl 24000 . . . . . . . . 9 ((𝜑𝑥𝑆) → 𝐵 ∈ ℝ)
2423fmpttd 6603 . . . . . . . 8 (𝜑 → (𝑥𝑆𝐵):𝑆⟶ℝ)
25 nfcv 2948 . . . . . . . . . 10 𝑦𝐵
26 nfcsb1v 3744 . . . . . . . . . 10 𝑥𝑦 / 𝑥𝐵
27 csbeq1a 3737 . . . . . . . . . 10 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
2825, 26, 27cbvmpt 4943 . . . . . . . . 9 (𝑥𝑆𝐵) = (𝑦𝑆𝑦 / 𝑥𝐵)
2928fmpt 6598 . . . . . . . 8 (∀𝑦𝑆 𝑦 / 𝑥𝐵 ∈ ℝ ↔ (𝑥𝑆𝐵):𝑆⟶ℝ)
3024, 29sylibr 225 . . . . . . 7 (𝜑 → ∀𝑦𝑆 𝑦 / 𝑥𝐵 ∈ ℝ)
3118, 30, 4rspcdva 3508 . . . . . 6 (𝜑𝑌 / 𝑥𝐵 ∈ ℝ)
3216, 31remulcld 10351 . . . . 5 (𝜑 → ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℝ)
33 csbeq1 3731 . . . . . . 7 (𝑦 = 𝑌𝑦 / 𝑥𝐴 = 𝑌 / 𝑥𝐴)
3433eleq1d 2870 . . . . . 6 (𝑦 = 𝑌 → (𝑦 / 𝑥𝐴 ∈ ℝ ↔ 𝑌 / 𝑥𝐴 ∈ ℝ))
3520fmpttd 6603 . . . . . . 7 (𝜑 → (𝑥𝑆𝐴):𝑆⟶ℝ)
36 nfcv 2948 . . . . . . . . 9 𝑦𝐴
37 nfcsb1v 3744 . . . . . . . . 9 𝑥𝑦 / 𝑥𝐴
38 csbeq1a 3737 . . . . . . . . 9 (𝑥 = 𝑦𝐴 = 𝑦 / 𝑥𝐴)
3936, 37, 38cbvmpt 4943 . . . . . . . 8 (𝑥𝑆𝐴) = (𝑦𝑆𝑦 / 𝑥𝐴)
4039fmpt 6598 . . . . . . 7 (∀𝑦𝑆 𝑦 / 𝑥𝐴 ∈ ℝ ↔ (𝑥𝑆𝐴):𝑆⟶ℝ)
4135, 40sylibr 225 . . . . . 6 (𝜑 → ∀𝑦𝑆 𝑦 / 𝑥𝐴 ∈ ℝ)
4234, 41, 4rspcdva 3508 . . . . 5 (𝜑𝑌 / 𝑥𝐴 ∈ ℝ)
4332, 42resubcld 10739 . . . 4 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
4413, 15resubcld 10739 . . . . . 6 (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ)
45 csbeq1 3731 . . . . . . . 8 (𝑦 = 𝑋𝑦 / 𝑥𝐵 = 𝑋 / 𝑥𝐵)
4645eleq1d 2870 . . . . . . 7 (𝑦 = 𝑋 → (𝑦 / 𝑥𝐵 ∈ ℝ ↔ 𝑋 / 𝑥𝐵 ∈ ℝ))
4746, 30, 6rspcdva 3508 . . . . . 6 (𝜑𝑋 / 𝑥𝐵 ∈ ℝ)
4844, 47remulcld 10351 . . . . 5 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ∈ ℝ)
49 csbeq1 3731 . . . . . . 7 (𝑦 = 𝑋𝑦 / 𝑥𝐴 = 𝑋 / 𝑥𝐴)
5049eleq1d 2870 . . . . . 6 (𝑦 = 𝑋 → (𝑦 / 𝑥𝐴 ∈ ℝ ↔ 𝑋 / 𝑥𝐴 ∈ ℝ))
5150, 41, 6rspcdva 3508 . . . . 5 (𝜑𝑋 / 𝑥𝐴 ∈ ℝ)
5248, 51resubcld 10739 . . . 4 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
53 fzfid 12992 . . . . 5 (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin)
54 dvfsum.b2 . . . . . . 7 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
5554ralrimiva 3154 . . . . . 6 (𝜑 → ∀𝑥𝑍 𝐵 ∈ ℝ)
56 elfzuz 12557 . . . . . . 7 (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ𝑀))
57 dvfsum.z . . . . . . 7 𝑍 = (ℤ𝑀)
5856, 57syl6eleqr 2896 . . . . . 6 (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘𝑍)
59 dvfsum.c . . . . . . . 8 (𝑥 = 𝑘𝐵 = 𝐶)
6059eleq1d 2870 . . . . . . 7 (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
6160rspccva 3501 . . . . . 6 ((∀𝑥𝑍 𝐵 ∈ ℝ ∧ 𝑘𝑍) → 𝐶 ∈ ℝ)
6255, 58, 61syl2an 585 . . . . 5 ((𝜑𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ)
6353, 62fsumrecl 14684 . . . 4 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ)
6444, 31remulcld 10351 . . . . . 6 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℝ)
6564, 51resubcld 10739 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
665, 13resubcld 10739 . . . . . . . . 9 (𝜑 → (𝑌𝑋) ∈ ℝ)
6731, 66remulcld 10351 . . . . . . . 8 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℝ)
6831recnd 10349 . . . . . . . . . 10 (𝜑𝑌 / 𝑥𝐵 ∈ ℂ)
695recnd 10349 . . . . . . . . . 10 (𝜑𝑌 ∈ ℂ)
7013recnd 10349 . . . . . . . . . 10 (𝜑𝑋 ∈ ℂ)
7168, 69, 70subdid 10767 . . . . . . . . 9 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) = ((𝑌 / 𝑥𝐵 · 𝑌) − (𝑌 / 𝑥𝐵 · 𝑋)))
72 eqid 2806 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
7372mulcn 22880 . . . . . . . . . . 11 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
74 pnfxr 10373 . . . . . . . . . . . . . . . 16 +∞ ∈ ℝ*
7574a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → +∞ ∈ ℝ*)
7612simprd 485 . . . . . . . . . . . . . . 15 (𝜑𝑇 < 𝑋)
77 ltpnf 12166 . . . . . . . . . . . . . . . 16 (𝑌 ∈ ℝ → 𝑌 < +∞)
785, 77syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑌 < +∞)
79 iccssioo 12456 . . . . . . . . . . . . . . 15 (((𝑇 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋𝑌 < +∞)) → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞))
809, 75, 76, 78, 79syl22anc 858 . . . . . . . . . . . . . 14 (𝜑 → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞))
8180, 2syl6ss 3810 . . . . . . . . . . . . 13 (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
82 ax-resscn 10274 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
8381, 82syl6ss 3810 . . . . . . . . . . . 12 (𝜑 → (𝑋[,]𝑌) ⊆ ℂ)
8482a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ⊆ ℂ)
85 cncfmptc 22924 . . . . . . . . . . . 12 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑌 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
8631, 83, 84, 85syl3anc 1483 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑌 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
87 cncfmptid 22925 . . . . . . . . . . . 12 (((𝑋[,]𝑌) ⊆ ℝ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ))
8881, 82, 87sylancl 576 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ))
89 remulcl 10302 . . . . . . . . . . 11 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑌 / 𝑥𝐵 · 𝑦) ∈ ℝ)
9072, 73, 86, 88, 82, 89cncfmpt2ss 22928 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
91 reelprrecn 10309 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, ℂ}
9291a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ {ℝ, ℂ})
93 ioossicc 12473 . . . . . . . . . . . . . . 15 (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
9493, 81syl5ss 3809 . . . . . . . . . . . . . 14 (𝜑 → (𝑋(,)𝑌) ⊆ ℝ)
9594sselda 3798 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
9695recnd 10349 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
97 1cnd 10316 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 1 ∈ ℂ)
98 simpr 473 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
9998recnd 10349 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
100 1cnd 10316 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 1 ∈ ℂ)
10192dvmptid 23933 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
10272tgioo2 22816 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
103 iooretop 22779 . . . . . . . . . . . . . 14 (𝑋(,)𝑌) ∈ (topGen‘ran (,))
104103a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑋(,)𝑌) ∈ (topGen‘ran (,)))
10592, 99, 100, 101, 94, 102, 72, 104dvmptres 23939 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 1))
10692, 96, 97, 105, 68dvmptcmul 23940 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 1)))
10768mulid1d 10338 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐵 · 1) = 𝑌 / 𝑥𝐵)
108107mpteq2dv 4939 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑌 / 𝑥𝐵))
109106, 108eqtrd 2840 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑌 / 𝑥𝐵))
11080, 1syl6sseqr 3849 . . . . . . . . . . . 12 (𝜑 → (𝑋[,]𝑌) ⊆ 𝑆)
111110resmptd 5657 . . . . . . . . . . 11 (𝜑 → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) = (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦 / 𝑥𝐴))
11220recnd 10349 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝐴 ∈ ℂ)
113112fmpttd 6603 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝑆𝐴):𝑆⟶ℂ)
11422dmeqd 5527 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (ℝ D (𝑥𝑆𝐴)) = dom (𝑥𝑆𝐵))
11521ralrimiva 3154 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑥𝑆 𝐵𝑉)
116 dmmptg 5846 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝑆 𝐵𝑉 → dom (𝑥𝑆𝐵) = 𝑆)
117115, 116syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑥𝑆𝐵) = 𝑆)
118114, 117eqtrd 2840 . . . . . . . . . . . . . . . 16 (𝜑 → dom (ℝ D (𝑥𝑆𝐴)) = 𝑆)
119 dvcn 23897 . . . . . . . . . . . . . . . 16 (((ℝ ⊆ ℂ ∧ (𝑥𝑆𝐴):𝑆⟶ℂ ∧ 𝑆 ⊆ ℝ) ∧ dom (ℝ D (𝑥𝑆𝐴)) = 𝑆) → (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ))
12084, 113, 19, 118, 119syl31anc 1485 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ))
121 cncffvrn 22911 . . . . . . . . . . . . . . 15 ((ℝ ⊆ ℂ ∧ (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ)) → ((𝑥𝑆𝐴) ∈ (𝑆cn→ℝ) ↔ (𝑥𝑆𝐴):𝑆⟶ℝ))
12282, 120, 121sylancr 577 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥𝑆𝐴) ∈ (𝑆cn→ℝ) ↔ (𝑥𝑆𝐴):𝑆⟶ℝ))
12335, 122mpbird 248 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑆𝐴) ∈ (𝑆cn→ℝ))
12439, 123syl5eqelr 2890 . . . . . . . . . . . 12 (𝜑 → (𝑦𝑆𝑦 / 𝑥𝐴) ∈ (𝑆cn→ℝ))
125 rescncf 22910 . . . . . . . . . . . 12 ((𝑋[,]𝑌) ⊆ 𝑆 → ((𝑦𝑆𝑦 / 𝑥𝐴) ∈ (𝑆cn→ℝ) → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ)))
126110, 124, 125sylc 65 . . . . . . . . . . 11 (𝜑 → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
127111, 126eqeltrrd 2886 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦 / 𝑥𝐴) ∈ ((𝑋[,]𝑌)–cn→ℝ))
12841r19.21bi 3120 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐴 ∈ ℝ)
129128recnd 10349 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐴 ∈ ℂ)
13030r19.21bi 3120 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐵 ∈ ℝ)
13139oveq2i 6881 . . . . . . . . . . . 12 (ℝ D (𝑥𝑆𝐴)) = (ℝ D (𝑦𝑆𝑦 / 𝑥𝐴))
13222, 131, 283eqtr3g 2863 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦𝑆𝑦 / 𝑥𝐴)) = (𝑦𝑆𝑦 / 𝑥𝐵))
13393, 110syl5ss 3809 . . . . . . . . . . 11 (𝜑 → (𝑋(,)𝑌) ⊆ 𝑆)
13492, 129, 130, 132, 133, 102, 72, 104dvmptres 23939 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦 / 𝑥𝐴)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦 / 𝑥𝐵))
13593sseli 3794 . . . . . . . . . . 11 (𝑦 ∈ (𝑋(,)𝑌) → 𝑦 ∈ (𝑋[,]𝑌))
136 simpl 470 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝜑)
137110sselda 3798 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑆)
1384adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌𝑆)
139 dvfsum.d . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℝ)
140139adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ∈ ℝ)
14113adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ ℝ)
142 elicc2 12452 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌)))
14313, 5, 142syl2anc 575 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌)))
144143biimpa 464 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌))
145144simp1d 1165 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ)
146 dvfsumlem1.3 . . . . . . . . . . . . . 14 (𝜑𝐷𝑋)
147146adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷𝑋)
148144simp2d 1166 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋𝑦)
149140, 141, 145, 147, 148letrd 10475 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷𝑦)
150144simp3d 1167 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑌)
151 dvfsumlem1.5 . . . . . . . . . . . . 13 (𝜑𝑌𝑈)
152151adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌𝑈)
153 simp2r 1250 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌𝑆)
154 eleq1 2873 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑘𝑆𝑌𝑆))
155154anbi2d 616 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌 → ((𝑦𝑆𝑘𝑆) ↔ (𝑦𝑆𝑌𝑆)))
156 breq2 4848 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑦𝑘𝑦𝑌))
157 breq1 4847 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑘𝑈𝑌𝑈))
158156, 1573anbi23d 1556 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌 → ((𝐷𝑦𝑦𝑘𝑘𝑈) ↔ (𝐷𝑦𝑦𝑌𝑌𝑈)))
159155, 1583anbi23d 1556 . . . . . . . . . . . . . . 15 (𝑘 = 𝑌 → ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈))))
160 vex 3394 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ V
161160, 59csbie 3754 . . . . . . . . . . . . . . . . 17 𝑘 / 𝑥𝐵 = 𝐶
162 csbeq1 3731 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌𝑘 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
163161, 162syl5eqr 2854 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌𝐶 = 𝑌 / 𝑥𝐵)
164163breq1d 4854 . . . . . . . . . . . . . . 15 (𝑘 = 𝑌 → (𝐶𝑦 / 𝑥𝐵𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵))
165159, 164imbi12d 335 . . . . . . . . . . . . . 14 (𝑘 = 𝑌 → (((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵) ↔ ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)))
166 nfv 2005 . . . . . . . . . . . . . . . 16 𝑥(𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈))
167 nfcv 2948 . . . . . . . . . . . . . . . . 17 𝑥𝐶
168 nfcv 2948 . . . . . . . . . . . . . . . . 17 𝑥
169167, 168, 26nfbr 4891 . . . . . . . . . . . . . . . 16 𝑥 𝐶𝑦 / 𝑥𝐵
170166, 169nfim 1987 . . . . . . . . . . . . . . 15 𝑥((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)
171 eleq1 2873 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑆𝑦𝑆))
172171anbi1d 617 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑥𝑆𝑘𝑆) ↔ (𝑦𝑆𝑘𝑆)))
173 breq2 4848 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐷𝑥𝐷𝑦))
174 breq1 4847 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑘𝑦𝑘))
175173, 1743anbi12d 1554 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐷𝑥𝑥𝑘𝑘𝑈) ↔ (𝐷𝑦𝑦𝑘𝑘𝑈)))
176172, 1753anbi23d 1556 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈))))
17727breq2d 4856 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝐶𝐵𝐶𝑦 / 𝑥𝐵))
178176, 177imbi12d 335 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵) ↔ ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)))
179 dvfsum.l . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵)
180170, 178, 179chvar 2436 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)
181165, 180vtoclg 3459 . . . . . . . . . . . . 13 (𝑌𝑆 → ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵))
182153, 181mpcom 38 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
183136, 137, 138, 149, 150, 152, 182syl123anc 1499 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
184135, 183sylan2 582 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
18513rexrd 10370 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℝ*)
1865rexrd 10370 . . . . . . . . . . 11 (𝜑𝑌 ∈ ℝ*)
187 dvfsumlem1.4 . . . . . . . . . . 11 (𝜑𝑋𝑌)
188 lbicc2 12504 . . . . . . . . . . 11 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*𝑋𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
189185, 186, 187, 188syl3anc 1483 . . . . . . . . . 10 (𝜑𝑋 ∈ (𝑋[,]𝑌))
190 ubicc2 12505 . . . . . . . . . . 11 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*𝑋𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
191185, 186, 187, 190syl3anc 1483 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑋[,]𝑌))
192 oveq2 6878 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵 · 𝑋))
193 oveq2 6878 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵 · 𝑌))
19413, 5, 90, 109, 127, 134, 184, 189, 191, 187, 192, 49, 193, 33dvle 23983 . . . . . . . . 9 (𝜑 → ((𝑌 / 𝑥𝐵 · 𝑌) − (𝑌 / 𝑥𝐵 · 𝑋)) ≤ (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴))
19571, 194eqbrtrd 4866 . . . . . . . 8 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ≤ (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴))
19667, 42, 51, 195lesubd 10912 . . . . . . 7 (𝜑𝑋 / 𝑥𝐴 ≤ (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
19764recnd 10349 . . . . . . . . 9 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℂ)
19832recnd 10349 . . . . . . . . 9 (𝜑 → ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℂ)
19942recnd 10349 . . . . . . . . 9 (𝜑𝑌 / 𝑥𝐴 ∈ ℂ)
200197, 198, 199subsubd 10701 . . . . . . . 8 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴))
201198, 197negsubdi2d 10689 . . . . . . . . . . 11 (𝜑 → -(((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)))
20215recnd 10349 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘𝑋) ∈ ℂ)
20369, 70, 202nnncan2d 10708 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) = (𝑌𝑋))
204203oveq1d 6885 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · 𝑌 / 𝑥𝐵) = ((𝑌𝑋) · 𝑌 / 𝑥𝐵))
20516recnd 10349 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℂ)
20644recnd 10349 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ)
207205, 206, 68subdird 10768 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)))
20866recnd 10349 . . . . . . . . . . . . . 14 (𝜑 → (𝑌𝑋) ∈ ℂ)
209208, 68mulcomd 10342 . . . . . . . . . . . . 13 (𝜑 → ((𝑌𝑋) · 𝑌 / 𝑥𝐵) = (𝑌 / 𝑥𝐵 · (𝑌𝑋)))
210204, 207, 2093eqtr3d 2848 . . . . . . . . . . . 12 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = (𝑌 / 𝑥𝐵 · (𝑌𝑋)))
211210negeqd 10556 . . . . . . . . . . 11 (𝜑 → -(((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = -(𝑌 / 𝑥𝐵 · (𝑌𝑋)))
212201, 211eqtr3d 2842 . . . . . . . . . 10 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = -(𝑌 / 𝑥𝐵 · (𝑌𝑋)))
213212oveq1d 6885 . . . . . . . . 9 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = (-(𝑌 / 𝑥𝐵 · (𝑌𝑋)) + 𝑌 / 𝑥𝐴))
21467recnd 10349 . . . . . . . . . 10 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℂ)
215214, 199negsubdid 10688 . . . . . . . . 9 (𝜑 → -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴) = (-(𝑌 / 𝑥𝐵 · (𝑌𝑋)) + 𝑌 / 𝑥𝐴))
216213, 215eqtr4d 2843 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴))
217214, 199negsubdi2d 10689 . . . . . . . 8 (𝜑 → -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴) = (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
218200, 216, 2173eqtrd 2844 . . . . . . 7 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
219196, 218breqtrrd 4872 . . . . . 6 (𝜑𝑋 / 𝑥𝐴 ≤ (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)))
22051, 64, 43, 219lesubd 10912 . . . . 5 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
221 flle 12820 . . . . . . . . 9 (𝑋 ∈ ℝ → (⌊‘𝑋) ≤ 𝑋)
22213, 221syl 17 . . . . . . . 8 (𝜑 → (⌊‘𝑋) ≤ 𝑋)
22313, 15subge0d 10898 . . . . . . . 8 (𝜑 → (0 ≤ (𝑋 − (⌊‘𝑋)) ↔ (⌊‘𝑋) ≤ 𝑋))
224222, 223mpbird 248 . . . . . . 7 (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋)))
22545breq2d 4856 . . . . . . . 8 (𝑦 = 𝑋 → (𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵𝑌 / 𝑥𝐵𝑋 / 𝑥𝐵))
226183ralrimiva 3154 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
227225, 226, 189rspcdva 3508 . . . . . . 7 (𝜑𝑌 / 𝑥𝐵𝑋 / 𝑥𝐵)
22831, 47, 44, 224, 227lemul2ad 11245 . . . . . 6 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ≤ ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵))
22964, 48, 51, 228lesub1dd 10924 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
23043, 65, 52, 220, 229letrd 10475 . . . 4 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
23143, 52, 63, 230leadd1dd 10922 . . 3 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
232 dvfsum.m . . . 4 (𝜑𝑀 ∈ ℤ)
233 dvfsum.md . . . 4 (𝜑𝑀 ≤ (𝐷 + 1))
234 dvfsum.u . . . 4 (𝜑𝑈 ∈ ℝ*)
235 dvfsum.h . . . 4 𝐻 = (𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴)))
236 dvfsumlem1.6 . . . 4 (𝜑𝑌 ≤ ((⌊‘𝑋) + 1))
2371, 57, 232, 139, 233, 8, 20, 21, 54, 22, 59, 234, 179, 235, 6, 4, 146, 187, 151, 236dvfsumlem1 24002 . . 3 (𝜑 → (𝐻𝑌) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
23813leidd 10875 . . . 4 (𝜑𝑋𝑋)
239185, 186, 234, 187, 151xrletrd 12207 . . . 4 (𝜑𝑋𝑈)
240 fllep1 12822 . . . . 5 (𝑋 ∈ ℝ → 𝑋 ≤ ((⌊‘𝑋) + 1))
24113, 240syl 17 . . . 4 (𝜑𝑋 ≤ ((⌊‘𝑋) + 1))
2421, 57, 232, 139, 233, 8, 20, 21, 54, 22, 59, 234, 179, 235, 6, 6, 146, 238, 239, 241dvfsumlem1 24002 . . 3 (𝜑 → (𝐻𝑋) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
243231, 237, 2423brtr4d 4876 . 2 (𝜑 → (𝐻𝑌) ≤ (𝐻𝑋))
24452, 47resubcld 10739 . . . . 5 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) ∈ ℝ)
24543, 31resubcld 10739 . . . . 5 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) ∈ ℝ)
246 peano2rem 10629 . . . . . . . . . . 11 ((𝑋 − (⌊‘𝑋)) ∈ ℝ → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℝ)
24744, 246syl 17 . . . . . . . . . 10 (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℝ)
248247, 47remulcld 10351 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℝ)
249248, 51resubcld 10739 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
250 peano2rem 10629 . . . . . . . . . . 11 ((𝑌 − (⌊‘𝑋)) ∈ ℝ → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
25116, 250syl 17 . . . . . . . . . 10 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
252251, 47remulcld 10351 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℝ)
253252, 42resubcld 10739 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
254251, 31remulcld 10351 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ∈ ℝ)
255254, 42resubcld 10739 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
256248recnd 10349 . . . . . . . . . . . . . 14 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℂ)
257252recnd 10349 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℂ)
258256, 257subcld 10673 . . . . . . . . . . . . 13 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) ∈ ℂ)
259258, 199addcomd 10519 . . . . . . . . . . . 12 (𝜑 → (((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = (𝑌 / 𝑥𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
260256, 257, 199subsubd 10701 . . . . . . . . . . . 12 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴))
261199, 257, 256subsub2d 10702 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))) = (𝑌 / 𝑥𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
262259, 260, 2613eqtr4d 2850 . . . . . . . . . . 11 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
263 1cnd 10316 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℂ)
264205, 206, 263nnncan2d 10708 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))))
265264, 203eqtrd 2840 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = (𝑌𝑋))
266265oveq1d 6885 . . . . . . . . . . . . 13 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · 𝑋 / 𝑥𝐵) = ((𝑌𝑋) · 𝑋 / 𝑥𝐵))
267251recnd 10349 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℂ)
268247recnd 10349 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℂ)
26947recnd 10349 . . . . . . . . . . . . . 14 (𝜑𝑋 / 𝑥𝐵 ∈ ℂ)
270267, 268, 269subdird 10768 . . . . . . . . . . . . 13 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · 𝑋 / 𝑥𝐵) = ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)))
271208, 269mulcomd 10342 . . . . . . . . . . . . 13 (𝜑 → ((𝑌𝑋) · 𝑋 / 𝑥𝐵) = (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
272266, 270, 2713eqtr3d 2848 . . . . . . . . . . . 12 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) = (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
273272oveq2d 6886 . . . . . . . . . . 11 (𝜑 → (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))) = (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))))
274262, 273eqtrd 2840 . . . . . . . . . 10 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))))
27547, 66remulcld 10351 . . . . . . . . . . 11 (𝜑 → (𝑋 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℝ)
276 cncfmptc 22924 . . . . . . . . . . . . . . 15 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑋 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
27747, 83, 84, 276syl3anc 1483 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑋 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
278 remulcl 10302 . . . . . . . . . . . . . 14 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 / 𝑥𝐵 · 𝑦) ∈ ℝ)
27972, 73, 277, 88, 82, 278cncfmpt2ss 22928 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
28092, 96, 97, 105, 269dvmptcmul 23940 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 1)))
281269mulid1d 10338 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋 / 𝑥𝐵 · 1) = 𝑋 / 𝑥𝐵)
282281mpteq2dv 4939 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑋 / 𝑥𝐵))
283280, 282eqtrd 2840 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑋 / 𝑥𝐵))
2846adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋𝑆)
285145rexrd 10370 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ*)
286186adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈ ℝ*)
287234adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑈 ∈ ℝ*)
288285, 286, 287, 150, 152xrletrd 12207 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑈)
289 vex 3394 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
290 eleq1 2873 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑘𝑆𝑦𝑆))
291290anbi2d 616 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → ((𝑋𝑆𝑘𝑆) ↔ (𝑋𝑆𝑦𝑆)))
292 breq2 4848 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑋𝑘𝑋𝑦))
293 breq1 4847 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑘𝑈𝑦𝑈))
294292, 2933anbi23d 1556 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → ((𝐷𝑋𝑋𝑘𝑘𝑈) ↔ (𝐷𝑋𝑋𝑦𝑦𝑈)))
295291, 2943anbi23d 1556 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈))))
296 csbeq1 3731 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦𝑘 / 𝑥𝐵 = 𝑦 / 𝑥𝐵)
297161, 296syl5eqr 2854 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦𝐶 = 𝑦 / 𝑥𝐵)
298297breq1d 4854 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → (𝐶𝑋 / 𝑥𝐵𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵))
299295, 298imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → (((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵) ↔ ((𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)))
300 simp2l 1249 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝑋𝑆)
301 nfv 2005 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈))
302 nfcsb1v 3744 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑋 / 𝑥𝐵
303167, 168, 302nfbr 4891 . . . . . . . . . . . . . . . . . . 19 𝑥 𝐶𝑋 / 𝑥𝐵
304301, 303nfim 1987 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)
305 eleq1 2873 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝑥𝑆𝑋𝑆))
306305anbi1d 617 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝑥𝑆𝑘𝑆) ↔ (𝑋𝑆𝑘𝑆)))
307 breq2 4848 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝐷𝑥𝐷𝑋))
308 breq1 4847 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝑥𝑘𝑋𝑘))
309307, 3083anbi12d 1554 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝐷𝑥𝑥𝑘𝑘𝑈) ↔ (𝐷𝑋𝑋𝑘𝑘𝑈)))
310306, 3093anbi23d 1556 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈))))
311 csbeq1a 3737 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋𝐵 = 𝑋 / 𝑥𝐵)
312311breq2d 4856 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (𝐶𝐵𝐶𝑋 / 𝑥𝐵))
313310, 312imbi12d 335 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵) ↔ ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)))
314304, 313, 179vtoclg1f 3458 . . . . . . . . . . . . . . . . 17 (𝑋𝑆 → ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵))
315300, 314mpcom 38 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)
316289, 299, 315vtocl 3452 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
317136, 284, 137, 147, 148, 288, 316syl123anc 1499 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
318135, 317sylan2 582 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
319 oveq2 6878 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵 · 𝑋))
320 oveq2 6878 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵 · 𝑌))
32113, 5, 127, 134, 279, 283, 318, 189, 191, 187, 49, 319, 33, 320dvle 23983 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴) ≤ ((𝑋 / 𝑥𝐵 · 𝑌) − (𝑋 / 𝑥𝐵 · 𝑋)))
322269, 69, 70subdid 10767 . . . . . . . . . . . 12 (𝜑 → (𝑋 / 𝑥𝐵 · (𝑌𝑋)) = ((𝑋 / 𝑥𝐵 · 𝑌) − (𝑋 / 𝑥𝐵 · 𝑋)))
323321, 322breqtrrd 4872 . . . . . . . . . . 11 (𝜑 → (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴) ≤ (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
32442, 51, 275, 323subled 10911 . . . . . . . . . 10 (𝜑 → (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))) ≤ 𝑋 / 𝑥𝐴)
325274, 324eqbrtrd 4866 . . . . . . . . 9 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) ≤ 𝑋 / 𝑥𝐴)
326248, 253, 51, 325subled 10911 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
327251renegcld 10738 . . . . . . . . . . . 12 (𝜑 → -((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
328 1red 10322 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
3295, 15, 328lesubadd2d 10907 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (⌊‘𝑋)) ≤ 1 ↔ 𝑌 ≤ ((⌊‘𝑋) + 1)))
330236, 329mpbird 248 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 − (⌊‘𝑋)) ≤ 1)
33116, 328suble0d 10899 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ (𝑌 − (⌊‘𝑋)) ≤ 1))
332330, 331mpbird 248 . . . . . . . . . . . . 13 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ≤ 0)
333251le0neg1d 10880 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1)))
334332, 333mpbid 223 . . . . . . . . . . . 12 (𝜑 → 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1))
33531, 47, 327, 334, 227lemul2ad 11245 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
336267, 68mulneg1d 10764 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵))
337267, 269mulneg1d 10764 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
338335, 336, 3373brtr3d 4875 . . . . . . . . . 10 (𝜑 → -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
339252, 254lenegd 10887 . . . . . . . . . 10 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ↔ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)))
340338, 339mpbird 248 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵))
341252, 254, 42, 340lesub1dd 10924 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
342249, 253, 255, 326, 341letrd 10475 . . . . . . 7 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
343206, 263, 269subdird 10768 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − (1 · 𝑋 / 𝑥𝐵)))
344269mulid2d 10339 . . . . . . . . . 10 (𝜑 → (1 · 𝑋 / 𝑥𝐵) = 𝑋 / 𝑥𝐵)
345344oveq2d 6886 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − (1 · 𝑋 / 𝑥𝐵)) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵))
346343, 345eqtrd 2840 . . . . . . . 8 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵))
347346oveq1d 6885 . . . . . . 7 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
348205, 263, 68subdird 10768 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (1 · 𝑌 / 𝑥𝐵)))
34968mulid2d 10339 . . . . . . . . . 10 (𝜑 → (1 · 𝑌 / 𝑥𝐵) = 𝑌 / 𝑥𝐵)
350349oveq2d 6886 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (1 · 𝑌 / 𝑥𝐵)) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵))
351348, 350eqtrd 2840 . . . . . . . 8 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵))
352351oveq1d 6885 . . . . . . 7 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
353342, 347, 3523brtr3d 4875 . . . . . 6 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
35448recnd 10349 . . . . . . 7 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ∈ ℂ)
35551recnd 10349 . . . . . . 7 (𝜑𝑋 / 𝑥𝐴 ∈ ℂ)
356354, 355, 269sub32d 10705 . . . . . 6 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
357198, 199, 68sub32d 10705 . . . . . 6 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
358353, 356, 3573brtr4d 4876 . . . . 5 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) ≤ ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵))
359244, 245, 63, 358leadd1dd 10922 . . . 4 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
36052recnd 10349 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℂ)
36163recnd 10349 . . . . 5 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ)
362360, 361, 269addsubd 10694 . . . 4 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵) = (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
36343recnd 10349 . . . . 5 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℂ)
364363, 361, 68addsubd 10694 . . . 4 (𝜑 → (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵) = (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
365359, 362, 3643brtr4d 4876 . . 3 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵) ≤ (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵))
366242oveq1d 6885 . . 3 (𝜑 → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) = (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵))
367237oveq1d 6885 . . 3 (𝜑 → ((𝐻𝑌) − 𝑌 / 𝑥𝐵) = (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵))
368365, 366, 3673brtr4d 4876 . 2 (𝜑 → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵))
369243, 368jca 503 1 (𝜑 → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wral 3096  csb 3728  wss 3769  {cpr 4372   class class class wbr 4844  cmpt 4923  dom cdm 5311  ran crn 5312  cres 5313  wf 6093  cfv 6097  (class class class)co 6870  cc 10215  cr 10216  0cc0 10217  1c1 10218   + caddc 10220   · cmul 10222  +∞cpnf 10352  *cxr 10354   < clt 10355  cle 10356  cmin 10547  -cneg 10548  cz 11639  cuz 11900  (,)cioo 12389  [,]cicc 12392  ...cfz 12545  cfl 12811  Σcsu 14635  TopOpenctopn 16283  topGenctg 16299  fldccnfld 19950  cnccncf 22889   D cdv 23840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295  ax-addf 10296  ax-mulf 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-of 7123  df-om 7292  df-1st 7394  df-2nd 7395  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-2o 7793  df-oadd 7796  df-er 7975  df-map 8090  df-pm 8091  df-ixp 8142  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-fsupp 8511  df-fi 8552  df-sup 8583  df-inf 8584  df-oi 8650  df-card 9044  df-cda 9271  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-q 12004  df-rp 12043  df-xneg 12158  df-xadd 12159  df-xmul 12160  df-ioo 12393  df-ico 12395  df-icc 12396  df-fz 12546  df-fzo 12686  df-fl 12813  df-seq 13021  df-exp 13080  df-hash 13334  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438  df-sum 14636  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16284  df-topn 16285  df-0g 16303  df-gsum 16304  df-topgen 16305  df-pt 16306  df-prds 16309  df-xrs 16363  df-qtop 16368  df-imas 16369  df-xps 16371  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17947  df-cmn 18392  df-psmet 19942  df-xmet 19943  df-met 19944  df-bl 19945  df-mopn 19946  df-fbas 19947  df-fg 19948  df-cnfld 19951  df-top 20909  df-topon 20926  df-topsp 20948  df-bases 20961  df-cld 21034  df-ntr 21035  df-cls 21036  df-nei 21113  df-lp 21151  df-perf 21152  df-cn 21242  df-cnp 21243  df-haus 21330  df-cmp 21401  df-tx 21576  df-hmeo 21769  df-fil 21860  df-fm 21952  df-flim 21953  df-flf 21954  df-xms 22335  df-ms 22336  df-tms 22337  df-cncf 22891  df-limc 23843  df-dv 23844
This theorem is referenced by:  dvfsumlem3  24004
  Copyright terms: Public domain W3C validator