Metamath Proof Explorer

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 ‘ 𝐹 ) )