Metamath Proof Explorer

Theorem dvfsumrlimge0

Description: Lemma for dvfsumrlim . Satisfy the assumption of dvfsumlem4 . (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvfsum.s ⊢ 𝑆 = ( 𝑇 (,) +∞ )
dvfsum.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
dvfsum.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
dvfsum.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
dvfsum.md ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
dvfsum.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
dvfsum.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
dvfsum.b1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
dvfsum.b2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
dvfsum.b3 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
dvfsum.c ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
dvfsumrlim.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) ) → 𝐶 ≤ 𝐵 )
dvfsumrlim.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
dvfsumrlim.k ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 )
Assertion dvfsumrlimge0 ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 0 ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 dvfsum.s ⊢ 𝑆 = ( 𝑇 (,) +∞ )
2 dvfsum.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 dvfsum.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 dvfsum.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5 dvfsum.md ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
6 dvfsum.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
7 dvfsum.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
8 dvfsum.b1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
9 dvfsum.b2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
10 dvfsum.b3 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
11 dvfsum.c ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
12 dvfsumrlim.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) ) → 𝐶 ≤ 𝐵 )
13 dvfsumrlim.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
14 dvfsumrlim.k ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 )
15 ioossre ⊢ ( 𝑇 (,) +∞ ) ⊆ ℝ
16 1 15 eqsstri ⊢ 𝑆 ⊆ ℝ
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑥 ∈ 𝑆 )
18 16 17 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
19 18 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ* )
20 18 renepnfd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑥 ≠ +∞ )
21 icopnfsup ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ +∞ ) → sup ( ( 𝑥 [,) +∞ ) , ℝ* , < ) = +∞ )
22 19 20 21 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → sup ( ( 𝑥 [,) +∞ ) , ℝ* , < ) = +∞ )
23 6 rexrd ⊢ ( 𝜑 → 𝑇 ∈ ℝ* )
24 17 1 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑥 ∈ ( 𝑇 (,) +∞ ) )
25 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑇 ∈ ℝ* )
26 elioopnf ⊢ ( 𝑇 ∈ ℝ* → ( 𝑥 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑇 < 𝑥 ) ) )
27 25 26 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑇 < 𝑥 ) ) )
28 24 27 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 𝑇 < 𝑥 ) )
29 28 simprd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝑇 < 𝑥 )
30 df-ioo ⊢ (,) = ( 𝑢 ∈ ℝ* , 𝑣 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑢 < 𝑤 ∧ 𝑤 < 𝑣 ) } )
31 df-ico ⊢ [,) = ( 𝑢 ∈ ℝ* , 𝑣 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑢 ≤ 𝑤 ∧ 𝑤 < 𝑣 ) } )
32 xrltletr ⊢ ( ( 𝑇 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑇 < 𝑥 ∧ 𝑥 ≤ 𝑧 ) → 𝑇 < 𝑧 ) )
33 30 31 32 ixxss1 ⊢ ( ( 𝑇 ∈ ℝ* ∧ 𝑇 < 𝑥 ) → ( 𝑥 [,) +∞ ) ⊆ ( 𝑇 (,) +∞ ) )
34 23 29 33 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 [,) +∞ ) ⊆ ( 𝑇 (,) +∞ ) )
35 34 1 sseqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 [,) +∞ ) ⊆ 𝑆 )
36 11 cbvmptv ⊢ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑆 ↦ 𝐶 )
37 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 )
38 36 37 eqbrtrrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑘 ∈ 𝑆 ↦ 𝐶 ) ⇝𝑟 0 )
39 35 38 rlimres2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑘 ∈ ( 𝑥 [,) +∞ ) ↦ 𝐶 ) ⇝𝑟 0 )
40 16 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
41 40 7 8 10 dvmptrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
42 41 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 ∈ ℝ )
43 42 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 ∈ ℂ )
44 rlimconst ⊢ ( ( 𝑆 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑘 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 𝐵 )
45 40 43 44 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑘 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 𝐵 )
46 35 45 rlimres2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑘 ∈ ( 𝑥 [,) +∞ ) ↦ 𝐵 ) ⇝𝑟 𝐵 )
47 41 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ )
49 35 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑥 [,) +∞ ) ) → 𝑘 ∈ 𝑆 )
50 11 eleq1d ⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
51 50 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑆 ) → 𝐶 ∈ ℝ )
52 48 49 51 syl2an2r ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑥 [,) +∞ ) ) → 𝐶 ∈ ℝ )
53 42 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑥 [,) +∞ ) ) → 𝐵 ∈ ℝ )
54 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑥 [,) +∞ ) ) → 𝜑 )
55 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑥 [,) +∞ ) ) → 𝑥 ∈ 𝑆 )
56 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑥 [,) +∞ ) ) → 𝐷 ≤ 𝑥 )
57 elicopnf ⊢ ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑘 ∈ ℝ ∧ 𝑥 ≤ 𝑘 ) ) )
58 18 57 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → ( 𝑘 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑘 ∈ ℝ ∧ 𝑥 ≤ 𝑘 ) ) )
59 58 simplbda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑥 [,) +∞ ) ) → 𝑥 ≤ 𝑘 )
60 54 55 49 56 59 12 syl122anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑥 [,) +∞ ) ) → 𝐶 ≤ 𝐵 )
61 22 39 46 52 53 60 rlimle ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 0 ≤ 𝐵 )