Metamath Proof Explorer

Theorem i1fibl

Description: A simple function is integrable. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion i1fibl ⊢F∈dom⁡∫1→F∈𝐿1

Proof

Step Hyp Ref Expression
1 i1ff ⊢F∈dom⁡∫1→F:ℝ⟶ℝ
2 1 feqmptd ⊢F∈dom⁡∫1→F=x∈ℝ⟼F⁡x
3 i1fmbf ⊢F∈dom⁡∫1→F∈MblFn
4 2 3 eqeltrrd ⊢F∈dom⁡∫1→x∈ℝ⟼F⁡x∈MblFn
5 simpr ⊢F∈dom⁡∫1∧x∈ℝ→x∈ℝ
6 5 biantrurd ⊢F∈dom⁡∫1∧x∈ℝ→0≤F⁡x↔x∈ℝ∧0≤F⁡x
7 6 ifbid ⊢F∈dom⁡∫1∧x∈ℝ→if0≤F⁡xF⁡x0=ifx∈ℝ∧0≤F⁡xF⁡x0
8 7 mpteq2dva ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0=x∈ℝ⟼ifx∈ℝ∧0≤F⁡xF⁡x0
9 8 fveq2d ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼if0≤F⁡xF⁡x0=∫2⁡x∈ℝ⟼ifx∈ℝ∧0≤F⁡xF⁡x0
10 eqid ⊢x∈ℝ⟼if0≤F⁡xF⁡x0=x∈ℝ⟼if0≤F⁡xF⁡x0
11 10 i1fpos ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0∈dom⁡∫1
12 0re ⊢0∈ℝ
13 1 ffvelcdmda ⊢F∈dom⁡∫1∧x∈ℝ→F⁡x∈ℝ
14 max1 ⊢0∈ℝ∧F⁡x∈ℝ→0≤if0≤F⁡xF⁡x0
15 12 13 14 sylancr ⊢F∈dom⁡∫1∧x∈ℝ→0≤if0≤F⁡xF⁡x0
16 15 ralrimiva ⊢F∈dom⁡∫1→∀x∈ℝ0≤if0≤F⁡xF⁡x0
17 reex ⊢ℝ∈V
18 17 a1i ⊢F∈dom⁡∫1→ℝ∈V
19 12 a1i ⊢F∈dom⁡∫1∧x∈ℝ→0∈ℝ
20 fvex ⊢F⁡x∈V
21 c0ex ⊢0∈V
22 20 21 ifex ⊢if0≤F⁡xF⁡x0∈V
23 22 a1i ⊢F∈dom⁡∫1∧x∈ℝ→if0≤F⁡xF⁡x0∈V
24 fconstmpt ⊢ℝ×0=x∈ℝ⟼0
25 24 a1i ⊢F∈dom⁡∫1→ℝ×0=x∈ℝ⟼0
26 eqidd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0=x∈ℝ⟼if0≤F⁡xF⁡x0
27 18 19 23 25 26 ofrfval2 ⊢F∈dom⁡∫1→ℝ×0≤fx∈ℝ⟼if0≤F⁡xF⁡x0↔∀x∈ℝ0≤if0≤F⁡xF⁡x0
28 16 27 mpbird ⊢F∈dom⁡∫1→ℝ×0≤fx∈ℝ⟼if0≤F⁡xF⁡x0
29 ax-resscn ⊢ℝ⊆ℂ
30 29 a1i ⊢F∈dom⁡∫1→ℝ⊆ℂ
31 22 10 fnmpti ⊢x∈ℝ⟼if0≤F⁡xF⁡x0Fnℝ
32 31 a1i ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0Fnℝ
33 30 32 0pledm ⊢F∈dom⁡∫1→0𝑝≤fx∈ℝ⟼if0≤F⁡xF⁡x0↔ℝ×0≤fx∈ℝ⟼if0≤F⁡xF⁡x0
34 28 33 mpbird ⊢F∈dom⁡∫1→0𝑝≤fx∈ℝ⟼if0≤F⁡xF⁡x0
35 itg2itg1 ⊢x∈ℝ⟼if0≤F⁡xF⁡x0∈dom⁡∫1∧0𝑝≤fx∈ℝ⟼if0≤F⁡xF⁡x0→∫2⁡x∈ℝ⟼if0≤F⁡xF⁡x0=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0
36 11 34 35 syl2anc ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼if0≤F⁡xF⁡x0=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0
37 9 36 eqtr3d ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼ifx∈ℝ∧0≤F⁡xF⁡x0=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0
38 itg1cl ⊢x∈ℝ⟼if0≤F⁡xF⁡x0∈dom⁡∫1→∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0∈ℝ
39 11 38 syl ⊢F∈dom⁡∫1→∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0∈ℝ
40 37 39 eqeltrd ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼ifx∈ℝ∧0≤F⁡xF⁡x0∈ℝ
41 5 biantrurd ⊢F∈dom⁡∫1∧x∈ℝ→0≤−F⁡x↔x∈ℝ∧0≤−F⁡x
42 41 ifbid ⊢F∈dom⁡∫1∧x∈ℝ→if0≤−F⁡x−F⁡x0=ifx∈ℝ∧0≤−F⁡x−F⁡x0
43 42 mpteq2dva ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0=x∈ℝ⟼ifx∈ℝ∧0≤−F⁡x−F⁡x0
44 43 fveq2d ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0=∫2⁡x∈ℝ⟼ifx∈ℝ∧0≤−F⁡x−F⁡x0
45 neg1rr ⊢−1∈ℝ
46 45 a1i ⊢F∈dom⁡∫1∧x∈ℝ→−1∈ℝ
47 fconstmpt ⊢ℝ×−1=x∈ℝ⟼−1
48 47 a1i ⊢F∈dom⁡∫1→ℝ×−1=x∈ℝ⟼−1
49 18 46 13 48 2 offval2 ⊢F∈dom⁡∫1→ℝ×−1×fF=x∈ℝ⟼-1⁢F⁡x
50 13 recnd ⊢F∈dom⁡∫1∧x∈ℝ→F⁡x∈ℂ
51 50 mulm1d ⊢F∈dom⁡∫1∧x∈ℝ→-1⁢F⁡x=−F⁡x
52 51 mpteq2dva ⊢F∈dom⁡∫1→x∈ℝ⟼-1⁢F⁡x=x∈ℝ⟼−F⁡x
53 49 52 eqtrd ⊢F∈dom⁡∫1→ℝ×−1×fF=x∈ℝ⟼−F⁡x
54 id ⊢F∈dom⁡∫1→F∈dom⁡∫1
55 45 a1i ⊢F∈dom⁡∫1→−1∈ℝ
56 54 55 i1fmulc ⊢F∈dom⁡∫1→ℝ×−1×fF∈dom⁡∫1
57 53 56 eqeltrrd ⊢F∈dom⁡∫1→x∈ℝ⟼−F⁡x∈dom⁡∫1
58 57 i1fposd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0∈dom⁡∫1
59 13 renegcld ⊢F∈dom⁡∫1∧x∈ℝ→−F⁡x∈ℝ
60 max1 ⊢0∈ℝ∧−F⁡x∈ℝ→0≤if0≤−F⁡x−F⁡x0
61 12 59 60 sylancr ⊢F∈dom⁡∫1∧x∈ℝ→0≤if0≤−F⁡x−F⁡x0
62 61 ralrimiva ⊢F∈dom⁡∫1→∀x∈ℝ0≤if0≤−F⁡x−F⁡x0
63 negex ⊢−F⁡x∈V
64 63 21 ifex ⊢if0≤−F⁡x−F⁡x0∈V
65 64 a1i ⊢F∈dom⁡∫1∧x∈ℝ→if0≤−F⁡x−F⁡x0∈V
66 eqidd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0=x∈ℝ⟼if0≤−F⁡x−F⁡x0
67 18 19 65 25 66 ofrfval2 ⊢F∈dom⁡∫1→ℝ×0≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0↔∀x∈ℝ0≤if0≤−F⁡x−F⁡x0
68 62 67 mpbird ⊢F∈dom⁡∫1→ℝ×0≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0
69 eqid ⊢x∈ℝ⟼if0≤−F⁡x−F⁡x0=x∈ℝ⟼if0≤−F⁡x−F⁡x0
70 64 69 fnmpti ⊢x∈ℝ⟼if0≤−F⁡x−F⁡x0Fnℝ
71 70 a1i ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0Fnℝ
72 30 71 0pledm ⊢F∈dom⁡∫1→0𝑝≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0↔ℝ×0≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0
73 68 72 mpbird ⊢F∈dom⁡∫1→0𝑝≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0
74 itg2itg1 ⊢x∈ℝ⟼if0≤−F⁡x−F⁡x0∈dom⁡∫1∧0𝑝≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0→∫2⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0=∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
75 58 73 74 syl2anc ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0=∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
76 44 75 eqtr3d ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼ifx∈ℝ∧0≤−F⁡x−F⁡x0=∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
77 itg1cl ⊢x∈ℝ⟼if0≤−F⁡x−F⁡x0∈dom⁡∫1→∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0∈ℝ
78 58 77 syl ⊢F∈dom⁡∫1→∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0∈ℝ
79 76 78 eqeltrd ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼ifx∈ℝ∧0≤−F⁡x−F⁡x0∈ℝ
80 13 iblrelem ⊢F∈dom⁡∫1→x∈ℝ⟼F⁡x∈𝐿1↔x∈ℝ⟼F⁡x∈MblFn∧∫2⁡x∈ℝ⟼ifx∈ℝ∧0≤F⁡xF⁡x0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈ℝ∧0≤−F⁡x−F⁡x0∈ℝ
81 4 40 79 80 mpbir3and ⊢F∈dom⁡∫1→x∈ℝ⟼F⁡x∈𝐿1
82 2 81 eqeltrd ⊢F∈dom⁡∫1→F∈𝐿1