Step |
Hyp |
Ref |
Expression |
1 |
|
sge0less.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) |
2 |
|
sge0less.f |
⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) |
3 |
|
sge0ssre.re |
⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ ) |
4 |
|
inex1g |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∩ 𝑌 ) ∈ V ) |
5 |
1 4
|
syl |
⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ∈ V ) |
6 |
|
fresin |
⊢ ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) → ( 𝐹 ↾ 𝑌 ) : ( 𝑋 ∩ 𝑌 ) ⟶ ( 0 [,] +∞ ) ) |
7 |
2 6
|
syl |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝑌 ) : ( 𝑋 ∩ 𝑌 ) ⟶ ( 0 [,] +∞ ) ) |
8 |
5 7
|
sge0xrcl |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ∈ ℝ* ) |
9 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
10 |
9
|
a1i |
⊢ ( 𝜑 → -∞ ∈ ℝ* ) |
11 |
|
0xr |
⊢ 0 ∈ ℝ* |
12 |
11
|
a1i |
⊢ ( 𝜑 → 0 ∈ ℝ* ) |
13 |
|
mnflt0 |
⊢ -∞ < 0 |
14 |
13
|
a1i |
⊢ ( 𝜑 → -∞ < 0 ) |
15 |
5 7
|
sge0ge0 |
⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ) |
16 |
10 12 8 14 15
|
xrltletrd |
⊢ ( 𝜑 → -∞ < ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ) |
17 |
1 2
|
sge0less |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ ( Σ^ ‘ 𝐹 ) ) |
18 |
|
xrre |
⊢ ( ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ∈ ℝ* ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) ∧ ( -∞ < ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ∧ ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ ( Σ^ ‘ 𝐹 ) ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ∈ ℝ ) |
19 |
8 3 16 17 18
|
syl22anc |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ∈ ℝ ) |