![]() |
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 23841 | . . 3 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))) | |
2 | 1 | simprbi 492 | . 2 ⊢ (𝐹 ∈ dom ∫1 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)) |
3 | 2 | simp1d 1178 | 1 ⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1113 ∈ wcel 2166 ∖ cdif 3796 {csn 4398 ◡ccnv 5342 dom cdm 5343 ran crn 5344 “ cima 5346 ⟶wf 6120 ‘cfv 6124 Fincfn 8223 ℝcr 10252 0cc0 10253 volcvol 23630 MblFncmbf 23781 ∫1citg1 23782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-sbc 3664 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-fv 6132 df-sum 14795 df-itg1 23787 |
This theorem is referenced by: i1fima 23845 i1fima2 23846 i1f0rn 23849 itg1val2 23851 itg1cl 23852 itg1ge0 23853 i1faddlem 23860 i1fmullem 23861 i1fadd 23862 i1fmul 23863 itg1addlem4 23866 itg1addlem5 23867 i1fmulclem 23869 i1fmulc 23870 itg1mulc 23871 i1fres 23872 i1fpos 23873 i1fposd 23874 i1fsub 23875 itg1sub 23876 itg10a 23877 itg1ge0a 23878 itg1lea 23879 itg1le 23880 itg1climres 23881 mbfi1fseqlem5 23886 mbfi1fseqlem6 23887 mbfi1flimlem 23889 mbfmullem2 23891 itg2itg1 23903 itg20 23904 itg2le 23906 itg2seq 23909 itg2uba 23910 itg2lea 23911 itg2mulclem 23913 itg2splitlem 23915 itg2split 23916 itg2monolem1 23917 itg2i1fseqle 23921 itg2i1fseq 23922 itg2addlem 23925 i1fibl 23974 itgitg1 23975 itg2addnclem 34005 itg2addnclem2 34006 itg2addnclem3 34007 itg2addnc 34008 ftc1anclem3 34031 ftc1anclem4 34032 ftc1anclem5 34033 ftc1anclem6 34034 ftc1anclem7 34035 ftc1anclem8 34036 ftc1anc 34037 |
Copyright terms: Public domain | W3C validator |