Theorem itg1ge0a

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

	Ref	Expression
Hypotheses	itg10a.1	⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
	itg10a.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	itg10a.3	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
	itg1ge0a.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
Assertion	itg1ge0a	⊢ ( 𝜑 → 0 ≤ ( ∫1 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		itg10a.1	⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2		itg10a.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		itg10a.3	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
4		itg1ge0a.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
5		i1frn	⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
6	1 5	syl	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
7		difss	⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹
8		ssfi	⊢ ( ( ran 𝐹 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
9	6 7 8	sylancl	⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
10		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
11	1 10	syl	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
12	11	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
13	12	ssdifssd	⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ℝ )
14	13	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑘 ∈ ℝ )
15		i1fima2sn	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ )
16	1 15	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ )
17	14 16	remulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) ∈ ℝ )
18		0le0	⊢ 0 ≤ 0
19		i1fima	⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
20	1 19	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
21		mblvol	⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
22	20 21	syl	⊢ ( 𝜑 → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
23	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
24	11	ffnd	⊢ ( 𝜑 → 𝐹 Fn ℝ )
25		fniniseg	⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
26	24 25	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
27	26	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
28		simprl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → 𝑥 ∈ ℝ )
29		eldif	⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐴 ) )
30	4	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
31	30	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
32		simprr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑘 )
33	32	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ 0 ≤ 𝑘 ) )
34		0red	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → 0 ∈ ℝ )
35	14	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → 𝑘 ∈ ℝ )
36	34 35	lenltd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 0 ≤ 𝑘 ↔ ¬ 𝑘 < 0 ) )
37	33 36	bitrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ¬ 𝑘 < 0 ) )
38	31 37	sylibd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑘 < 0 ) )
39	29 38	syl5bir	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐴 ) → ¬ 𝑘 < 0 ) )
40	28 39	mpand	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ 𝑘 < 0 ) )
41	40	con4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 𝑘 < 0 → 𝑥 ∈ 𝐴 ) )
42	41	impancom	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) → 𝑥 ∈ 𝐴 ) )
43	27 42	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) → 𝑥 ∈ 𝐴 ) )
44	43	ssrdv	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( ◡ 𝐹 “ { 𝑘 } ) ⊆ 𝐴 )
45	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → 𝐴 ⊆ ℝ )
46	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( vol* ‘ 𝐴 ) = 0 )
47		ovolssnul	⊢ ( ( ( ◡ 𝐹 “ { 𝑘 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = 0 )
48	44 45 46 47	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = 0 )
49	23 48	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = 0 )
50	49	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) = ( 𝑘 · 0 ) )
51	14	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑘 ∈ ℂ )
52	51	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → 𝑘 ∈ ℂ )
53	52	mul01d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( 𝑘 · 0 ) = 0 )
54	50 53	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) = 0 )
55	18 54	breqtrrid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑘 < 0 ) → 0 ≤ ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
56	14	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → 𝑘 ∈ ℝ )
57	16	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ∈ ℝ )
58		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → 0 ≤ 𝑘 )
59	20	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
60		mblss	⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol → ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ )
61	59 60	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ )
62		ovolge0	⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ → 0 ≤ ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
63	61 62	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → 0 ≤ ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
64	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
65	63 64	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → 0 ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
66	56 57 58 65	mulge0d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 0 ≤ 𝑘 ) → 0 ≤ ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
67		0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 0 ∈ ℝ )
68	55 66 14 67	ltlecasei	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 0 ≤ ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
69	9 17 68	fsumge0	⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
70		itg1val	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
71	1 70	syl	⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
72	69 71	breqtrrd	⊢ ( 𝜑 → 0 ≤ ( ∫1 ‘ 𝐹 ) )