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

Theorem itg2cnlem2 23279
Description: Lemma for itgcn 23359. (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 11718 . . 3 (𝜑 → (𝐶 / 2) ∈ ℝ+)
3 itg2cn.5 . . . 4 (𝜑𝑀 ∈ ℕ)
43nnrpd 11704 . . 3 (𝜑𝑀 ∈ ℝ+)
52, 4rpdivcld 11723 . 2 (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ+)
6 simprl 789 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ∈ dom vol)
7 itg2cn.2 . . . . . . . . . 10 (𝜑𝐹 ∈ MblFn)
87adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 ∈ MblFn)
9 itg2cn.1 . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶(0[,)+∞))
10 rge0ssre 12109 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
11 fss 5954 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
129, 10, 11sylancl 692 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
1312adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶ℝ)
14 mbfima 23149 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
158, 13, 14syl2anc 690 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
16 inmbl 23061 . . . . . . . 8 ((𝑢 ∈ dom vol ∧ (𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
176, 15, 16syl2anc 690 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
18 difmbl 23062 . . . . . . . 8 ((𝑢 ∈ dom vol ∧ (𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
196, 15, 18syl2anc 690 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
20 inass 3784 . . . . . . . . . . 11 ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) = (𝑢 ∩ ((𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))))
21 disjdif 3991 . . . . . . . . . . . 12 ((𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) = ∅
2221ineq2i 3772 . . . . . . . . . . 11 (𝑢 ∩ ((𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))) = (𝑢 ∩ ∅)
23 in0 3919 . . . . . . . . . . 11 (𝑢 ∩ ∅) = ∅
2420, 22, 233eqtri 2635 . . . . . . . . . 10 ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) = ∅
2524fveq2i 6090 . . . . . . . . 9 (vol*‘((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))) = (vol*‘∅)
26 ovol0 23012 . . . . . . . . 9 (vol*‘∅) = 0
2725, 26eqtri 2631 . . . . . . . 8 (vol*‘((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))) = 0
2827a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))) = 0)
29 inundif 3997 . . . . . . . . 9 ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) = 𝑢
3029eqcomi 2618 . . . . . . . 8 𝑢 = ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))))
3130a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 = ((𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))))
32 mblss 23050 . . . . . . . . . 10 (𝑢 ∈ dom vol → 𝑢 ⊆ ℝ)
336, 32syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ⊆ ℝ)
3433sselda 3567 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥𝑢) → 𝑥 ∈ ℝ)
359adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,)+∞))
3635ffvelrnda 6251 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
37 elrege0 12107 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
3836, 37sylib 206 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
3938simpld 473 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
4039rexrd 9945 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ*)
4138simprd 477 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
42 elxrge0 12110 . . . . . . . . 9 ((𝐹𝑥) ∈ (0[,]+∞) ↔ ((𝐹𝑥) ∈ ℝ* ∧ 0 ≤ (𝐹𝑥)))
4340, 41, 42sylanbrc 694 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,]+∞))
4434, 43syldan 485 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥𝑢) → (𝐹𝑥) ∈ (0[,]+∞))
45 eqid 2609 . . . . . . 7 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))
46 eqid 2609 . . . . . . 7 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))
47 eqid 2609 . . . . . . 7 (𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))
48 0e0iccpnf 12112 . . . . . . . . . 10 0 ∈ (0[,]+∞)
49 ifcl 4079 . . . . . . . . . 10 (((𝐹𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
5043, 48, 49sylancl 692 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
5150, 45fmptd 6276 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞))
52 itg2cn.3 . . . . . . . . 9 (𝜑 → (∫2𝐹) ∈ ℝ)
5352adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2𝐹) ∈ ℝ)
54 icossicc 12089 . . . . . . . . . 10 (0[,)+∞) ⊆ (0[,]+∞)
55 fss 5954 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
5635, 54, 55sylancl 692 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,]+∞))
5739leidd 10445 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ≤ (𝐹𝑥))
58 breq1 4580 . . . . . . . . . . . . 13 ((𝐹𝑥) = if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
59 breq1 4580 . . . . . . . . . . . . 13 (0 = if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
6058, 59ifboth 4073 . . . . . . . . . . . 12 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
6157, 41, 60syl2anc 690 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
6261ralrimiva 2948 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
63 reex 9883 . . . . . . . . . . . 12 ℝ ∈ V
6463a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ ∈ V)
65 eqidd 2610 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))
6635feqmptd 6143 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
6764, 50, 39, 65, 66ofrfval2 6790 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
6862, 67mpbird 245 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹)
69 itg2le 23256 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
7051, 56, 68, 69syl3anc 1317 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
71 itg2lecl 23255 . . . . . . . 8 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫2𝐹) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
7251, 53, 70, 71syl3anc 1317 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
73 ifcl 4079 . . . . . . . . . 10 (((𝐹𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
7443, 48, 73sylancl 692 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
7574, 46fmptd 6276 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞))
76 breq1 4580 . . . . . . . . . . . . 13 ((𝐹𝑥) = if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
77 breq1 4580 . . . . . . . . . . . . 13 (0 = if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
7876, 77ifboth 4073 . . . . . . . . . . . 12 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
7957, 41, 78syl2anc 690 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
8079ralrimiva 2948 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
81 eqidd 2610 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))
8264, 74, 39, 81, 66ofrfval2 6790 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
8380, 82mpbird 245 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹)
84 itg2le 23256 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
8575, 56, 83, 84syl3anc 1317 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
86 itg2lecl 23255 . . . . . . . 8 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫2𝐹) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
8775, 53, 85, 86syl3anc 1317 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
8817, 19, 28, 31, 44, 45, 46, 47, 72, 87itg2split 23266 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
891adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℝ+)
9089rphalfcld 11718 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ+)
9190rpred 11706 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ)
92 ifcl 4079 . . . . . . . . . . 11 (((𝐹𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ∈ (0[,]+∞))
9343, 48, 92sylancl 692 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ∈ (0[,]+∞))
94 eqid 2609 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))
9593, 94fmptd 6276 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞))
96 breq1 4580 . . . . . . . . . . . . . 14 ((𝐹𝑥) = if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
97 breq1 4580 . . . . . . . . . . . . . 14 (0 = if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
9896, 97ifboth 4073 . . . . . . . . . . . . 13 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥))
9957, 41, 98syl2anc 690 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥))
10099ralrimiva 2948 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥))
101 eqidd 2610 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)))
10264, 93, 43, 101, 66ofrfval2 6790 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
103100, 102mpbird 245 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) ∘𝑟𝐹)
104 itg2le 23256 . . . . . . . . . 10 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) ∘𝑟𝐹) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ≤ (∫2𝐹))
10595, 56, 103, 104syl3anc 1317 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ≤ (∫2𝐹))
106 itg2lecl 23255 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫2𝐹) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ≤ (∫2𝐹)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ∈ ℝ)
10795, 53, 105, 106syl3anc 1317 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) ∈ ℝ)
108 0red 9897 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
109 elinel2 3761 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)))
110109a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
111 ifle 11863 . . . . . . . . . . . 12 ((((𝐹𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ (𝐹𝑥)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))
11239, 108, 41, 110, 111syl31anc 1320 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))
113112ralrimiva 2948 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))
11464, 50, 93, 65, 101ofrfval2 6790 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)))
115113, 114mpbird 245 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)))
116 itg2le 23256 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))))
11751, 95, 115, 116syl3anc 1317 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))))
11866fveq2d 6091 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2𝐹) = (∫2‘(𝑥 ∈ ℝ ↦ (𝐹𝑥))))
119 cmmbl 23053 . . . . . . . . . . . . 13 ((𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
12015, 119syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
121 disjdif 3991 . . . . . . . . . . . . . . 15 ((𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (𝐹 “ (𝑀(,)+∞)))) = ∅
122121fveq2i 6090 . . . . . . . . . . . . . 14 (vol*‘((𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))))) = (vol*‘∅)
123122, 26eqtri 2631 . . . . . . . . . . . . 13 (vol*‘((𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))))) = 0
124123a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))))) = 0)
125 undif2 3995 . . . . . . . . . . . . 13 ((𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (𝐹 “ (𝑀(,)+∞)))) = ((𝐹 “ (𝑀(,)+∞)) ∪ ℝ)
126 mblss 23050 . . . . . . . . . . . . . . 15 ((𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
12715, 126syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
128 ssequn1 3744 . . . . . . . . . . . . . 14 ((𝐹 “ (𝑀(,)+∞)) ⊆ ℝ ↔ ((𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
129127, 128sylib 206 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
130125, 129syl5req 2656 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ = ((𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (𝐹 “ (𝑀(,)+∞)))))
131 eqid 2609 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))
132 iftrue 4041 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → if(𝑥 ∈ ℝ, (𝐹𝑥), 0) = (𝐹𝑥))
133132mpteq2ia 4662 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ (𝐹𝑥))
134133eqcomi 2618 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ (𝐹𝑥)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹𝑥), 0))
135 ifcl 4079 . . . . . . . . . . . . . . 15 (((𝐹𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
13643, 48, 135sylancl 692 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ∈ (0[,]+∞))
137136, 131fmptd 6276 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞))
138 breq1 4580 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
139 breq1 4580 . . . . . . . . . . . . . . . . . 18 (0 = if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
140138, 139ifboth 4073 . . . . . . . . . . . . . . . . 17 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
14157, 41, 140syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
142141ralrimiva 2948 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥))
143 eqidd 2610 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))
14464, 136, 43, 143, 66ofrfval2 6790 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ (𝐹𝑥)))
145142, 144mpbird 245 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹)
146 itg2le 23256 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟𝐹) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
147137, 56, 145, 146syl3anc 1317 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹))
148 itg2lecl 23255 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫2𝐹) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2𝐹)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
149137, 53, 147, 148syl3anc 1317 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ∈ ℝ)
15015, 120, 124, 130, 43, 94, 131, 134, 107, 149itg2split 23266 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ (𝐹𝑥))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
151118, 150eqtrd 2643 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2𝐹) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
152 itg2cn.6 . . . . . . . . . . . . . 14 (𝜑 → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)))
153152adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)))
154 eldif 3549 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
155154baib 941 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
156155adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
1579ffnd 5944 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 Fn ℝ)
158157ad2antrr 757 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
159 elpreima 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (𝑀(,)+∞))))
160158, 159syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (𝑀(,)+∞))))
16139biantrurd 527 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹𝑥) ↔ ((𝐹𝑥) ∈ ℝ ∧ 𝑀 < (𝐹𝑥))))
1623nnred 10884 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℝ)
163162ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ)
164163rexrd 9945 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ*)
165 elioopnf 12096 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℝ* → ((𝐹𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 𝑀 < (𝐹𝑥))))
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 𝑀 < (𝐹𝑥))))
167 simpr 475 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
168167biantrurd 527 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (𝑀(,)+∞) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (𝑀(,)+∞))))
169161, 166, 1683bitr2d 294 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹𝑥) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (𝑀(,)+∞))))
170163, 39ltnled 10035 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹𝑥) ↔ ¬ (𝐹𝑥) ≤ 𝑀))
171160, 169, 1703bitr2rd 295 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ (𝐹𝑥) ≤ 𝑀𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
172171con1bid 343 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)) ↔ (𝐹𝑥) ≤ 𝑀))
173156, 172bitrd 266 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))) ↔ (𝐹𝑥) ≤ 𝑀))
174173ifbid 4057 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))
175174mpteq2dva 4666 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0)))
176175fveq2d 6091 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))))
177176breq1d 4587 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)) ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑀, (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2))))
178153, 177mtbird 313 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2)))
17953, 91resubcld 10309 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2𝐹) − (𝐶 / 2)) ∈ ℝ)
180179, 149ltnled 10035 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫2𝐹) − (𝐶 / 2)) < (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ↔ ¬ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ ((∫2𝐹) − (𝐶 / 2))))
181178, 180mpbird 245 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2𝐹) − (𝐶 / 2)) < (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))))
18253, 91, 149ltsubadd2d 10476 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫2𝐹) − (𝐶 / 2)) < (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ↔ (∫2𝐹) < ((𝐶 / 2) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))))))
183181, 182mpbid 220 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2𝐹) < ((𝐶 / 2) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
184151, 183eqbrtrrd 4601 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))) < ((𝐶 / 2) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))))
185107, 91, 149ltadd1d 10471 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) < (𝐶 / 2) ↔ ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))) < ((𝐶 / 2) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))))))
186184, 185mpbird 245 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐹 “ (𝑀(,)+∞)), (𝐹𝑥), 0))) < (𝐶 / 2))
18772, 107, 91, 117, 186lelttrd 10046 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) < (𝐶 / 2))
188162adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ)
189 mblvol 23049 . . . . . . . . . . 11 (𝑢 ∈ dom vol → (vol‘𝑢) = (vol*‘𝑢))
1906, 189syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) = (vol*‘𝑢))
1915rpred 11706 . . . . . . . . . . . 12 (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ)
192191adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ)
193 simprr 791 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) < ((𝐶 / 2) / 𝑀))
194190, 193eqbrtrrd 4601 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) < ((𝐶 / 2) / 𝑀))
195 ovolcl 22997 . . . . . . . . . . . . . 14 (𝑢 ⊆ ℝ → (vol*‘𝑢) ∈ ℝ*)
19633, 195syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ*)
197192rexrd 9945 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ*)
198 xrltle 11819 . . . . . . . . . . . . 13 (((vol*‘𝑢) ∈ ℝ* ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ*) → ((vol*‘𝑢) < ((𝐶 / 2) / 𝑀) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀)))
199196, 197, 198syl2anc 690 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((vol*‘𝑢) < ((𝐶 / 2) / 𝑀) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀)))
200194, 199mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀))
201 ovollecl 23002 . . . . . . . . . . 11 ((𝑢 ⊆ ℝ ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ ∧ (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀)) → (vol*‘𝑢) ∈ ℝ)
20233, 192, 200, 201syl3anc 1317 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ)
203190, 202eqeltrd 2687 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ)
204188, 203remulcld 9926 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) ∈ ℝ)
205188rexrd 9945 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ*)
2063adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ)
207206nnnn0d 11200 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ0)
208207nn0ge0d 11203 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ 𝑀)
209 elxrge0 12110 . . . . . . . . . . . . . 14 (𝑀 ∈ (0[,]+∞) ↔ (𝑀 ∈ ℝ* ∧ 0 ≤ 𝑀))
210205, 208, 209sylanbrc 694 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,]+∞))
211 ifcl 4079 . . . . . . . . . . . . 13 ((𝑀 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥𝑢, 𝑀, 0) ∈ (0[,]+∞))
212210, 48, 211sylancl 692 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥𝑢, 𝑀, 0) ∈ (0[,]+∞))
213212adantr 479 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥𝑢, 𝑀, 0) ∈ (0[,]+∞))
214 eqid 2609 . . . . . . . . . . 11 (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))
215213, 214fmptd 6276 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞))
216 eldifn 3694 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) → ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)))
217216adantl 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → ¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)))
218 difssd 3699 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) ⊆ 𝑢)
219218sselda 3567 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → 𝑥𝑢)
22034, 171syldan 485 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥𝑢) → (¬ (𝐹𝑥) ≤ 𝑀𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
221219, 220syldan 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → (¬ (𝐹𝑥) ≤ 𝑀𝑥 ∈ (𝐹 “ (𝑀(,)+∞))))
222221con1bid 343 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → (¬ 𝑥 ∈ (𝐹 “ (𝑀(,)+∞)) ↔ (𝐹𝑥) ≤ 𝑀))
223217, 222mpbid 220 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → (𝐹𝑥) ≤ 𝑀)
224 iftrue 4041 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = (𝐹𝑥))
225224adantl 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = (𝐹𝑥))
226219iftrued 4043 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥𝑢, 𝑀, 0) = 𝑀)
227223, 225, 2263brtr4d 4609 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0))
228 iffalse 4044 . . . . . . . . . . . . . . 15 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = 0)
229228adantl 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) = 0)
230 0le0 10959 . . . . . . . . . . . . . . . 16 0 ≤ 0
231 breq2 4581 . . . . . . . . . . . . . . . . 17 (𝑀 = if(𝑥𝑢, 𝑀, 0) → (0 ≤ 𝑀 ↔ 0 ≤ if(𝑥𝑢, 𝑀, 0)))
232 breq2 4581 . . . . . . . . . . . . . . . . 17 (0 = if(𝑥𝑢, 𝑀, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥𝑢, 𝑀, 0)))
233231, 232ifboth 4073 . . . . . . . . . . . . . . . 16 ((0 ≤ 𝑀 ∧ 0 ≤ 0) → 0 ≤ if(𝑥𝑢, 𝑀, 0))
234208, 230, 233sylancl 692 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ if(𝑥𝑢, 𝑀, 0))
235234adantr 479 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → 0 ≤ if(𝑥𝑢, 𝑀, 0))
236229, 235eqbrtrd 4599 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0))
237227, 236pm2.61dan 827 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0))
238237ralrimivw 2949 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0))
239 eqidd 2610 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)))
24064, 74, 213, 81, 239ofrfval2 6790 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0) ≤ if(𝑥𝑢, 𝑀, 0)))
241238, 240mpbird 245 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)))
242 itg2le 23256 . . . . . . . . . 10 (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))))
24375, 215, 241, 242syl3anc 1317 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))))
244 elrege0 12107 . . . . . . . . . . 11 (𝑀 ∈ (0[,)+∞) ↔ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀))
245188, 208, 244sylanbrc 694 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,)+∞))
246 itg2const 23257 . . . . . . . . . 10 ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑀 ∈ (0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
2476, 203, 245, 246syl3anc 1317 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
248243, 247breqtrd 4603 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) ≤ (𝑀 · (vol‘𝑢)))
249206nngt0d 10913 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 < 𝑀)
250 ltmuldiv2 10748 . . . . . . . . . 10 (((vol‘𝑢) ∈ ℝ ∧ (𝐶 / 2) ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
251203, 91, 188, 249, 250syl112anc 1321 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
252193, 251mpbird 245 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) < (𝐶 / 2))
25387, 204, 91, 248, 252lelttrd 10046 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) < (𝐶 / 2))
25472, 87, 91, 91, 187, 253lt2addd 10501 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (𝐹 “ (𝑀(,)+∞))), (𝐹𝑥), 0)))) < ((𝐶 / 2) + (𝐶 / 2)))
25588, 254eqbrtrd 4599 . . . . 5 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < ((𝐶 / 2) + (𝐶 / 2)))
25689rpcnd 11708 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℂ)
2572562halvesd 11127 . . . . 5 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
258255, 257breqtrd 4603 . . . 4 ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶)
259258expr 640 . . 3 ((𝜑𝑢 ∈ dom vol) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
260259ralrimiva 2948 . 2 (𝜑 → ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
261 breq2 4581 . . . . 5 (𝑑 = ((𝐶 / 2) / 𝑀) → ((vol‘𝑢) < 𝑑 ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
262261imbi1d 329 . . . 4 (𝑑 = ((𝐶 / 2) / 𝑀) → (((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶) ↔ ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶)))
263262ralbidv 2968 . . 3 (𝑑 = ((𝐶 / 2) / 𝑀) → (∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶) ↔ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶)))
264263rspcev 3281 . 2 ((((𝐶 / 2) / 𝑀) ∈ ℝ+ ∧ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶)) → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
2655, 260, 264syl2anc 690 1 (𝜑 → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝑢, (𝐹𝑥), 0))) < 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895  wrex 2896  Vcvv 3172  cdif 3536  cun 3537  cin 3538  wss 3539  c0 3873  ifcif 4035   class class class wbr 4577  cmpt 4637  ccnv 5026  dom cdm 5027  cima 5030   Fn wfn 5784  wf 5785  cfv 5789  (class class class)co 6526  𝑟 cofr 6771  cr 9791  0cc0 9792   + caddc 9795   · cmul 9797  +∞cpnf 9927  *cxr 9929   < clt 9930  cle 9931  cmin 10117   / cdiv 10535  cn 10869  2c2 10919  +crp 11666  (,)cioo 12004  [,)cico 12006  [,]cicc 12007  vol*covol 22982  volcvol 22983  MblFncmbf 23133  2citg2 23135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-se 4987  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-isom 5798  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-of 6772  df-ofr 6773  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-n0 11142  df-z 11213  df-uz 11522  df-q 11623  df-rp 11667  df-xneg 11780  df-xadd 11781  df-xmul 11782  df-ioo 12008  df-ico 12010  df-icc 12011  df-fz 12155  df-fzo 12292  df-fl 12412  df-seq 12621  df-exp 12680  df-hash 12937  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772  df-clim 14015  df-sum 14213  df-rest 15854  df-topgen 15875  df-psmet 19507  df-xmet 19508  df-met 19509  df-bl 19510  df-mopn 19511  df-top 20468  df-bases 20469  df-topon 20470  df-cmp 20947  df-ovol 22984  df-vol 22985  df-mbf 23138  df-itg1 23139  df-itg2 23140  df-0p 23187
This theorem is referenced by:  itg2cn  23280
  Copyright terms: Public domain W3C validator