Metamath Proof Explorer

Theorem itg2cn

Description: A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses itg2cn.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2cn.2 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
itg2cn.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
itg2cn.4 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion itg2cn ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) )

Proof

Step Hyp Ref Expression
1 itg2cn.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
2 itg2cn.2 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
3 itg2cn.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
4 itg2cn.4 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
5 4 rphalfcld ⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ+ )
6 3 5 ltsubrpd ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ 𝐹 ) )
7 5 rpred ⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ )
8 3 7 resubcld ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ∈ ℝ )
9 8 3 ltnled ⊢ ( 𝜑 → ( ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ 𝐹 ) ↔ ¬ ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
10 6 9 mpbid ⊢ ( 𝜑 → ¬ ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
11 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
12 elrege0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
13 11 12 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
14 13 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
15 14 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
16 13 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
17 elxrge0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
18 15 16 17 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
19 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
20 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
21 18 19 20 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
22 21 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
23 22 fmpttd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
24 itg2cl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ* )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ* )
26 25 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) : ℕ ⟶ ℝ* )
27 26 frnd ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ⊆ ℝ* )
28 8 rexrd ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ∈ ℝ* )
29 supxrleub ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ⊆ ℝ* ∧ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ∈ ℝ* ) → ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) , ℝ* , < ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) 𝑧 ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
30 27 28 29 syl2anc ⊢ ( 𝜑 → ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) , ℝ* , < ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) 𝑧 ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
31 1 2 3 itg2cnlem1 ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) , ℝ* , < ) = ( ∫2 ‘ 𝐹 ) )
32 31 breq1d ⊢ ( 𝜑 → ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) , ℝ* , < ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
33 26 ffnd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) Fn ℕ )
34 breq1 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑚 ) → ( 𝑧 ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑚 ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
35 34 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) 𝑧 ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑚 ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
36 breq2 ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) )
37 36 ifbid ⊢ ( 𝑛 = 𝑚 → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
38 37 mpteq2dv ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
39 38 fveq2d ⊢ ( 𝑛 = 𝑚 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
40 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
41 fvex ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ V
42 39 40 41 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑚 ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
43 42 breq1d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑚 ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
44 43 ralbiia ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑚 ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
45 35 44 bitrdi ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) 𝑧 ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
46 33 45 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) 𝑧 ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
47 30 32 46 3bitr3d ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
48 10 47 mtbid ⊢ ( 𝜑 → ¬ ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
49 rexnal ⊢ ( ∃ 𝑚 ∈ ℕ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ¬ ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
50 48 49 sylibr ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
51 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
52 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → 𝐹 ∈ MblFn )
53 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
54 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → 𝐶 ∈ ℝ+ )
55 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → 𝑚 ∈ ℕ )
56 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
57 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
58 57 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
59 58 57 ifbieq1d ⊢ ( 𝑥 = 𝑦 → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) )
60 59 cbvmptv ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) )
61 60 fveq2i ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) )
62 61 breq1i ⊢ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ↔ ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
63 56 62 sylnib ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → ¬ ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
64 51 52 53 54 55 63 itg2cnlem2 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) )
65 elequ1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑢 ↔ 𝑦 ∈ 𝑢 ) )
66 65 57 ifbieq1d ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( 𝑦 ∈ 𝑢 , ( 𝐹 ‘ 𝑦 ) , 0 ) )
67 66 cbvmptv ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( 𝐹 ‘ 𝑦 ) , 0 ) )
68 67 fveq2i ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) )
69 68 breq1i ⊢ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ↔ ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) < 𝐶 )
70 69 imbi2i ⊢ ( ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ↔ ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) )
71 70 ralbii ⊢ ( ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ↔ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) )
72 71 rexbii ⊢ ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ↔ ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) )
73 64 72 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) )
74 50 73 rexlimddv ⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) )