Step |
Hyp |
Ref |
Expression |
1 |
|
itg10 |
⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = 0 |
2 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ) |
3 |
|
0xr |
⊢ 0 ∈ ℝ* |
4 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
5 |
|
elicc1 |
⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) ≤ +∞ ) ) ) |
6 |
3 4 5
|
mp2an |
⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) ≤ +∞ ) ) |
7 |
6
|
simp2bi |
⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) ) |
8 |
2 7
|
syl |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) ) |
9 |
8
|
ralrimiva |
⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ∀ 𝑦 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) |
10 |
|
0re |
⊢ 0 ∈ ℝ |
11 |
|
fnconstg |
⊢ ( 0 ∈ ℝ → ( ℝ × { 0 } ) Fn ℝ ) |
12 |
10 11
|
mp1i |
⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ℝ × { 0 } ) Fn ℝ ) |
13 |
|
ffn |
⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → 𝐹 Fn ℝ ) |
14 |
|
reex |
⊢ ℝ ∈ V |
15 |
14
|
a1i |
⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ℝ ∈ V ) |
16 |
|
inidm |
⊢ ( ℝ ∩ ℝ ) = ℝ |
17 |
|
c0ex |
⊢ 0 ∈ V |
18 |
17
|
fvconst2 |
⊢ ( 𝑦 ∈ ℝ → ( ( ℝ × { 0 } ) ‘ 𝑦 ) = 0 ) |
19 |
18
|
adantl |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℝ × { 0 } ) ‘ 𝑦 ) = 0 ) |
20 |
|
eqidd |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
21 |
12 13 15 15 16 19 20
|
ofrfval |
⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ( ℝ × { 0 } ) ∘r ≤ 𝐹 ↔ ∀ 𝑦 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) ) |
22 |
9 21
|
mpbird |
⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ℝ × { 0 } ) ∘r ≤ 𝐹 ) |
23 |
|
i1f0 |
⊢ ( ℝ × { 0 } ) ∈ dom ∫1 |
24 |
|
itg2ub |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ℝ × { 0 } ) ∈ dom ∫1 ∧ ( ℝ × { 0 } ) ∘r ≤ 𝐹 ) → ( ∫1 ‘ ( ℝ × { 0 } ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
25 |
23 24
|
mp3an2 |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ℝ × { 0 } ) ∘r ≤ 𝐹 ) → ( ∫1 ‘ ( ℝ × { 0 } ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
26 |
22 25
|
mpdan |
⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫1 ‘ ( ℝ × { 0 } ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
27 |
1 26
|
eqbrtrrid |
⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → 0 ≤ ( ∫2 ‘ 𝐹 ) ) |