![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > i1ff | Structured version Visualization version GIF version |
Description: A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.) |
Ref | Expression |
---|---|
i1ff | ⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isi1f 25424 | . . 3 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))) | |
2 | 1 | simprbi 496 | . 2 ⊢ (𝐹 ∈ dom ∫1 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)) |
3 | 2 | simp1d 1141 | 1 ⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 ∈ wcel 2105 ∖ cdif 3945 {csn 4628 ◡ccnv 5675 dom cdm 5676 ran crn 5677 “ cima 5679 ⟶wf 6539 ‘cfv 6543 Fincfn 8943 ℝcr 11113 0cc0 11114 volcvol 25213 MblFncmbf 25364 ∫1citg1 25365 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-fv 6551 df-sum 15638 df-itg1 25370 |
This theorem is referenced by: i1fima 25428 i1fima2 25429 i1f0rn 25432 itg1val2 25434 itg1cl 25435 itg1ge0 25436 i1faddlem 25443 i1fmullem 25444 i1fadd 25445 i1fmul 25446 itg1addlem4 25449 itg1addlem4OLD 25450 itg1addlem5 25451 i1fmulclem 25453 i1fmulc 25454 itg1mulc 25455 i1fres 25456 i1fpos 25457 i1fposd 25458 i1fsub 25459 itg1sub 25460 itg10a 25461 itg1ge0a 25462 itg1lea 25463 itg1le 25464 itg1climres 25465 mbfi1fseqlem5 25470 mbfi1fseqlem6 25471 mbfi1flimlem 25473 mbfmullem2 25475 itg2itg1 25487 itg20 25488 itg2le 25490 itg2seq 25493 itg2uba 25494 itg2lea 25495 itg2mulclem 25497 itg2splitlem 25499 itg2split 25500 itg2monolem1 25501 itg2i1fseqle 25505 itg2i1fseq 25506 itg2addlem 25509 i1fibl 25558 itgitg1 25559 itg2addnclem 36843 itg2addnclem2 36844 itg2addnclem3 36845 itg2addnc 36846 ftc1anclem3 36867 ftc1anclem4 36868 ftc1anclem5 36869 ftc1anclem6 36870 ftc1anclem7 36871 ftc1anclem8 36872 ftc1anc 36873 |
Copyright terms: Public domain | W3C validator |