| Step | Hyp | Ref
| Expression |
| 1 | | itg2cn.3 |
. . . . . 6
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
| 2 | | itg2cn.4 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 3 | 2 | rphalfcld 13089 |
. . . . . 6
⊢ (𝜑 → (𝐶 / 2) ∈
ℝ+) |
| 4 | 1, 3 | ltsubrpd 13109 |
. . . . 5
⊢ (𝜑 →
((∫2‘𝐹) − (𝐶 / 2)) < (∫2‘𝐹)) |
| 5 | 3 | rpred 13077 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 2) ∈ ℝ) |
| 6 | 1, 5 | resubcld 11691 |
. . . . . 6
⊢ (𝜑 →
((∫2‘𝐹) − (𝐶 / 2)) ∈ ℝ) |
| 7 | 6, 1 | ltnled 11408 |
. . . . 5
⊢ (𝜑 →
(((∫2‘𝐹) − (𝐶 / 2)) < (∫2‘𝐹) ↔ ¬
(∫2‘𝐹)
≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 8 | 4, 7 | mpbid 232 |
. . . 4
⊢ (𝜑 → ¬
(∫2‘𝐹)
≤ ((∫2‘𝐹) − (𝐶 / 2))) |
| 9 | | itg2cn.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
| 10 | 9 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
| 11 | | elrege0 13494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 12 | 10, 11 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 13 | 12 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
| 14 | 13 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈
ℝ*) |
| 15 | 12 | simprd 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
| 16 | | elxrge0 13497 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) ∈ (0[,]+∞) ↔ ((𝐹‘𝑥) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝑥))) |
| 17 | 14, 15, 16 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,]+∞)) |
| 18 | | 0e0iccpnf 13499 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]+∞) |
| 19 | | ifcl 4571 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈
(0[,]+∞)) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ (0[,]+∞)) |
| 20 | 17, 18, 19 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ (0[,]+∞)) |
| 21 | 20 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ (0[,]+∞)) |
| 22 | 21 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥),
0)):ℝ⟶(0[,]+∞)) |
| 23 | | itg2cl 25767 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) ∈
ℝ*) |
| 24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) ∈
ℝ*) |
| 25 | 24 | fmpttd 7135 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥),
0)))):ℕ⟶ℝ*) |
| 26 | 25 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) ⊆
ℝ*) |
| 27 | 6 | rexrd 11311 |
. . . . . 6
⊢ (𝜑 →
((∫2‘𝐹) − (𝐶 / 2)) ∈
ℝ*) |
| 28 | | supxrleub 13368 |
. . . . . 6
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) ⊆ ℝ* ∧
((∫2‘𝐹) − (𝐶 / 2)) ∈ ℝ*) →
(sup(ran (𝑛 ∈ ℕ
↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) ≤
((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 29 | 26, 27, 28 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) ≤
((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 30 | | itg2cn.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ MblFn) |
| 31 | 9, 30, 1 | itg2cnlem1 25796 |
. . . . . 6
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) =
(∫2‘𝐹)) |
| 32 | 31 | breq1d 5153 |
. . . . 5
⊢ (𝜑 → (sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) ≤
((∫2‘𝐹) − (𝐶 / 2)) ↔ (∫2‘𝐹) ≤
((∫2‘𝐹) − (𝐶 / 2)))) |
| 33 | 25 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) Fn ℕ) |
| 34 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) → (𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 35 | 34 | ralrn 7108 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 36 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑥) ≤ 𝑛 ↔ (𝐹‘𝑥) ≤ 𝑚)) |
| 37 | 36 | ifbid 4549 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
| 38 | 37 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
| 39 | 38 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
| 40 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) |
| 41 | | fvex 6919 |
. . . . . . . . . 10
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ∈ V |
| 42 | 39, 40, 41 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
| 43 | 42 | breq1d 5153 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 44 | 43 | ralbiia 3091 |
. . . . . . 7
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
| 45 | 35, 44 | bitrdi 287 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 46 | 33, 45 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 47 | 29, 32, 46 | 3bitr3d 309 |
. . . 4
⊢ (𝜑 →
((∫2‘𝐹) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
| 48 | 8, 47 | mtbid 324 |
. . 3
⊢ (𝜑 → ¬ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
| 49 | | rexnal 3100 |
. . 3
⊢
(∃𝑚 ∈
ℕ ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ¬ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
| 50 | 48, 49 | sylibr 234 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
| 51 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → 𝐹:ℝ⟶(0[,)+∞)) |
| 52 | 30 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → 𝐹 ∈ MblFn) |
| 53 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) →
(∫2‘𝐹)
∈ ℝ) |
| 54 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → 𝐶 ∈
ℝ+) |
| 55 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → 𝑚 ∈ ℕ) |
| 56 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
| 57 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
| 58 | 57 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ 𝑚)) |
| 59 | 58, 57 | ifbieq1d 4550 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
| 60 | 59 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
| 61 | 60 | fveq2i 6909 |
. . . . . 6
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) = (∫2‘(𝑦 ∈ ℝ ↦
if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) |
| 62 | 61 | breq1i 5150 |
. . . . 5
⊢
((∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔
(∫2‘(𝑦
∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
| 63 | 56, 62 | sylnib 328 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → ¬
(∫2‘(𝑦
∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
| 64 | 51, 52, 53, 54, 55, 63 | itg2cnlem2 25797 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶)) |
| 65 | | elequ1 2115 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑢 ↔ 𝑦 ∈ 𝑢)) |
| 66 | 65, 57 | ifbieq1d 4550 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0) = if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0)) |
| 67 | 66 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0)) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0)) |
| 68 | 67 | fveq2i 6909 |
. . . . . . 7
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) = (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) |
| 69 | 68 | breq1i 5150 |
. . . . . 6
⊢
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶 ↔ (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶) |
| 70 | 69 | imbi2i 336 |
. . . . 5
⊢
(((vol‘𝑢) <
𝑑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶) ↔ ((vol‘𝑢) < 𝑑 → (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶)) |
| 71 | 70 | ralbii 3093 |
. . . 4
⊢
(∀𝑢 ∈
dom vol((vol‘𝑢) <
𝑑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶) ↔ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶)) |
| 72 | 71 | rexbii 3094 |
. . 3
⊢
(∃𝑑 ∈
ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶) ↔ ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶)) |
| 73 | 64, 72 | sylibr 234 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) |
| 74 | 50, 73 | rexlimddv 3161 |
1
⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) |