i1fibl

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

		Ref	Expression
	Assertion	i1fibl	$⊢ F \in dom \int^{1} \to F \in 𝐿^{1}$

Proof

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

Metamath Proof Explorer

Theorem i1fibl

Proof