itg1ge0a

Description: The integral of an almost positive simple function is positive. (Contributed by Mario Carneiro, 11-Aug-2014)

	Ref	Expression
Hypotheses	itg10a.1	$⊢ φ \to F \in dom \int^{1}$
	itg10a.2	$⊢ φ \to A \subseteq ℝ$
	itg10a.3	$⊢ φ \to {vol}^{*} (A) = 0$
	itg1ge0a.4	$⊢ (φ \land x \in (ℝ ∖ A)) \to 0 \leq F (x)$
Assertion	itg1ge0a	$⊢ φ \to 0 \leq \int^{1} (F)$

Proof

Step	Hyp	Ref	Expression
1		itg10a.1	$⊢ φ \to F \in dom \int^{1}$
2		itg10a.2	$⊢ φ \to A \subseteq ℝ$
3		itg10a.3	$⊢ φ \to {vol}^{*} (A) = 0$
4		itg1ge0a.4	$⊢ (φ \land x \in (ℝ ∖ A)) \to 0 \leq F (x)$
5		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
6	1 5	syl	$⊢ φ \to ran F \in Fin$
7		difss	$⊢ ran F ∖ \{0\} \subseteq ran F$
8		ssfi	$⊢ (ran F \in Fin \land ran F ∖ \{0\} \subseteq ran F) \to ran F ∖ \{0\} \in Fin$
9	6 7 8	sylancl	$⊢ φ \to ran F ∖ \{0\} \in Fin$
10		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
11	1 10	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
12	11	frnd	$⊢ φ \to ran F \subseteq ℝ$
13	12	ssdifssd	$⊢ φ \to ran F ∖ \{0\} \subseteq ℝ$
14	13	sselda	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k \in ℝ$
15		i1fima2sn	$⊢ (F \in dom \int^{1} \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) \in ℝ$
16	1 15	sylan	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) \in ℝ$
17	14 16	remulcld	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k vol (F^{-1} [\{k\}]) \in ℝ$
18		0le0	$⊢ 0 \leq 0$
19		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{k\}] \in dom vol$
20	1 19	syl	$⊢ φ \to F^{-1} [\{k\}] \in dom vol$
21		mblvol	$⊢ F^{-1} [\{k\}] \in dom vol \to vol (F^{-1} [\{k\}]) = {vol}^{*} (F^{-1} [\{k\}])$
22	20 21	syl	$⊢ φ \to vol (F^{-1} [\{k\}]) = {vol}^{*} (F^{-1} [\{k\}])$
23	22	ad2antrr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to vol (F^{-1} [\{k\}]) = {vol}^{*} (F^{-1} [\{k\}])$
24	11	ffnd	$⊢ φ \to F Fn ℝ$
25		fniniseg	$⊢ F Fn ℝ \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land F (x) = k))$
26	24 25	syl	$⊢ φ \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land F (x) = k))$
27	26	ad2antrr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land F (x) = k))$
28		simprl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to x \in ℝ$
29		eldif	$⊢ x \in (ℝ ∖ A) \leftrightarrow (x \in ℝ \land \neg x \in A)$
30	4	ex	$⊢ φ \to (x \in (ℝ ∖ A) \to 0 \leq F (x))$
31	30	ad2antrr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (x \in (ℝ ∖ A) \to 0 \leq F (x))$
32		simprr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to F (x) = k$
33	32	breq2d	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (0 \leq F (x) \leftrightarrow 0 \leq k)$
34		0red	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to 0 \in ℝ$
35	14	adantr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to k \in ℝ$
36	34 35	lenltd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (0 \leq k \leftrightarrow \neg k < 0)$
37	33 36	bitrd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (0 \leq F (x) \leftrightarrow \neg k < 0)$
38	31 37	sylibd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (x \in (ℝ ∖ A) \to \neg k < 0)$
39	29 38	syl5bir	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to ((x \in ℝ \land \neg x \in A) \to \neg k < 0)$
40	28 39	mpand	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (\neg x \in A \to \neg k < 0)$
41	40	con4d	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (k < 0 \to x \in A)$
42	41	impancom	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to ((x \in ℝ \land F (x) = k) \to x \in A)$
43	27 42	sylbid	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to (x \in F^{-1} [\{k\}] \to x \in A)$
44	43	ssrdv	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to F^{-1} [\{k\}] \subseteq A$
45	2	ad2antrr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to A \subseteq ℝ$
46	3	ad2antrr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to {vol}^{*} (A) = 0$
47		ovolssnul	$⊢ (F^{-1} [\{k\}] \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) = 0) \to {vol}^{} (F^{-1} [\{k\}]) = 0$
48	44 45 46 47	syl3anc	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to {vol}^{*} (F^{-1} [\{k\}]) = 0$
49	23 48	eqtrd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to vol (F^{-1} [\{k\}]) = 0$
50	49	oveq2d	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to k vol (F^{-1} [\{k\}]) = k \cdot 0$
51	14	recnd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k \in ℂ$
52	51	adantr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to k \in ℂ$
53	52	mul01d	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to k \cdot 0 = 0$
54	50 53	eqtrd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to k vol (F^{-1} [\{k\}]) = 0$
55	18 54	breqtrrid	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land k < 0) \to 0 \leq k vol (F^{-1} [\{k\}])$
56	14	adantr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to k \in ℝ$
57	16	adantr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to vol (F^{-1} [\{k\}]) \in ℝ$
58		simpr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to 0 \leq k$
59	20	ad2antrr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to F^{-1} [\{k\}] \in dom vol$
60		mblss	$⊢ F^{-1} [\{k\}] \in dom vol \to F^{-1} [\{k\}] \subseteq ℝ$
61	59 60	syl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to F^{-1} [\{k\}] \subseteq ℝ$
62		ovolge0	$⊢ F^{-1} [\{k\}] \subseteq ℝ \to 0 \leq {vol}^{*} (F^{-1} [\{k\}])$
63	61 62	syl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to 0 \leq {vol}^{*} (F^{-1} [\{k\}])$
64	22	ad2antrr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to vol (F^{-1} [\{k\}]) = {vol}^{*} (F^{-1} [\{k\}])$
65	63 64	breqtrrd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to 0 \leq vol (F^{-1} [\{k\}])$
66	56 57 58 65	mulge0d	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land 0 \leq k) \to 0 \leq k vol (F^{-1} [\{k\}])$
67		0red	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to 0 \in ℝ$
68	55 66 14 67	ltlecasei	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to 0 \leq k vol (F^{-1} [\{k\}])$
69	9 17 68	fsumge0	$⊢ φ \to 0 \leq \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
70		itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
71	1 70	syl	$⊢ φ \to \int^{1} (F) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
72	69 71	breqtrrd	$⊢ φ \to 0 \leq \int^{1} (F)$

Metamath Proof Explorer

Theorem itg1ge0a

Proof