Step | Hyp | Ref
| Expression |
1 | | i1frn 23489 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
2 | | difss 3770 |
. . . . 5
⊢ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹 |
3 | | ssfi 8221 |
. . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹) → (ran 𝐹 ∖ {0}) ∈
Fin) |
4 | 1, 2, 3 | sylancl 695 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (ran 𝐹 ∖ {0})
∈ Fin) |
5 | 4 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → (ran 𝐹 ∖ {0}) ∈ Fin) |
6 | | i1ff 23488 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → 𝐹:ℝ⟶ℝ) |
8 | | frn 6091 |
. . . . . . 7
⊢ (𝐹:ℝ⟶ℝ →
ran 𝐹 ⊆
ℝ) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → ran 𝐹 ⊆ ℝ) |
10 | 9 | ssdifssd 3781 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → (ran 𝐹 ∖ {0}) ⊆
ℝ) |
11 | 10 | sselda 3636 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 𝑥 ∈ ℝ) |
12 | | i1fima2sn 23492 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
13 | 12 | adantlr 751 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
14 | 11, 13 | remulcld 10108 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (𝑥 · (vol‘(◡𝐹 “ {𝑥}))) ∈ ℝ) |
15 | | eldifi 3765 |
. . . . 5
⊢ (𝑥 ∈ (ran 𝐹 ∖ {0}) → 𝑥 ∈ ran 𝐹) |
16 | | 0cn 10070 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
17 | | fnconstg 6131 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℂ → (ℂ × {0}) Fn ℂ) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℂ
× {0}) Fn ℂ |
19 | | df-0p 23482 |
. . . . . . . . . . . 12
⊢
0𝑝 = (ℂ × {0}) |
20 | 19 | fneq1i 6023 |
. . . . . . . . . . 11
⊢
(0𝑝 Fn ℂ ↔ (ℂ × {0}) Fn
ℂ) |
21 | 18, 20 | mpbir 221 |
. . . . . . . . . 10
⊢
0𝑝 Fn ℂ |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 Fn ℂ) |
23 | | ffn 6083 |
. . . . . . . . . 10
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
24 | 6, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 Fn
ℝ) |
25 | | cnex 10055 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
26 | 25 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ℂ ∈ V) |
27 | | reex 10065 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
28 | 27 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ℝ ∈ V) |
29 | | ax-resscn 10031 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
30 | | sseqin2 3850 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ) |
31 | 29, 30 | mpbi 220 |
. . . . . . . . 9
⊢ (ℂ
∩ ℝ) = ℝ |
32 | | 0pval 23483 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ →
(0𝑝‘𝑦) = 0) |
33 | 32 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ ℂ)
→ (0𝑝‘𝑦) = 0) |
34 | | eqidd 2652 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ ℝ)
→ (𝐹‘𝑦) = (𝐹‘𝑦)) |
35 | 22, 24, 26, 28, 31, 33, 34 | ofrfval 6947 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘𝑟 ≤ 𝐹 ↔ ∀𝑦 ∈ ℝ 0 ≤ (𝐹‘𝑦))) |
36 | 35 | biimpa 500 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → ∀𝑦 ∈ ℝ 0 ≤ (𝐹‘𝑦)) |
37 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → 𝐹 Fn ℝ) |
38 | | breq2 4689 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑦) → (0 ≤ 𝑥 ↔ 0 ≤ (𝐹‘𝑦))) |
39 | 38 | ralrn 6402 |
. . . . . . . 8
⊢ (𝐹 Fn ℝ →
(∀𝑥 ∈ ran 𝐹0 ≤ 𝑥 ↔ ∀𝑦 ∈ ℝ 0 ≤ (𝐹‘𝑦))) |
40 | 37, 39 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → (∀𝑥 ∈ ran 𝐹0 ≤ 𝑥 ↔ ∀𝑦 ∈ ℝ 0 ≤ (𝐹‘𝑦))) |
41 | 36, 40 | mpbird 247 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → ∀𝑥 ∈ ran 𝐹0 ≤ 𝑥) |
42 | 41 | r19.21bi 2961 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) ∧ 𝑥 ∈ ran 𝐹) → 0 ≤ 𝑥) |
43 | 15, 42 | sylan2 490 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 0 ≤ 𝑥) |
44 | | i1fima 23490 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {𝑥}) ∈ dom vol) |
45 | 44 | ad2antrr 762 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol) |
46 | | mblss 23345 |
. . . . . . 7
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ) |
47 | | ovolge0 23295 |
. . . . . . 7
⊢ ((◡𝐹 “ {𝑥}) ⊆ ℝ → 0 ≤
(vol*‘(◡𝐹 “ {𝑥}))) |
48 | 46, 47 | syl 17 |
. . . . . 6
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → 0 ≤
(vol*‘(◡𝐹 “ {𝑥}))) |
49 | | mblvol 23344 |
. . . . . 6
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ {𝑥}))) |
50 | 48, 49 | breqtrrd 4713 |
. . . . 5
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → 0 ≤
(vol‘(◡𝐹 “ {𝑥}))) |
51 | 45, 50 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 0 ≤
(vol‘(◡𝐹 “ {𝑥}))) |
52 | 11, 13, 43, 51 | mulge0d 10642 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 0 ≤ (𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
53 | 5, 14, 52 | fsumge0 14571 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → 0 ≤ Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
54 | | itg1val 23495 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
55 | 54 | adantr 480 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
56 | 53, 55 | breqtrrd 4713 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝐹) → 0 ≤
(∫1‘𝐹)) |