Step | Hyp | Ref
| Expression |
1 | | itg2cn.3 |
. . . . . 6
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
2 | | itg2cn.4 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
3 | 2 | rphalfcld 11760 |
. . . . . 6
⊢ (𝜑 → (𝐶 / 2) ∈
ℝ+) |
4 | 1, 3 | ltsubrpd 11780 |
. . . . 5
⊢ (𝜑 →
((∫2‘𝐹) − (𝐶 / 2)) < (∫2‘𝐹)) |
5 | 3 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 2) ∈ ℝ) |
6 | 1, 5 | resubcld 10337 |
. . . . . 6
⊢ (𝜑 →
((∫2‘𝐹) − (𝐶 / 2)) ∈ ℝ) |
7 | 6, 1 | ltnled 10063 |
. . . . 5
⊢ (𝜑 →
(((∫2‘𝐹) − (𝐶 / 2)) < (∫2‘𝐹) ↔ ¬
(∫2‘𝐹)
≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
8 | 4, 7 | mpbid 221 |
. . . 4
⊢ (𝜑 → ¬
(∫2‘𝐹)
≤ ((∫2‘𝐹) − (𝐶 / 2))) |
9 | | itg2cn.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
10 | 9 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
11 | | elrege0 12149 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
12 | 10, 11 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
13 | 12 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
14 | 13 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈
ℝ*) |
15 | 12 | simprd 478 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
16 | | elxrge0 12152 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) ∈ (0[,]+∞) ↔ ((𝐹‘𝑥) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝑥))) |
17 | 14, 15, 16 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,]+∞)) |
18 | | 0e0iccpnf 12154 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]+∞) |
19 | | ifcl 4080 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈
(0[,]+∞)) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ (0[,]+∞)) |
20 | 17, 18, 19 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ (0[,]+∞)) |
21 | 20 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ (0[,]+∞)) |
22 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
23 | 21, 22 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥),
0)):ℝ⟶(0[,]+∞)) |
24 | | itg2cl 23305 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) ∈
ℝ*) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) ∈
ℝ*) |
26 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) |
27 | 25, 26 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥),
0)))):ℕ⟶ℝ*) |
28 | | frn 5966 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))):ℕ⟶ℝ*
→ ran (𝑛 ∈
ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) ⊆
ℝ*) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) ⊆
ℝ*) |
30 | 6 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 →
((∫2‘𝐹) − (𝐶 / 2)) ∈
ℝ*) |
31 | | supxrleub 12028 |
. . . . . 6
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) ⊆ ℝ* ∧
((∫2‘𝐹) − (𝐶 / 2)) ∈ ℝ*) →
(sup(ran (𝑛 ∈ ℕ
↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) ≤
((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
32 | 29, 30, 31 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) ≤
((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
33 | | itg2cn.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ MblFn) |
34 | 9, 33, 1 | itg2cnlem1 23334 |
. . . . . 6
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) =
(∫2‘𝐹)) |
35 | 34 | breq1d 4593 |
. . . . 5
⊢ (𝜑 → (sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) ≤
((∫2‘𝐹) − (𝐶 / 2)) ↔ (∫2‘𝐹) ≤
((∫2‘𝐹) − (𝐶 / 2)))) |
36 | | ffn 5958 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))):ℕ⟶ℝ*
→ (𝑛 ∈ ℕ
↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) Fn ℕ) |
37 | 27, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) Fn ℕ) |
38 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) → (𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
39 | 38 | ralrn 6270 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
40 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑥) ≤ 𝑛 ↔ (𝐹‘𝑥) ≤ 𝑚)) |
41 | 40 | ifbid 4058 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
42 | 41 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
44 | | fvex 6113 |
. . . . . . . . . 10
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ∈ V |
45 | 43, 26, 44 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
46 | 45 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
47 | 46 | ralbiia 2962 |
. . . . . . 7
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))‘𝑚) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
48 | 39, 47 | syl6bb 275 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
49 | 37, 48 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))))𝑧 ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
50 | 32, 35, 49 | 3bitr3d 297 |
. . . 4
⊢ (𝜑 →
((∫2‘𝐹) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) |
51 | 8, 50 | mtbid 313 |
. . 3
⊢ (𝜑 → ¬ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
52 | | rexnal 2978 |
. . 3
⊢
(∃𝑚 ∈
ℕ ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔ ¬ ∀𝑚 ∈ ℕ
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
53 | 51, 52 | sylibr 223 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
54 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → 𝐹:ℝ⟶(0[,)+∞)) |
55 | 33 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → 𝐹 ∈ MblFn) |
56 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) →
(∫2‘𝐹)
∈ ℝ) |
57 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → 𝐶 ∈
ℝ+) |
58 | | simprl 790 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → 𝑚 ∈ ℕ) |
59 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
60 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
61 | 60 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ 𝑚)) |
62 | 61, 60 | ifbieq1d 4059 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
63 | 62 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
64 | 63 | fveq2i 6106 |
. . . . . 6
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) = (∫2‘(𝑦 ∈ ℝ ↦
if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) |
65 | 64 | breq1i 4590 |
. . . . 5
⊢
((∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)) ↔
(∫2‘(𝑦
∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
66 | 59, 65 | sylnib 317 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → ¬
(∫2‘(𝑦
∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2))) |
67 | 54, 55, 56, 57, 58, 66 | itg2cnlem2 23335 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶)) |
68 | | elequ1 1984 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑢 ↔ 𝑦 ∈ 𝑢)) |
69 | 68, 60 | ifbieq1d 4059 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0) = if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0)) |
70 | 69 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0)) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0)) |
71 | 70 | fveq2i 6106 |
. . . . . . 7
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) = (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) |
72 | 71 | breq1i 4590 |
. . . . . 6
⊢
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶 ↔ (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶) |
73 | 72 | imbi2i 325 |
. . . . 5
⊢
(((vol‘𝑢) <
𝑑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶) ↔ ((vol‘𝑢) < 𝑑 → (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶)) |
74 | 73 | ralbii 2963 |
. . . 4
⊢
(∀𝑢 ∈
dom vol((vol‘𝑢) <
𝑑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶) ↔ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶)) |
75 | 74 | rexbii 3023 |
. . 3
⊢
(∃𝑑 ∈
ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶) ↔ ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝑢, (𝐹‘𝑦), 0))) < 𝐶)) |
76 | 67, 75 | sylibr 223 |
. 2
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ ¬
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))) → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) |
77 | 53, 76 | rexlimddv 3017 |
1
⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) |