MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  i1ff Structured version   Visualization version   GIF version

Theorem i1ff 23366
Description: A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.)
Assertion
Ref Expression
i1ff (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)

Proof of Theorem i1ff
StepHypRef Expression
1 isi1f 23364 . . 3 (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
21simprbi 480 . 2 (𝐹 ∈ dom ∫1 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
32simp1d 1071 1 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036  wcel 1987  cdif 3556  {csn 4153  ccnv 5078  dom cdm 5079  ran crn 5080  cima 5082  wf 5848  cfv 5852  Fincfn 7907  cr 9887  0cc0 9888  volcvol 23155  MblFncmbf 23306  1citg1 23307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-fv 5860  df-sum 14359  df-itg1 23312
This theorem is referenced by:  i1fima  23368  i1fima2  23369  i1f0rn  23372  itg1val2  23374  itg1cl  23375  itg1ge0  23376  i1faddlem  23383  i1fmullem  23384  i1fadd  23385  i1fmul  23386  itg1addlem4  23389  itg1addlem5  23390  i1fmulclem  23392  i1fmulc  23393  itg1mulc  23394  i1fres  23395  i1fpos  23396  i1fposd  23397  i1fsub  23398  itg1sub  23399  itg10a  23400  itg1ge0a  23401  itg1lea  23402  itg1le  23403  itg1climres  23404  mbfi1fseqlem5  23409  mbfi1fseqlem6  23410  mbfi1flimlem  23412  mbfmullem2  23414  itg2itg1  23426  itg20  23427  itg2le  23429  itg2seq  23432  itg2uba  23433  itg2lea  23434  itg2mulclem  23436  itg2splitlem  23438  itg2split  23439  itg2monolem1  23440  itg2i1fseqle  23444  itg2i1fseq  23445  itg2addlem  23448  i1fibl  23497  itgitg1  23498  itg2addnclem  33128  itg2addnclem2  33129  itg2addnclem3  33130  itg2addnc  33131  ftc1anclem3  33154  ftc1anclem4  33155  ftc1anclem5  33156  ftc1anclem6  33157  ftc1anclem7  33158  ftc1anclem8  33159  ftc1anc  33160
  Copyright terms: Public domain W3C validator