Mathbox for Brendan Leahy |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > itggt0cn | Structured version Visualization version GIF version |
Description: itggt0 25113 holds for continuous functions in the absence of ax-cc 10296. (Contributed by Brendan Leahy, 16-Nov-2017.) |
Ref | Expression |
---|---|
itggt0cn.1 | ⊢ (𝜑 → 𝑋 < 𝑌) |
itggt0cn.2 | ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1) |
itggt0cn.3 | ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℝ+) |
itggt0cn.cn | ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
Ref | Expression |
---|---|
itggt0cn | ⊢ (𝜑 → 0 < ∫(𝑋(,)𝑌)𝐵 d𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | itggt0cn.1 | . . 3 ⊢ (𝜑 → 𝑋 < 𝑌) | |
2 | itggt0cn.3 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℝ+) | |
3 | 2 | rpred 12877 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℝ) |
4 | 2 | rpge0d 12881 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 ≤ 𝐵) |
5 | elrege0 13291 | . . . . . . 7 ⊢ (𝐵 ∈ (0[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) | |
6 | 3, 4, 5 | sylanbrc 584 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ (0[,)+∞)) |
7 | 0e0icopnf 13295 | . . . . . . 7 ⊢ 0 ∈ (0[,)+∞) | |
8 | 7 | a1i 11 | . . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ (𝑋(,)𝑌)) → 0 ∈ (0[,)+∞)) |
9 | 6, 8 | ifclda 4512 | . . . . 5 ⊢ (𝜑 → if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0) ∈ (0[,)+∞)) |
10 | 9 | adantr 482 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0) ∈ (0[,)+∞)) |
11 | 10 | fmpttd 7049 | . . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)):ℝ⟶(0[,)+∞)) |
12 | 2 | rpgt0d 12880 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < 𝐵) |
13 | elioore 13214 | . . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ) | |
14 | 13 | adantl 483 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑥 ∈ ℝ) |
15 | iftrue 4483 | . . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0) = 𝐵) | |
16 | 15 | adantl 483 | . . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0) = 𝐵) |
17 | 16, 2 | eqeltrd 2838 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0) ∈ ℝ+) |
18 | eqid 2737 | . . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) | |
19 | 18 | fvmpt2 6946 | . . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0) ∈ ℝ+) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥) = if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) |
20 | 14, 17, 19 | syl2anc 585 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥) = if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) |
21 | 20, 16 | eqtrd 2777 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥) = 𝐵) |
22 | 12, 21 | breqtrrd 5124 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥)) |
23 | 22 | ralrimiva 3140 | . . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥)) |
24 | nfcv 2905 | . . . . . . 7 ⊢ Ⅎ𝑥0 | |
25 | nfcv 2905 | . . . . . . 7 ⊢ Ⅎ𝑥 < | |
26 | nffvmpt1 6840 | . . . . . . 7 ⊢ Ⅎ𝑥((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑦) | |
27 | 24, 25, 26 | nfbr 5143 | . . . . . 6 ⊢ Ⅎ𝑥0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑦) |
28 | nfv 1917 | . . . . . 6 ⊢ Ⅎ𝑦0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥) | |
29 | fveq2 6829 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥)) | |
30 | 29 | breq2d 5108 | . . . . . 6 ⊢ (𝑦 = 𝑥 → (0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑦) ↔ 0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥))) |
31 | 27, 28, 30 | cbvralw 3286 | . . . . 5 ⊢ (∀𝑦 ∈ (𝑋(,)𝑌)0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑦) ↔ ∀𝑥 ∈ (𝑋(,)𝑌)0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑥)) |
32 | 23, 31 | sylibr 233 | . . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (𝑋(,)𝑌)0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑦)) |
33 | 32 | r19.21bi 3231 | . . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 0 < ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))‘𝑦)) |
34 | ioossre 13245 | . . . . . 6 ⊢ (𝑋(,)𝑌) ⊆ ℝ | |
35 | resmpt 5981 | . . . . . 6 ⊢ ((𝑋(,)𝑌) ⊆ ℝ → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0))) | |
36 | 34, 35 | ax-mp 5 | . . . . 5 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) |
37 | 15 | mpteq2ia 5199 | . . . . 5 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) |
38 | 36, 37 | eqtri 2765 | . . . 4 ⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) |
39 | itggt0cn.cn | . . . 4 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) | |
40 | 38, 39 | eqeltrid 2842 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
41 | 1, 11, 33, 40 | itg2gt0cn 35988 | . 2 ⊢ (𝜑 → 0 < (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)))) |
42 | itggt0cn.2 | . . 3 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1) | |
43 | 3, 42, 4 | itgposval 25065 | . 2 ⊢ (𝜑 → ∫(𝑋(,)𝑌)𝐵 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑋(,)𝑌), 𝐵, 0)))) |
44 | 41, 43 | breqtrrd 5124 | 1 ⊢ (𝜑 → 0 < ∫(𝑋(,)𝑌)𝐵 d𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 = wceq 1541 ∈ wcel 2106 ∀wral 3062 ⊆ wss 3901 ifcif 4477 class class class wbr 5096 ↦ cmpt 5179 ↾ cres 5626 ‘cfv 6483 (class class class)co 7341 ℂcc 10974 ℝcr 10975 0cc0 10976 +∞cpnf 11111 < clt 11114 ≤ cle 11115 ℝ+crp 12835 (,)cioo 13184 [,)cico 13186 –cn→ccncf 24144 ∫2citg2 24885 𝐿1cibl 24886 ∫citg 24887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5233 ax-sep 5247 ax-nul 5254 ax-pow 5312 ax-pr 5376 ax-un 7654 ax-inf2 9502 ax-cnex 11032 ax-resscn 11033 ax-1cn 11034 ax-icn 11035 ax-addcl 11036 ax-addrcl 11037 ax-mulcl 11038 ax-mulrcl 11039 ax-mulcom 11040 ax-addass 11041 ax-mulass 11042 ax-distr 11043 ax-i2m1 11044 ax-1ne0 11045 ax-1rid 11046 ax-rnegex 11047 ax-rrecex 11048 ax-cnre 11049 ax-pre-lttri 11050 ax-pre-lttrn 11051 ax-pre-ltadd 11052 ax-pre-mulgt0 11053 ax-pre-sup 11054 ax-addf 11055 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3731 df-csb 3847 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3920 df-nul 4274 df-if 4478 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4857 df-int 4899 df-iun 4947 df-disj 5062 df-br 5097 df-opab 5159 df-mpt 5180 df-tr 5214 df-id 5522 df-eprel 5528 df-po 5536 df-so 5537 df-fr 5579 df-se 5580 df-we 5581 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6242 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6435 df-fun 6485 df-fn 6486 df-f 6487 df-f1 6488 df-fo 6489 df-f1o 6490 df-fv 6491 df-isom 6492 df-riota 7297 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7599 df-ofr 7600 df-om 7785 df-1st 7903 df-2nd 7904 df-frecs 8171 df-wrecs 8202 df-recs 8276 df-rdg 8315 df-1o 8371 df-2o 8372 df-er 8573 df-map 8692 df-pm 8693 df-en 8809 df-dom 8810 df-sdom 8811 df-fin 8812 df-fi 9272 df-sup 9303 df-inf 9304 df-oi 9371 df-dju 9762 df-card 9800 df-pnf 11116 df-mnf 11117 df-xr 11118 df-ltxr 11119 df-le 11120 df-sub 11312 df-neg 11313 df-div 11738 df-nn 12079 df-2 12141 df-3 12142 df-4 12143 df-n0 12339 df-z 12425 df-uz 12688 df-q 12794 df-rp 12836 df-xneg 12953 df-xadd 12954 df-xmul 12955 df-ioo 13188 df-ico 13190 df-icc 13191 df-fz 13345 df-fzo 13488 df-fl 13617 df-mod 13695 df-seq 13827 df-exp 13888 df-hash 14150 df-cj 14909 df-re 14910 df-im 14911 df-sqrt 15045 df-abs 15046 df-clim 15296 df-rlim 15297 df-sum 15497 df-rest 17230 df-topgen 17251 df-psmet 20694 df-xmet 20695 df-met 20696 df-bl 20697 df-mopn 20698 df-top 22148 df-topon 22165 df-bases 22201 df-cmp 22643 df-cncf 24146 df-ovol 24733 df-vol 24734 df-mbf 24888 df-itg1 24889 df-itg2 24890 df-ibl 24891 df-itg 24892 df-0p 24939 |
This theorem is referenced by: ftc1cnnclem 36004 |
Copyright terms: Public domain | W3C validator |