Theorem i1fibl

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

	Ref	Expression
Assertion	i1fibl	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1 )

Proof

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