Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2cnlem2 Structured version   Visualization version   GIF version

Theorem itg2cnlem2 23335
 Description: Lemma for itgcn 23415. (Contributed by Mario Carneiro, 31-Aug-2014.)
Hypotheses
Ref Expression
itg2cn.1 (𝜑𝐹:ℝ⟶(0[,)+∞))
itg2cn.2 (𝜑𝐹 ∈ MblFn)
itg2cn.3 (𝜑 → (∫2𝐹) ∈ ℝ)
itg2cn.4 (𝜑𝐶 ∈ ℝ+)
itg2cn.5 (𝜑𝑀 ∈ ℕ)
itg2cn.6 (𝜑 → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)))
Assertion
Ref Expression
itg2cnlem2 (𝜑 → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
Distinct variable groups:   𝑢,𝑑,𝑥,𝐶   𝐹,𝑑,𝑢,𝑥   𝜑,𝑢,𝑥   𝑀,𝑑,𝑢,𝑥
Allowed substitution hint:   𝜑(𝑑)

Proof of Theorem itg2cnlem2
StepHypRef Expression
1 itg2cn.4 . . . 4 (𝜑𝐶 ∈ ℝ+)
21rphalfcld 11760 . . 3 (𝜑 → (𝐶 / 2) ∈ ℝ+)
3 itg2cn.5 . . . 4 (𝜑𝑀 ∈ ℕ)
43nnrpd 11746 . . 3 (𝜑𝑀 ∈ ℝ+)
52, 4rpdivcld 11765 . 2 (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ+)
6 simprl 790 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ∈ dom vol)
7 itg2cn.2 . . . . . . . . . 10 (𝜑𝐹 ∈ MblFn)
87adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 ∈ MblFn)
9 itg2cn.1 . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶(0[,)+∞))
10 rge0ssre 12151 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
11 fss 5969 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
129, 10, 11sylancl 693 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
1312adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶ℝ)
14 mbfima 23205 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
158, 13, 14syl2anc 691 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
16 inmbl 23117 . . . . . . . 8 ((𝑢 ∈ dom vol ∧ (𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
176, 15, 16syl2anc 691 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
18 difmbl 23118 . . . . . . . 8 ((𝑢 ∈ dom vol ∧ (𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
196, 15, 18syl2anc 691 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
20 inass 3785 . . . . . . . . . . 11 ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) = (𝑢 ∩ ((𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))))
21 disjdif 3992 . . . . . . . . . . . 12 ((𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) = ∅
2221ineq2i 3773 . . . . . . . . . . 11 (𝑢 ∩ ((𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))) = (𝑢 ∩ ∅)
23 in0 3920 . . . . . . . . . . 11 (𝑢 ∩ ∅) = ∅
2420, 22, 233eqtri 2636 . . . . . . . . . 10 ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) = ∅
2524fveq2i 6106 . . . . . . . . 9 (vol*‘((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))) = (vol*‘∅)
26 ovol0 23068 . . . . . . . . 9 (vol*‘∅) = 0
2725, 26eqtri 2632 . . . . . . . 8 (vol*‘((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))) = 0
2827a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))) = 0)
29 inundif 3998 . . . . . . . . 9 ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) = 𝑢
3029eqcomi 2619 . . . . . . . 8 𝑢 = ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))
3130a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 = ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))))
32 mblss 23106 . . . . . . . . . 10 (𝑢 ∈ dom vol → 𝑢 ⊆ ℝ)
336, 32syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ⊆ ℝ)
3433sselda 3568 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥𝑢) → 𝑥 ∈ ℝ)
359adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,)+∞))
3635ffvelrnda 6267 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
37 elrege0 12149 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
3836, 37sylib 207 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
3938simpld 474 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
4039rexrd 9968 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ*)
4138simprd 478 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
42 elxrge0 12152 . . . . . . . . 9 ((𝐹𝑥) ∈ (0[,]+∞) ↔ ((𝐹𝑥) ∈ ℝ* ∧ 0 ≤ (𝐹𝑥)))
4340, 41, 42sylanbrc 695 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,]+∞))
4434, 43syldan 486 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥𝑢) → (𝐹𝑥) ∈ (0[,]+∞))
45 eqid 2610 . . . . . . 7 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))
46 eqid 2610 . . . . . . 7 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))
47 eqid 2610 . . . . . . 7 (𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))
48 0e0iccpnf 12154 . . . . . . . . . 10 0 ∈ (0[,]+∞)
49 ifcl 4080 . . . . . . . . . 10 (((𝐹𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
5043, 48, 49sylancl 693 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
5150, 45fmptd 6292 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞))
52 itg2cn.3 . . . . . . . . 9 (𝜑 → (∫2𝐹) ∈ ℝ)
5352adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2𝐹) ∈ ℝ)
54 icossicc 12131 . . . . . . . . . 10 (0[,)+∞) ⊆ (0[,]+∞)
55 fss 5969 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
5635, 54, 55sylancl 693 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,]+∞))
5739leidd 10473 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ≤ (𝐹𝑥))
58 breq1 4586 . . . . . . . . . . . . 13 ((𝐹𝑥) = if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
59 breq1 4586 . . . . . . . . . . . . 13 (0 = if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
6058, 59ifboth 4074 . . . . . . . . . . . 12 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
6157, 41, 60syl2anc 691 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
6261ralrimiva 2949 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
63 reex 9906 . . . . . . . . . . . 12 ℝ ∈ V
6463a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ ∈ V)
65 eqidd 2611 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))
6635feqmptd 6159 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
6764, 50, 39, 65, 66ofrfval2 6813 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
6862, 67mpbird 246 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹)
69 itg2le 23312 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
7051, 56, 68, 69syl3anc 1318 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
71 itg2lecl 23311 . . . . . . . 8 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫2𝐹) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
7251, 53, 70, 71syl3anc 1318 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
73 ifcl 4080 . . . . . . . . . 10 (((𝐹𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
7443, 48, 73sylancl 693 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
7574, 46fmptd 6292 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞))
76 breq1 4586 . . . . . . . . . . . . 13 ((𝐹𝑥) = if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
77 breq1 4586 . . . . . . . . . . . . 13 (0 = if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
7876, 77ifboth 4074 . . . . . . . . . . . 12 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
7957, 41, 78syl2anc 691 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
8079ralrimiva 2949 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
81 eqidd 2611 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))
8264, 74, 39, 81, 66ofrfval2 6813 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
8380, 82mpbird 246 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹)
84 itg2le 23312 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
8575, 56, 83, 84syl3anc 1318 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
86 itg2lecl 23311 . . . . . . . 8 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫2𝐹) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
8775, 53, 85, 86syl3anc 1318 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
8817, 19, 28, 31, 44, 45, 46, 47, 72, 87itg2split 23322 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
891adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℝ+)
9089rphalfcld 11760 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ+)
9190rpred 11748 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ)
92 ifcl 4080 . . . . . . . . . . 11 (((𝐹𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ∈ (0[,]+∞))
9343, 48, 92sylancl 693 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ∈ (0[,]+∞))
94 eqid 2610 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))
9593, 94fmptd 6292 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞))
96 breq1 4586 . . . . . . . . . . . . . 14 ((𝐹𝑥) = if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
97 breq1 4586 . . . . . . . . . . . . . 14 (0 = if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
9896, 97ifboth 4074 . . . . . . . . . . . . 13 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥))
9957, 41, 98syl2anc 691 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥))
10099ralrimiva 2949 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥))
101 eqidd 2611 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)))
10264, 93, 43, 101, 66ofrfval2 6813 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
103100, 102mpbird 246 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) ∘𝑟𝐹)
104 itg2le 23312 . . . . . . . . . 10 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) ∘𝑟𝐹) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ≤ (∫2𝐹))
10595, 56, 103, 104syl3anc 1318 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ≤ (∫2𝐹))
106 itg2lecl 23311 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫2𝐹) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ≤ (∫2𝐹)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ∈ ℝ)
10795, 53, 105, 106syl3anc 1318 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ∈ ℝ)
108 0red 9920 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
109 elinel2 3762 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)))
110109a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
111 ifle 11902 . . . . . . . . . . . 12 ((((𝐹𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ (𝐹𝑥)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))
11239, 108, 41, 110, 111syl31anc 1321 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))
113112ralrimiva 2949 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))
11464, 50, 93, 65, 101ofrfval2 6813 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)))
115113, 114mpbird 246 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)))
116 itg2le 23312 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))))
11751, 95, 115, 116syl3anc 1318 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))))
11866fveq2d 6107 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2𝐹) = (∫2‘(𝑥 ∈ ℝ ↦ (𝐹𝑥))))
119 cmmbl 23109 . . . . . . . . . . . . 13 ((𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
12015, 119syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
121 disjdif 3992 . . . . . . . . . . . . . . 15 ((𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (𝐹 “ (𝑀(,)+∞)))) = ∅
122121fveq2i 6106 . . . . . . . . . . . . . 14 (vol*‘((𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))))) = (vol*‘∅)
123122, 26eqtri 2632 . . . . . . . . . . . . 13 (vol*‘((𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))))) = 0
124123a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))))) = 0)
125 undif2 3996 . . . . . . . . . . . . 13 ((𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (𝐹 “ (𝑀(,)+∞)))) = ((𝐹 “ (𝑀(,)+∞)) ∪ ℝ)
126 mblss 23106 . . . . . . . . . . . . . . 15 ((𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
12715, 126syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
128 ssequn1 3745 . . . . . . . . . . . . . 14 ((𝐹 “ (𝑀(,)+∞)) ⊆ ℝ ↔ ((𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
129127, 128sylib 207 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
130125, 129syl5req 2657 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ = ((𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (𝐹 “ (𝑀(,)+∞)))))
131 eqid 2610 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))
132 iftrue 4042 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → if(𝑥 ∈ ℝ, (𝐹𝑥), 0) = (𝐹𝑥))
133132mpteq2ia 4668 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ (𝐹𝑥))
134133eqcomi 2619 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ (𝐹𝑥)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹𝑥), 0))
135 ifcl 4080 . . . . . . . . . . . . . . 15 (((𝐹𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
13643, 48, 135sylancl 693 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
137136, 131fmptd 6292 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞))
138 breq1 4586 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
139 breq1 4586 . . . . . . . . . . . . . . . . . 18 (0 = if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
140138, 139ifboth 4074 . . . . . . . . . . . . . . . . 17 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
14157, 41, 140syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
142141ralrimiva 2949 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
143 eqidd 2611 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))
14464, 136, 43, 143, 66ofrfval2 6813 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
145142, 144mpbird 246 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹)
146 itg2le 23312 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
147137, 56, 145, 146syl3anc 1318 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
148 itg2lecl 23311 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫2𝐹) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
149137, 53, 147, 148syl3anc 1318 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
15015, 120, 124, 130, 43, 94, 131, 134, 107, 149itg2split 23322 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ (𝐹𝑥))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
151118, 150eqtrd 2644 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2𝐹) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
152 itg2cn.6 . . . . . . . . . . . . . 14 (𝜑 → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)))
153152adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)))
154 eldif 3550 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
155154baib 942 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
156155adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
1579ffnd 5959 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 Fn ℝ)
158157ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
159 elpreima 6245 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (𝑀(,)+∞))))
160158, 159syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (𝑀(,)+∞))))
16139biantrurd 528 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹𝑥) ↔ ((𝐹𝑥) ∈ ℝ ∧ 𝑀 < (𝐹𝑥))))
1623nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℝ)
163162ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ)
164163rexrd 9968 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ*)
165 elioopnf 12138 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℝ* → ((𝐹𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 𝑀 < (𝐹𝑥))))
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 𝑀 < (𝐹𝑥))))
167 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
168167biantrurd 528 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (𝑀(,)+∞) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (𝑀(,)+∞))))
169161, 166, 1683bitr2d 295 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹𝑥) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (𝑀(,)+∞))))
170163, 39ltnled 10063 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹𝑥) ↔ ¬ (𝐹𝑥) ≤ 𝑀))
171160, 169, 1703bitr2rd 296 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ (𝐹𝑥) ≤ 𝑀𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
172171con1bid 344 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)) ↔ (𝐹𝑥) ≤ 𝑀))
173156, 172bitrd 267 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ↔ (𝐹𝑥) ≤ 𝑀))
174173ifbid 4058 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))
175174mpteq2dva 4672 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0)))
176175fveq2d 6107 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))))
177176breq1d 4593 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)) ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2))))
178153, 177mtbird 314 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)))
17953, 91resubcld 10337 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2𝐹) − (𝐶 / 2)) ∈ ℝ)
180179, 149ltnled 10063 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫2𝐹) − (𝐶 / 2)) < (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ↔ ¬ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2))))
181178, 180mpbird 246 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2𝐹) − (𝐶 / 2)) < (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))))
18253, 91, 149ltsubadd2d 10504 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫2𝐹) − (𝐶 / 2)) < (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ↔ (∫2𝐹) < ((𝐶 / 2) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))))))
183181, 182mpbid 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2𝐹) < ((𝐶 / 2) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
184151, 183eqbrtrrd 4607 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))) < ((𝐶 / 2) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
185107, 91, 149ltadd1d 10499 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) < (𝐶 / 2) ↔ ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))) < ((𝐶 / 2) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))))))
186184, 185mpbird 246 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) < (𝐶 / 2))
18772, 107, 91, 117, 186lelttrd 10074 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) < (𝐶 / 2))
188162adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ)
189 mblvol 23105 . . . . . . . . . . 11 (𝑢 ∈ dom vol → (vol‘𝑢) = (vol*‘𝑢))
1906, 189syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) = (vol*‘𝑢))
1915rpred 11748 . . . . . . . . . . . 12 (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ)
192191adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ)
193 simprr 792 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) < ((𝐶 / 2) / 𝑀))
194190, 193eqbrtrrd 4607 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) < ((𝐶 / 2) / 𝑀))
195 ovolcl 23053 . . . . . . . . . . . . . 14 (𝑢 ⊆ ℝ → (vol*‘𝑢) ∈ ℝ*)
19633, 195syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ*)
197192rexrd 9968 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ*)
198 xrltle 11858 . . . . . . . . . . . . 13 (((vol*‘𝑢) ∈ ℝ* ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ*) → ((vol*‘𝑢) < ((𝐶 / 2) / 𝑀) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀)))
199196, 197, 198syl2anc 691 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((vol*‘𝑢) < ((𝐶 / 2) / 𝑀) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀)))
200194, 199mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀))
201 ovollecl 23058 . . . . . . . . . . 11 ((𝑢 ⊆ ℝ ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ ∧ (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀)) → (vol*‘𝑢) ∈ ℝ)
20233, 192, 200, 201syl3anc 1318 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ)
203190, 202eqeltrd 2688 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ)
204188, 203remulcld 9949 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) ∈ ℝ)
205188rexrd 9968 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ*)
2063adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ)
207206nnnn0d 11228 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ0)
208207nn0ge0d 11231 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ 𝑀)
209 elxrge0 12152 . . . . . . . . . . . . . 14 (𝑀 ∈ (0[,]+∞) ↔ (𝑀 ∈ ℝ* ∧ 0 ≤ 𝑀))
210205, 208, 209sylanbrc 695 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,]+∞))
211 ifcl 4080 . . . . . . . . . . . . 13 ((𝑀 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥𝑢, 𝑀, 0) ∈ (0[,]+∞))
212210, 48, 211sylancl 693 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥𝑢, 𝑀, 0) ∈ (0[,]+∞))
213212adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑢, 𝑀, 0) ∈ (0[,]+∞))
214 eqid 2610 . . . . . . . . . . 11 (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))
215213, 214fmptd 6292 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞))
216 eldifn 3695 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) → ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)))
217216adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)))
218 difssd 3700 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) ⊆ 𝑢)
219218sselda 3568 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → 𝑥𝑢)
22034, 171syldan 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥𝑢) → (¬ (𝐹𝑥) ≤ 𝑀𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
221219, 220syldan 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → (¬ (𝐹𝑥) ≤ 𝑀𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
222221con1bid 344 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → (¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)) ↔ (𝐹𝑥) ≤ 𝑀))
223217, 222mpbid 221 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → (𝐹𝑥) ≤ 𝑀)
224 iftrue 4042 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = (𝐹𝑥))
225224adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = (𝐹𝑥))
226219iftrued 4044 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥𝑢, 𝑀, 0) = 𝑀)
227223, 225, 2263brtr4d 4615 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0))
228 iffalse 4045 . . . . . . . . . . . . . . 15 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = 0)
229228adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = 0)
230 0le0 10987 . . . . . . . . . . . . . . . 16 0 ≤ 0
231 breq2 4587 . . . . . . . . . . . . . . . . 17 (𝑀 = if(𝑥𝑢, 𝑀, 0) → (0 ≤ 𝑀 ↔ 0 ≤ if(𝑥𝑢, 𝑀, 0)))
232 breq2 4587 . . . . . . . . . . . . . . . . 17 (0 = if(𝑥𝑢, 𝑀, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥𝑢, 𝑀, 0)))
233231, 232ifboth 4074 . . . . . . . . . . . . . . . 16 ((0 ≤ 𝑀 ∧ 0 ≤ 0) → 0 ≤ if(𝑥𝑢, 𝑀, 0))
234208, 230, 233sylancl 693 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ if(𝑥𝑢, 𝑀, 0))
235234adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → 0 ≤ if(𝑥𝑢, 𝑀, 0))
236229, 235eqbrtrd 4605 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0))
237227, 236pm2.61dan 828 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0))
238237ralrimivw 2950 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0))
239 eqidd 2611 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)))
24064, 74, 213, 81, 239ofrfval2 6813 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0)))
241238, 240mpbird 246 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)))
242 itg2le 23312 . . . . . . . . . 10 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))))
24375, 215, 241, 242syl3anc 1318 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))))
244 elrege0 12149 . . . . . . . . . . 11 (𝑀 ∈ (0[,)+∞) ↔ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀))
245188, 208, 244sylanbrc 695 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,)+∞))
246 itg2const 23313 . . . . . . . . . 10 ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑀 ∈ (0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
2476, 203, 245, 246syl3anc 1318 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
248243, 247breqtrd 4609 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (𝑀 · (vol‘𝑢)))
249206nngt0d 10941 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 < 𝑀)
250 ltmuldiv2 10776 . . . . . . . . . 10 (((vol‘𝑢) ∈ ℝ ∧ (𝐶 / 2) ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
251203, 91, 188, 249, 250syl112anc 1322 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
252193, 251mpbird 246 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) < (𝐶 / 2))
25387, 204, 91, 248, 252lelttrd 10074 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) < (𝐶 / 2))
25472, 87, 91, 91, 187, 253lt2addd 10529 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))) < ((𝐶 / 2) + (𝐶 / 2)))
25588, 254eqbrtrd 4605 . . . . 5 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < ((𝐶 / 2) + (𝐶 / 2)))
25689rpcnd 11750 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℂ)
2572562halvesd 11155 . . . . 5 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
258255, 257breqtrd 4609 . . . 4 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶)
259258expr 641 . . 3 ((𝜑𝑢 ∈ dom vol) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
260259ralrimiva 2949 . 2 (𝜑 → ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
261 breq2 4587 . . . . 5 (𝑑 = ((𝐶 / 2) / 𝑀) → ((vol‘𝑢) < 𝑑 ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
262261imbi1d 330 . . . 4 (𝑑 = ((𝐶 / 2) / 𝑀) → (((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶) ↔ ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶)))
263262ralbidv 2969 . . 3 (𝑑 = ((𝐶 / 2) / 𝑀) → (∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶) ↔ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶)))
264263rspcev 3282 . 2 ((((𝐶 / 2) / 𝑀) ∈ ℝ+ ∧ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶)) → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
2655, 260, 264syl2anc 691 1 (𝜑 → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  ◡ccnv 5037  dom cdm 5038   “ cima 5041   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘𝑟 cofr 6794  ℝcr 9814  0cc0 9815   + caddc 9818   · cmul 9820  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  ℝ+crp 11708  (,)cioo 12046  [,)cico 12048  [,]cicc 12049  vol*covol 23038  volcvol 23039  MblFncmbf 23189  ∫2citg2 23191 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195  df-itg2 23196  df-0p 23243 This theorem is referenced by:  itg2cn  23336
 Copyright terms: Public domain W3C validator