| Step |
Hyp |
Ref |
Expression |
| 1 |
|
itg2cn.1 |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ) |
| 2 |
|
itg2cn.2 |
⊢ ( 𝜑 → 𝐹 ∈ MblFn ) |
| 3 |
|
itg2cn.3 |
⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ ) |
| 4 |
|
itg2cn.4 |
⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) |
| 5 |
|
itg2cn.5 |
⊢ ( 𝜑 → 𝑀 ∈ ℕ ) |
| 6 |
|
itg2cn.6 |
⊢ ( 𝜑 → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) |
| 7 |
4
|
rphalfcld |
⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ+ ) |
| 8 |
5
|
nnrpd |
⊢ ( 𝜑 → 𝑀 ∈ ℝ+ ) |
| 9 |
7 8
|
rpdivcld |
⊢ ( 𝜑 → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ+ ) |
| 10 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 ∈ dom vol ) |
| 11 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 ∈ MblFn ) |
| 12 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
| 13 |
|
fss |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ ) |
| 14 |
1 12 13
|
sylancl |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
| 15 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ℝ ) |
| 16 |
|
mbfima |
⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) |
| 17 |
11 15 16
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) |
| 18 |
|
inmbl |
⊢ ( ( 𝑢 ∈ dom vol ∧ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) → ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
| 19 |
10 17 18
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
| 20 |
|
difmbl |
⊢ ( ( 𝑢 ∈ dom vol ∧ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
| 21 |
10 17 20
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
| 22 |
|
inass |
⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ( 𝑢 ∩ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) |
| 23 |
|
disjdif |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅ |
| 24 |
23
|
ineq2i |
⊢ ( 𝑢 ∩ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( 𝑢 ∩ ∅ ) |
| 25 |
|
in0 |
⊢ ( 𝑢 ∩ ∅ ) = ∅ |
| 26 |
22 24 25
|
3eqtri |
⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅ |
| 27 |
26
|
fveq2i |
⊢ ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( vol* ‘ ∅ ) |
| 28 |
|
ovol0 |
⊢ ( vol* ‘ ∅ ) = 0 |
| 29 |
27 28
|
eqtri |
⊢ ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 |
| 30 |
29
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 ) |
| 31 |
|
inundif |
⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = 𝑢 |
| 32 |
31
|
eqcomi |
⊢ 𝑢 = ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
| 33 |
32
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 = ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) |
| 34 |
|
mblss |
⊢ ( 𝑢 ∈ dom vol → 𝑢 ⊆ ℝ ) |
| 35 |
10 34
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 ⊆ ℝ ) |
| 36 |
35
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → 𝑥 ∈ ℝ ) |
| 37 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ) |
| 38 |
37
|
ffvelcdmda |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) |
| 39 |
|
elrege0 |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 40 |
38 39
|
sylib |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 41 |
40
|
simpld |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
| 42 |
41
|
rexrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ) |
| 43 |
40
|
simprd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 44 |
|
elxrge0 |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 45 |
42 43 44
|
sylanbrc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) |
| 46 |
36 45
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) |
| 47 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 48 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 49 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 50 |
|
0e0iccpnf |
⊢ 0 ∈ ( 0 [,] +∞ ) |
| 51 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 52 |
45 50 51
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 53 |
52
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
| 54 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ ) |
| 55 |
|
icossicc |
⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) |
| 56 |
|
fss |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ) |
| 57 |
37 55 56
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ) |
| 58 |
41
|
leidd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 59 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 60 |
|
breq1 |
⊢ ( 0 = if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 61 |
59 60
|
ifboth |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 62 |
58 43 61
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 63 |
62
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 64 |
|
reex |
⊢ ℝ ∈ V |
| 65 |
64
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ℝ ∈ V ) |
| 66 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 67 |
37
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
| 68 |
65 52 41 66 67
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 69 |
63 68
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) |
| 70 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
| 71 |
53 57 69 70
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
| 72 |
|
itg2lecl |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
| 73 |
53 54 71 72
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
| 74 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 75 |
45 50 74
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 76 |
75
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
| 77 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 78 |
|
breq1 |
⊢ ( 0 = if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 79 |
77 78
|
ifboth |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 80 |
58 43 79
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 81 |
80
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 82 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 83 |
65 75 41 82 67
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 84 |
81 83
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) |
| 85 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
| 86 |
76 57 84 85
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
| 87 |
|
itg2lecl |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
| 88 |
76 54 86 87
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
| 89 |
19 21 30 33 46 47 48 49 73 88
|
itg2split |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 90 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐶 ∈ ℝ+ ) |
| 91 |
90
|
rphalfcld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝐶 / 2 ) ∈ ℝ+ ) |
| 92 |
91
|
rpred |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝐶 / 2 ) ∈ ℝ ) |
| 93 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 94 |
45 50 93
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 95 |
94
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
| 96 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 97 |
|
breq1 |
⊢ ( 0 = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 98 |
96 97
|
ifboth |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 99 |
58 43 98
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 100 |
99
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 101 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 102 |
65 94 45 101 67
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 103 |
100 102
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) |
| 104 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
| 105 |
95 57 103 104
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
| 106 |
|
itg2lecl |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
| 107 |
95 54 105 106
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
| 108 |
|
0red |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ ) |
| 109 |
|
elinel2 |
⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) |
| 110 |
109
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
| 111 |
|
ifle |
⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 112 |
41 108 43 110 111
|
syl31anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 113 |
112
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 114 |
65 52 94 66 101
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 115 |
113 114
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 116 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 117 |
53 95 115 116
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 118 |
67
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 119 |
|
cmmbl |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
| 120 |
17 119
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
| 121 |
|
disjdif |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅ |
| 122 |
121
|
fveq2i |
⊢ ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( vol* ‘ ∅ ) |
| 123 |
122 28
|
eqtri |
⊢ ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 |
| 124 |
123
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 ) |
| 125 |
|
undif2 |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ ) |
| 126 |
|
mblss |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ ) |
| 127 |
17 126
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ ) |
| 128 |
|
ssequn1 |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ ↔ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ ) = ℝ ) |
| 129 |
127 128
|
sylib |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ ) = ℝ ) |
| 130 |
125 129
|
eqtr2id |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ℝ = ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) |
| 131 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 132 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 133 |
|
iftrue |
⊢ ( 𝑥 ∈ ℝ → if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) ) |
| 134 |
133
|
mpteq2ia |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) |
| 135 |
134
|
eqcomi |
⊢ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 136 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 137 |
45 50 136
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 138 |
137
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
| 139 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 140 |
|
breq1 |
⊢ ( 0 = if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 141 |
139 140
|
ifboth |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 142 |
58 43 141
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 143 |
142
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
| 144 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 145 |
65 137 45 144 67
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 146 |
143 145
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) |
| 147 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
| 148 |
138 57 146 147
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
| 149 |
|
itg2lecl |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
| 150 |
138 54 148 149
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
| 151 |
17 120 124 130 45 131 132 135 107 150
|
itg2split |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 152 |
118 151
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 153 |
|
eldif |
⊢ ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
| 154 |
153
|
baib |
⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
| 155 |
154
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
| 156 |
1
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn ℝ ) |
| 157 |
156
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝐹 Fn ℝ ) |
| 158 |
|
elpreima |
⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) ) |
| 159 |
157 158
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) ) |
| 160 |
41
|
biantrurd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 161 |
5
|
nnred |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
| 162 |
161
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℝ ) |
| 163 |
162
|
rexrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℝ* ) |
| 164 |
|
elioopnf |
⊢ ( 𝑀 ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 165 |
163 164
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 166 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ ) |
| 167 |
166
|
biantrurd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) ) |
| 168 |
160 165 167
|
3bitr2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) ) |
| 169 |
162 41
|
ltnled |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) |
| 170 |
159 168 169
|
3bitr2rd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
| 171 |
170
|
con1bid |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) |
| 172 |
155 171
|
bitrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) |
| 173 |
172
|
ifbid |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 174 |
173
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 175 |
174
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 176 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) |
| 177 |
175 176
|
eqnbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) |
| 178 |
54 92
|
resubcld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ∈ ℝ ) |
| 179 |
178 150
|
ltnled |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ↔ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) |
| 180 |
177 179
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 181 |
54 92 150
|
ltsubadd2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ↔ ( ∫2 ‘ 𝐹 ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) ) |
| 182 |
180 181
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 183 |
152 182
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 184 |
107 92 150
|
ltadd1d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ↔ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) ) |
| 185 |
183 184
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ) |
| 186 |
73 107 92 117 185
|
lelttrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ) |
| 187 |
161
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℝ ) |
| 188 |
|
mblvol |
⊢ ( 𝑢 ∈ dom vol → ( vol ‘ 𝑢 ) = ( vol* ‘ 𝑢 ) ) |
| 189 |
10 188
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) = ( vol* ‘ 𝑢 ) ) |
| 190 |
9
|
rpred |
⊢ ( 𝜑 → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ ) |
| 191 |
190
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ ) |
| 192 |
|
ovolcl |
⊢ ( 𝑢 ⊆ ℝ → ( vol* ‘ 𝑢 ) ∈ ℝ* ) |
| 193 |
35 192
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ* ) |
| 194 |
191
|
rexrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ* ) |
| 195 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) |
| 196 |
189 195
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) |
| 197 |
193 194 196
|
xrltled |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ≤ ( ( 𝐶 / 2 ) / 𝑀 ) ) |
| 198 |
|
ovollecl |
⊢ ( ( 𝑢 ⊆ ℝ ∧ ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ ∧ ( vol* ‘ 𝑢 ) ≤ ( ( 𝐶 / 2 ) / 𝑀 ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ ) |
| 199 |
35 191 197 198
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ ) |
| 200 |
189 199
|
eqeltrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) ∈ ℝ ) |
| 201 |
187 200
|
remulcld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑀 · ( vol ‘ 𝑢 ) ) ∈ ℝ ) |
| 202 |
187
|
rexrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℝ* ) |
| 203 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℕ ) |
| 204 |
203
|
nnnn0d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℕ0 ) |
| 205 |
204
|
nn0ge0d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 ≤ 𝑀 ) |
| 206 |
|
elxrge0 |
⊢ ( 𝑀 ∈ ( 0 [,] +∞ ) ↔ ( 𝑀 ∈ ℝ* ∧ 0 ≤ 𝑀 ) ) |
| 207 |
202 205 206
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ( 0 [,] +∞ ) ) |
| 208 |
|
ifcl |
⊢ ( ( 𝑀 ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 209 |
207 50 208
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 210 |
209
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) ) |
| 211 |
210
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
| 212 |
|
eldifn |
⊢ ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) |
| 213 |
212
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) |
| 214 |
|
difssd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ⊆ 𝑢 ) |
| 215 |
214
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → 𝑥 ∈ 𝑢 ) |
| 216 |
36 170
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
| 217 |
215 216
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
| 218 |
217
|
con1bid |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) |
| 219 |
213 218
|
mpbid |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) |
| 220 |
|
iftrue |
⊢ ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) ) |
| 221 |
220
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) ) |
| 222 |
215
|
iftrued |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) = 𝑀 ) |
| 223 |
219 221 222
|
3brtr4d |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
| 224 |
|
iffalse |
⊢ ( ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 ) |
| 225 |
224
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 ) |
| 226 |
|
0le0 |
⊢ 0 ≤ 0 |
| 227 |
|
breq2 |
⊢ ( 𝑀 = if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) → ( 0 ≤ 𝑀 ↔ 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
| 228 |
|
breq2 |
⊢ ( 0 = if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
| 229 |
227 228
|
ifboth |
⊢ ( ( 0 ≤ 𝑀 ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
| 230 |
205 226 229
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
| 231 |
230
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
| 232 |
225 231
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
| 233 |
223 232
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
| 234 |
233
|
ralrimivw |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
| 235 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
| 236 |
65 75 210 82 235
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
| 237 |
234 236
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
| 238 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) ) |
| 239 |
76 211 237 238
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) ) |
| 240 |
|
elrege0 |
⊢ ( 𝑀 ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ) |
| 241 |
187 205 240
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ( 0 [,) +∞ ) ) |
| 242 |
|
itg2const |
⊢ ( ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) ∈ ℝ ∧ 𝑀 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) = ( 𝑀 · ( vol ‘ 𝑢 ) ) ) |
| 243 |
10 200 241 242
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) = ( 𝑀 · ( vol ‘ 𝑢 ) ) ) |
| 244 |
239 243
|
breqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( 𝑀 · ( vol ‘ 𝑢 ) ) ) |
| 245 |
203
|
nngt0d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 < 𝑀 ) |
| 246 |
|
ltmuldiv2 |
⊢ ( ( ( vol ‘ 𝑢 ) ∈ ℝ ∧ ( 𝐶 / 2 ) ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → ( ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) |
| 247 |
200 92 187 245 246
|
syl112anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) |
| 248 |
195 247
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) ) |
| 249 |
88 201 92 244 248
|
lelttrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ) |
| 250 |
73 88 92 92 186 249
|
lt2addd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) ) |
| 251 |
89 250
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) ) |
| 252 |
90
|
rpcnd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐶 ∈ ℂ ) |
| 253 |
252
|
2halvesd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) = 𝐶 ) |
| 254 |
251 253
|
breqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) |
| 255 |
254
|
expr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ dom vol ) → ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) |
| 256 |
255
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) |
| 257 |
|
breq2 |
⊢ ( 𝑑 = ( ( 𝐶 / 2 ) / 𝑀 ) → ( ( vol ‘ 𝑢 ) < 𝑑 ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) |
| 258 |
257
|
rspceaimv |
⊢ ( ( ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ+ ∧ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) |
| 259 |
9 256 258
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) |