![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dvfsumrlimge0 | Structured version Visualization version GIF version |
Description: Lemma for dvfsumrlim 25783. Satisfy the assumption of dvfsumlem4 25781. (Contributed by Mario Carneiro, 18-May-2016.) |
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 | ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
dvfsumrlim.l | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵) |
dvfsumrlim.g | ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) |
dvfsumrlim.k | ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0) |
Ref | Expression |
---|---|
dvfsumrlimge0 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvfsum.s | . . . . . 6 ⊢ 𝑆 = (𝑇(,)+∞) | |
2 | ioossre 13389 | . . . . . 6 ⊢ (𝑇(,)+∞) ⊆ ℝ | |
3 | 1, 2 | eqsstri 4015 | . . . . 5 ⊢ 𝑆 ⊆ ℝ |
4 | simprl 767 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝑥 ∈ 𝑆) | |
5 | 3, 4 | sselid 3979 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
6 | 5 | rexrd 11268 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝑥 ∈ ℝ*) |
7 | 5 | renepnfd 11269 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝑥 ≠ +∞) |
8 | icopnfsup 13834 | . . 3 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑥 ≠ +∞) → sup((𝑥[,)+∞), ℝ*, < ) = +∞) | |
9 | 6, 7, 8 | syl2anc 582 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → sup((𝑥[,)+∞), ℝ*, < ) = +∞) |
10 | dvfsum.t | . . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ℝ) | |
11 | 10 | rexrd 11268 | . . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℝ*) |
12 | 4, 1 | eleqtrdi 2841 | . . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝑥 ∈ (𝑇(,)+∞)) |
13 | 11 | adantr 479 | . . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝑇 ∈ ℝ*) |
14 | elioopnf 13424 | . . . . . . . 8 ⊢ (𝑇 ∈ ℝ* → (𝑥 ∈ (𝑇(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑇 < 𝑥))) | |
15 | 13, 14 | syl 17 | . . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑥 ∈ (𝑇(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑇 < 𝑥))) |
16 | 12, 15 | mpbid 231 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 𝑇 < 𝑥)) |
17 | 16 | simprd 494 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝑇 < 𝑥) |
18 | df-ioo 13332 | . . . . . 6 ⊢ (,) = (𝑢 ∈ ℝ*, 𝑣 ∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤 ∧ 𝑤 < 𝑣)}) | |
19 | df-ico 13334 | . . . . . 6 ⊢ [,) = (𝑢 ∈ ℝ*, 𝑣 ∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 ≤ 𝑤 ∧ 𝑤 < 𝑣)}) | |
20 | xrltletr 13140 | . . . . . 6 ⊢ ((𝑇 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → ((𝑇 < 𝑥 ∧ 𝑥 ≤ 𝑧) → 𝑇 < 𝑧)) | |
21 | 18, 19, 20 | ixxss1 13346 | . . . . 5 ⊢ ((𝑇 ∈ ℝ* ∧ 𝑇 < 𝑥) → (𝑥[,)+∞) ⊆ (𝑇(,)+∞)) |
22 | 11, 17, 21 | syl2an2r 681 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑥[,)+∞) ⊆ (𝑇(,)+∞)) |
23 | 22, 1 | sseqtrrdi 4032 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑥[,)+∞) ⊆ 𝑆) |
24 | dvfsum.c | . . . . 5 ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) | |
25 | 24 | cbvmptv 5260 | . . . 4 ⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑘 ∈ 𝑆 ↦ 𝐶) |
26 | dvfsumrlim.k | . . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0) | |
27 | 26 | adantr 479 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0) |
28 | 25, 27 | eqbrtrrid 5183 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑘 ∈ 𝑆 ↦ 𝐶) ⇝𝑟 0) |
29 | 23, 28 | rlimres2 15509 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑘 ∈ (𝑥[,)+∞) ↦ 𝐶) ⇝𝑟 0) |
30 | 3 | a1i 11 | . . . 4 ⊢ (𝜑 → 𝑆 ⊆ ℝ) |
31 | dvfsum.a | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) | |
32 | dvfsum.b1 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) | |
33 | dvfsum.b3 | . . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) | |
34 | 30, 31, 32, 33 | dvmptrecl 25776 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
35 | 34 | adantrr 713 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝐵 ∈ ℝ) |
36 | 35 | recnd 11246 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝐵 ∈ ℂ) |
37 | rlimconst 15492 | . . . 4 ⊢ ((𝑆 ⊆ ℝ ∧ 𝐵 ∈ ℂ) → (𝑘 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 𝐵) | |
38 | 30, 36, 37 | syl2an2r 681 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑘 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 𝐵) |
39 | 23, 38 | rlimres2 15509 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑘 ∈ (𝑥[,)+∞) ↦ 𝐵) ⇝𝑟 𝐵) |
40 | 34 | ralrimiva 3144 | . . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ) |
41 | 40 | adantr 479 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ) |
42 | 23 | sselda 3981 | . . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑘 ∈ (𝑥[,)+∞)) → 𝑘 ∈ 𝑆) |
43 | 24 | eleq1d 2816 | . . . 4 ⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
44 | 43 | rspccva 3610 | . . 3 ⊢ ((∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑆) → 𝐶 ∈ ℝ) |
45 | 41, 42, 44 | syl2an2r 681 | . 2 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑘 ∈ (𝑥[,)+∞)) → 𝐶 ∈ ℝ) |
46 | 35 | adantr 479 | . 2 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑘 ∈ (𝑥[,)+∞)) → 𝐵 ∈ ℝ) |
47 | simpll 763 | . . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑘 ∈ (𝑥[,)+∞)) → 𝜑) | |
48 | simplrl 773 | . . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑘 ∈ (𝑥[,)+∞)) → 𝑥 ∈ 𝑆) | |
49 | simplrr 774 | . . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑘 ∈ (𝑥[,)+∞)) → 𝐷 ≤ 𝑥) | |
50 | elicopnf 13426 | . . . . 5 ⊢ (𝑥 ∈ ℝ → (𝑘 ∈ (𝑥[,)+∞) ↔ (𝑘 ∈ ℝ ∧ 𝑥 ≤ 𝑘))) | |
51 | 5, 50 | syl 17 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → (𝑘 ∈ (𝑥[,)+∞) ↔ (𝑘 ∈ ℝ ∧ 𝑥 ≤ 𝑘))) |
52 | 51 | simplbda 498 | . . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑘 ∈ (𝑥[,)+∞)) → 𝑥 ≤ 𝑘) |
53 | dvfsumrlim.l | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵) | |
54 | 47, 48, 42, 49, 52, 53 | syl122anc 1377 | . 2 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑘 ∈ (𝑥[,)+∞)) → 𝐶 ≤ 𝐵) |
55 | 9, 29, 39, 45, 46, 54 | rlimle 15598 | 1 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ⊆ wss 3947 class class class wbr 5147 ↦ cmpt 5230 ‘cfv 6542 (class class class)co 7411 supcsup 9437 ℂcc 11110 ℝcr 11111 0cc0 11112 1c1 11113 + caddc 11115 +∞cpnf 11249 ℝ*cxr 11251 < clt 11252 ≤ cle 11253 − cmin 11448 ℤcz 12562 ℤ≥cuz 12826 (,)cioo 13328 [,)cico 13330 ...cfz 13488 ⌊cfl 13759 ⇝𝑟 crli 15433 Σcsu 15636 D cdv 25612 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-map 8824 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fi 9408 df-sup 9439 df-inf 9440 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-z 12563 df-dec 12682 df-uz 12827 df-q 12937 df-rp 12979 df-xneg 13096 df-xadd 13097 df-xmul 13098 df-ioo 13332 df-ico 13334 df-icc 13335 df-fz 13489 df-seq 13971 df-exp 14032 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-rlim 15437 df-struct 17084 df-slot 17119 df-ndx 17131 df-base 17149 df-plusg 17214 df-mulr 17215 df-starv 17216 df-tset 17220 df-ple 17221 df-ds 17223 df-unif 17224 df-rest 17372 df-topn 17373 df-topgen 17393 df-psmet 21136 df-xmet 21137 df-met 21138 df-bl 21139 df-mopn 21140 df-fbas 21141 df-fg 21142 df-cnfld 21145 df-top 22616 df-topon 22633 df-topsp 22655 df-bases 22669 df-cld 22743 df-ntr 22744 df-cls 22745 df-nei 22822 df-lp 22860 df-perf 22861 df-cn 22951 df-cnp 22952 df-haus 23039 df-fil 23570 df-fm 23662 df-flim 23663 df-flf 23664 df-xms 24046 df-ms 24047 df-cncf 24618 df-limc 25615 df-dv 25616 |
This theorem is referenced by: dvfsumrlim 25783 dvfsumrlim2 25784 |
Copyright terms: Public domain | W3C validator |