Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itg2gt0cn Structured version   Visualization version   GIF version

Theorem itg2gt0cn 35152
 Description: itg2gt0 24378 holds on functions continuous on an open interval in the absence of ax-cc 9853. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.)
Hypotheses
Ref Expression
itg2gt0cn.2 (𝜑𝑋 < 𝑌)
itg2gt0cn.3 (𝜑𝐹:ℝ⟶(0[,)+∞))
itg2gt0cn.5 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹𝑥))
itg2gt0cn.cn (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
Assertion
Ref Expression
itg2gt0cn (𝜑 → 0 < (∫2𝐹))
Distinct variable groups:   𝑥,𝑋   𝑥,𝑌   𝑥,𝐹   𝜑,𝑥

Proof of Theorem itg2gt0cn
Dummy variables 𝑦 𝑧 𝑤 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0xr 10684 . . 3 0 ∈ ℝ*
2 imassrn 5908 . . . . 5 (𝐹 “ (𝑋(,)𝑌)) ⊆ ran 𝐹
3 itg2gt0cn.3 . . . . . . 7 (𝜑𝐹:ℝ⟶(0[,)+∞))
43frnd 6497 . . . . . 6 (𝜑 → ran 𝐹 ⊆ (0[,)+∞))
5 icossxr 12817 . . . . . 6 (0[,)+∞) ⊆ ℝ*
64, 5sstrdi 3927 . . . . 5 (𝜑 → ran 𝐹 ⊆ ℝ*)
72, 6sstrid 3926 . . . 4 (𝜑 → (𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*)
8 supxrcl 12703 . . . 4 ((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
97, 8syl 17 . . 3 (𝜑 → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
10 itg2gt0cn.2 . . . . . 6 (𝜑𝑋 < 𝑌)
11 ltrelxr 10698 . . . . . . . . . 10 < ⊆ (ℝ* × ℝ*)
1211ssbri 5076 . . . . . . . . 9 (𝑋 < 𝑌𝑋(ℝ* × ℝ*)𝑌)
1310, 12syl 17 . . . . . . . 8 (𝜑𝑋(ℝ* × ℝ*)𝑌)
14 brxp 5566 . . . . . . . 8 (𝑋(ℝ* × ℝ*)𝑌 ↔ (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
1513, 14sylib 221 . . . . . . 7 (𝜑 → (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
16 ioon0 12759 . . . . . . 7 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
1715, 16syl 17 . . . . . 6 (𝜑 → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
1810, 17mpbird 260 . . . . 5 (𝜑 → (𝑋(,)𝑌) ≠ ∅)
19 itg2gt0cn.5 . . . . . 6 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹𝑥))
2019ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
21 r19.2z 4398 . . . . 5 (((𝑋(,)𝑌) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)) → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
2218, 20, 21syl2anc 587 . . . 4 (𝜑 → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
23 supxrlub 12713 . . . . . 6 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
247, 1, 23sylancl 589 . . . . 5 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
253ffnd 6491 . . . . . 6 (𝜑𝐹 Fn ℝ)
26 ioossre 12793 . . . . . 6 (𝑋(,)𝑌) ⊆ ℝ
27 breq2 5035 . . . . . . 7 (𝑦 = (𝐹𝑥) → (0 < 𝑦 ↔ 0 < (𝐹𝑥)))
2827rexima 6982 . . . . . 6 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
2925, 26, 28sylancl 589 . . . . 5 (𝜑 → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3024, 29bitrd 282 . . . 4 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3122, 30mpbird 260 . . 3 (𝜑 → 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))
32 qbtwnxr 12588 . . 3 ((0 ∈ ℝ* ∧ sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ* ∧ 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
331, 9, 31, 32mp3an2i 1463 . 2 (𝜑 → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
34 qre 12348 . . . . . . . . 9 (𝑦 ∈ ℚ → 𝑦 ∈ ℝ)
3534adantr 484 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
36 simpr 488 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 0 < 𝑦)
3735, 36elrpd 12423 . . . . . . 7 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ+)
3837anim1i 617 . . . . . 6 (((𝑦 ∈ ℚ ∧ 0 < 𝑦) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
3938anasss 470 . . . . 5 ((𝑦 ∈ ℚ ∧ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
40 simplr 768 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝑦 ∈ ℝ+)
41 rpxr 12393 . . . . . . . . . . 11 (𝑦 ∈ ℝ+𝑦 ∈ ℝ*)
42 supxrlub 12713 . . . . . . . . . . 11 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*𝑦 ∈ ℝ*) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
437, 41, 42syl2an 598 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
44 breq2 5035 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑥) → (𝑦 < 𝑧𝑦 < (𝐹𝑥)))
4544rexima 6982 . . . . . . . . . . . 12 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4625, 26, 45sylancl 589 . . . . . . . . . . 11 (𝜑 → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4746adantr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4843, 47bitrd 282 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
491a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 ∈ ℝ*)
50 ioorp 12810 . . . . . . . . . . . . . . . . . . 19 (0(,)+∞) = ℝ+
51 ioossicc 12818 . . . . . . . . . . . . . . . . . . 19 (0(,)+∞) ⊆ (0[,]+∞)
5250, 51eqsstrri 3950 . . . . . . . . . . . . . . . . . 18 + ⊆ (0[,]+∞)
5352sseli 3911 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ (0[,]+∞))
54 0e0iccpnf 12844 . . . . . . . . . . . . . . . . 17 0 ∈ (0[,]+∞)
55 ifcl 4469 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5653, 54, 55sylancl 589 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5756adantr 484 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5857fmpttd 6861 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
59 itg2cl 24350 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6058, 59syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6160ad5antlr 734 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
62 ifcl 4469 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6353, 54, 62sylancl 589 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6463adantr 484 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6564fmpttd 6861 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
66 itg2cl 24350 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
6765, 66syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
6867ad5antlr 734 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
69 rpre 12392 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
7069ad4antlr 732 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ ℝ)
71 ioombl 24183 . . . . . . . . . . . . . . . . . 18 (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol
72 mblvol 24148 . . . . . . . . . . . . . . . . . 18 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
7371, 72ax-mp 5 . . . . . . . . . . . . . . . . 17 (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
74 elioore 12763 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ)
7574ad3antlr 730 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ)
76 rpre 12392 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
7776adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈ ℝ)
7875, 77resubcld 11064 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ)
7978adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ)
8078rexrd 10687 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ*)
8180adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ*)
8215simpld 498 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ*)
8382ad5antr 733 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ*)
8415simprd 499 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑌 ∈ ℝ*)
8584ad5antr 733 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑌 ∈ ℝ*)
8682ad4antr 731 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 ∈ ℝ*)
87 xrltnle 10704 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
8880, 86, 87syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
8988biimpar 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) < 𝑋)
9010ad5antr 733 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 < 𝑌)
91 xrre2 12558 . . . . . . . . . . . . . . . . . . . 20 ((((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) < 𝑋𝑋 < 𝑌)) → 𝑋 ∈ ℝ)
9281, 83, 85, 89, 90, 91syl32anc 1375 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ)
9379, 92ifclda 4459 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ)
9484ad5antr 733 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ*)
9577, 75readdcld 10666 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ)
9695adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
97 mnfxr 10694 . . . . . . . . . . . . . . . . . . . . . . 23 -∞ ∈ ℝ*
9897a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -∞ ∈ ℝ*)
99 mnfle 12524 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 ∈ ℝ* → -∞ ≤ 𝑋)
10082, 99syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -∞ ≤ 𝑋)
10198, 82, 84, 100, 10xrlelttrd 12548 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → -∞ < 𝑌)
102101ad5antr 733 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → -∞ < 𝑌)
103 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ≤ (𝑧 + 𝑥))
104 xrre 12557 . . . . . . . . . . . . . . . . . . . 20 (((𝑌 ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ) ∧ (-∞ < 𝑌𝑌 ≤ (𝑧 + 𝑥))) → 𝑌 ∈ ℝ)
10594, 96, 102, 103, 104syl22anc 837 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ)
10695adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
107105, 106ifclda 4459 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ)
10875rexrd 10687 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ*)
10984ad4antr 731 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑌 ∈ ℝ*)
110 rpgt0 12396 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ+ → 0 < 𝑧)
111110adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑧)
11277, 75ltsubposd 11222 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧 ↔ (𝑥𝑧) < 𝑥))
113111, 112mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑥)
114 eliooord 12791 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑥𝑥 < 𝑌))
115114simprd 499 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 < 𝑌)
116115ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < 𝑌)
11780, 108, 109, 113, 116xrlttrd 12547 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑌)
11877, 75ltaddpos2d 11221 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧𝑥 < (𝑧 + 𝑥)))
119111, 118mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < (𝑧 + 𝑥))
12078, 75, 95, 113, 119lttrd 10797 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < (𝑧 + 𝑥))
121 breq2 5035 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < 𝑌 ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
122 breq2 5035 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < (𝑧 + 𝑥) ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
123121, 122ifboth 4463 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑧) < 𝑌 ∧ (𝑥𝑧) < (𝑧 + 𝑥)) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
124117, 120, 123syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
12510ad4antr 731 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑌)
12695rexrd 10687 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ*)
127114simpld 498 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝑋(,)𝑌) → 𝑋 < 𝑥)
128127ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑥)
12986, 108, 126, 128, 119xrlttrd 12547 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < (𝑧 + 𝑥))
130 breq2 5035 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < 𝑌𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
131 breq2 5035 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < (𝑧 + 𝑥) ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
132130, 131ifboth 4463 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 < 𝑌𝑋 < (𝑧 + 𝑥)) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
133125, 129, 132syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
134 breq1 5034 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑧) = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → ((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
135 breq1 5034 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → (𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
136134, 135ifboth 4463 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∧ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
137124, 133, 136syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
13893, 107, 137ltled 10784 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
139 ovolioo 24186 . . . . . . . . . . . . . . . . . 18 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ ∧ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ ∧ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14093, 107, 138, 139syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14173, 140syl5eq 2845 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
142107, 93resubcld 11064 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)) ∈ ℝ)
143141, 142eqeltrd 2890 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ)
144 rpgt0 12396 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → 0 < 𝑦)
145144ad4antlr 732 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑦)
14693, 107posdifd 11223 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋))))
147137, 146mpbid 235 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
148147, 141breqtrrd 5059 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
14970, 143, 145, 148mulgt0d 10791 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
150 iooin 12767 . . . . . . . . . . . . . . . . . . . 20 (((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*)) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
15186, 109, 80, 126, 150syl22anc 837 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
152151eleq2d 2875 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ 𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
153152ifbid 4447 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))
154153mpteq2dv 5127 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)))
155154fveq2d 6654 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))))
156 rpge0 12397 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
157 elrege0 12839 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦))
15869, 156, 157sylanbrc 586 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ (0[,)+∞))
159158ad4antlr 732 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ (0[,)+∞))
160 itg2const 24358 . . . . . . . . . . . . . . . 16 (((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol ∧ (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ ∧ 𝑦 ∈ (0[,)+∞)) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
16171, 143, 159, 160mp3an2i 1463 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
162155, 161eqtrd 2833 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
163149, 162breqtrrd 5059 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
164163adantr 484 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
16558ad5antlr 734 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
16665ad5antlr 734 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
167 fvoveq1 7163 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑤 → (abs‘(𝑢𝑥)) = (abs‘(𝑤𝑥)))
168167breq1d 5041 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑤 → ((abs‘(𝑢𝑥)) < 𝑧 ↔ (abs‘(𝑤𝑥)) < 𝑧))
169168imbrov2fvoveq 7165 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑤 → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ↔ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
170169rspccva 3570 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
171 breq1 5034 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
172 breq1 5034 . . . . . . . . . . . . . . . . . . . . . 22 (0 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
17369leidd 11202 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℝ+𝑦𝑦)
174173ad6antlr 736 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦𝑦)
17574ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑥 ∈ ℝ)
17676ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑧 ∈ ℝ)
177175, 176resubcld 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ)
178177rexrd 10687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ*)
179176, 175readdcld 10666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ)
180179rexrd 10687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ*)
181 elioo2 12774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
182178, 180, 181syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
183 3anass 1092 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
184182, 183syl6bb 290 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
185 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
18674ad5antlr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℝ)
187185, 186resubcld 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑤𝑥) ∈ ℝ)
18876ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℝ)
189187, 188absltd 14788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ (-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧)))
190188renegcld 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → -𝑧 ∈ ℝ)
191186, 190, 185ltaddsub2d 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ -𝑧 < (𝑤𝑥)))
192186recnd 10665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℂ)
193188recnd 10665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℂ)
194192, 193negsubd 10999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑥 + -𝑧) = (𝑥𝑧))
195194breq1d 5041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ (𝑥𝑧) < 𝑤))
196191, 195bitr3d 284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (-𝑧 < (𝑤𝑥) ↔ (𝑥𝑧) < 𝑤))
197185, 186, 188ltsubaddd 11232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑤𝑥) < 𝑧𝑤 < (𝑧 + 𝑥)))
198196, 197anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧) ↔ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
199189, 198bitrd 282 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
200199pm5.32da 582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
201184, 200bitr4d 285 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)))
202201biimpa 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧))
203 pm3.35 802 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘(𝑤𝑥)) < 𝑧 ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
204203ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
20569ad6antlr 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ∈ ℝ)
206 rge0ssre 12841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0[,)+∞) ⊆ ℝ
2073ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
208207ffvelrnda 6833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
209206, 208sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ ℝ)
210209adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑤) ∈ ℝ)
2113adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑦 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
212211ffvelrnda 6833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
213206, 212sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
21474, 213sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℝ)
215214ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
216209, 215resubcld 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑤) − (𝐹𝑥)) ∈ ℝ)
21769ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
218214, 217resubcld 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
219218ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
220216, 219absltd 14788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
221214recnd 10665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℂ)
222 rpcn 12394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
223222ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
224221, 223negsubdi2d 11009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
225224ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
226225breq1d 5041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
227226anbi1d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦)) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
228220, 227bitrd 282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
229228simprbda 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)))
230214ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑥) ∈ ℝ)
231205, 210, 230ltsub1d 11245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 < (𝐹𝑤) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
232229, 231mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 < (𝐹𝑤))
233205, 210, 232ltled 10784 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ≤ (𝐹𝑤))
234204, 233sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
235234an4s 659 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
236202, 235syldan 594 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ (𝐹𝑤))
237236iftrued 4433 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) = 𝑦)
238174, 237breqtrrd 5059 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
239 0le0 11733 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
240 breq2 5035 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 𝑦 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
241 breq2 5035 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
242240, 241ifboth 4463 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ≤ 𝑦 ∧ 0 ≤ 0) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
243156, 239, 242sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℝ+ → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
244243ad6antlr 736 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ ¬ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
245171, 172, 238, 244ifbothda 4462 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
246170, 245sylan2 595 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
247246anassrs 471 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
248 iftrue 4431 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
249248adantl 485 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
250 iftrue 4431 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
251250adantl 485 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
252247, 249, 2513brtr4d 5063 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
253252ex 416 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)))
254239a1i 11 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → 0 ≤ 0)
255 iffalse 4434 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = 0)
256 iffalse 4434 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = 0)
257254, 255, 2563brtr4d 5063 . . . . . . . . . . . . . . . . 17 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
258253, 257pm2.61d1 183 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
259 elin 3897 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))))
260 ifbi 4446 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
261259, 260ax-mp 5 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)
262 ifan 4476 . . . . . . . . . . . . . . . . 17 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
263261, 262eqtri 2821 . . . . . . . . . . . . . . . 16 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
264 fveq2 6650 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑤 → (𝐹𝑣) = (𝐹𝑤))
265264breq2d 5043 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑦 ≤ (𝐹𝑣) ↔ 𝑦 ≤ (𝐹𝑤)))
266265elrab 3628 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)))
267 ifbi 4446 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤))) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0))
268266, 267ax-mp 5 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0)
269 ifan 4476 . . . . . . . . . . . . . . . . 17 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
270268, 269eqtri 2821 . . . . . . . . . . . . . . . 16 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
271258, 263, 2703brtr4g 5065 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
272271ralrimivw 3150 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
273 reex 10624 . . . . . . . . . . . . . . . 16 ℝ ∈ V
274273a1i 11 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ℝ ∈ V)
27556ad6antlr 736 . . . . . . . . . . . . . . 15 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
27663ad6antlr 736 . . . . . . . . . . . . . . 15 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
277 eqidd 2799 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))
278 eqidd 2799 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
279274, 275, 276, 277, 278ofrfval2 7414 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘r ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
280272, 279mpbird 260 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘r ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
281 itg2le 24357 . . . . . . . . . . . . 13 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘r ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
282165, 166, 280, 281syl3anc 1368 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
28349, 61, 68, 164, 282xrltletrd 12549 . . . . . . . . . . 11 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
284 itg2gt0cn.cn . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
285284ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
286 simplr 768 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 𝑥 ∈ (𝑋(,)𝑌))
287 fssres 6521 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:ℝ⟶(0[,)+∞) ∧ (𝑋(,)𝑌) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
28826, 287mpan2 690 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℝ⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
289 fss 6504 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
290206, 289mpan2 690 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
2913, 288, 2903syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
292291adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
293292ffvelrnda 6833 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ∈ ℝ)
294293, 217resubcld 11064 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
295294adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
296217, 293posdifd 11223 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
297296biimpa 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))
298295, 297elrpd 12423 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+)
299 cncfi 23513 . . . . . . . . . . . . . . 15 (((𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ 𝑥 ∈ (𝑋(,)𝑌) ∧ (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
300285, 286, 298, 299syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
301300ex 416 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))))
302 fvres 6669 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
303302breq2d 5043 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑋(,)𝑌) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
304303adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
305 fvres 6669 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
306305adantl 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
307302ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
308306, 307oveq12d 7158 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) = ((𝐹𝑢) − (𝐹𝑥)))
309308fveq2d 6654 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) = (abs‘((𝐹𝑢) − (𝐹𝑥))))
310302oveq1d 7155 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑋(,)𝑌) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
311310ad2antlr 726 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
312309, 311breq12d 5044 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ↔ (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
313312imbi2d 344 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
314313ralbidva 3161 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
315314rexbidv 3256 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
316301, 304, 3153imtr3d 296 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
317316imp 410 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
318283, 317r19.29a 3248 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
319318rexlimdva2 3246 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
32048, 319sylbid 243 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
321320imp 410 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
32265ad2antlr 726 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
323 icossicc 12821 . . . . . . . . . 10 (0[,)+∞) ⊆ (0[,]+∞)
324 fss 6504 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
3253, 323, 324sylancl 589 . . . . . . . . 9 (𝜑𝐹:ℝ⟶(0[,]+∞))
326325ad2antrr 725 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹:ℝ⟶(0[,]+∞))
327 breq1 5034 . . . . . . . . . . . 12 (𝑦 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (𝑦 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
328 breq1 5034 . . . . . . . . . . . 12 (0 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (0 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
329266simprbi 500 . . . . . . . . . . . . 13 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} → 𝑦 ≤ (𝐹𝑤))
330329adantl 485 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 𝑦 ≤ (𝐹𝑤))
3313ffvelrnda 6833 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
332 elrege0 12839 . . . . . . . . . . . . . . 15 ((𝐹𝑤) ∈ (0[,)+∞) ↔ ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
333331, 332sylib 221 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ℝ) → ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
334333simprd 499 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ) → 0 ≤ (𝐹𝑤))
335334adantr 484 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ ¬ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 0 ≤ (𝐹𝑤))
336327, 328, 330, 335ifbothda 4462 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
337336ralrimiva 3149 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
338337ad2antrr 725 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
339273a1i 11 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ℝ ∈ V)
34063ad3antlr 730 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
341 fvexd 6665 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ V)
342 eqidd 2799 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
3433feqmptd 6713 . . . . . . . . . . 11 (𝜑𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
344343ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
345339, 340, 341, 342, 344ofrfval2 7414 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘r𝐹 ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
346338, 345mpbird 260 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘r𝐹)
347 itg2le 24357 . . . . . . . 8 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘r𝐹) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
348322, 326, 346, 347syl3anc 1368 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
34940, 321, 348jca32 519 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
350349expl 461 . . . . 5 (𝜑 → ((𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)))))
35139, 350syl5 34 . . . 4 (𝜑 → ((𝑦 ∈ ℚ ∧ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)))))
352351reximdv2 3230 . . 3 (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
35367adantl 485 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
354 itg2cl 24350 . . . . . . 7 (𝐹:ℝ⟶(0[,]+∞) → (∫2𝐹) ∈ ℝ*)
355325, 354syl 17 . . . . . 6 (𝜑 → (∫2𝐹) ∈ ℝ*)
356355adantr 484 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2𝐹) ∈ ℝ*)
357 xrltletr 12545 . . . . 5 ((0 ∈ ℝ* ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
3581, 353, 356, 357mp3an2i 1463 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
359358rexlimdva 3243 . . 3 (𝜑 → (∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
360352, 359syld 47 . 2 (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2𝐹)))
36133, 360mpd 15 1 (𝜑 → 0 < (∫2𝐹))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ifcif 4425   class class class wbr 5031   ↦ cmpt 5111   × cxp 5518  dom cdm 5520  ran crn 5521   ↾ cres 5522   “ cima 5523   Fn wfn 6322  ⟶wf 6323  ‘cfv 6327  (class class class)co 7140   ∘r cofr 7394  supcsup 8895  ℂcc 10531  ℝcr 10532  0cc0 10533   + caddc 10536   · cmul 10538  +∞cpnf 10668  -∞cmnf 10669  ℝ*cxr 10670   < clt 10671   ≤ cle 10672   − cmin 10866  -cneg 10867  ℚcq 12343  ℝ+crp 12384  (,)cioo 12733  [,)cico 12735  [,]cicc 12736  abscabs 14592  –cn→ccncf 23495  vol*covol 24080  volcvol 24081  ∫2citg2 24234 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7448  ax-inf2 9095  ax-cnex 10589  ax-resscn 10590  ax-1cn 10591  ax-icn 10592  ax-addcl 10593  ax-addrcl 10594  ax-mulcl 10595  ax-mulrcl 10596  ax-mulcom 10597  ax-addass 10598  ax-mulass 10599  ax-distr 10600  ax-i2m1 10601  ax-1ne0 10602  ax-1rid 10603  ax-rnegex 10604  ax-rrecex 10605  ax-cnre 10606  ax-pre-lttri 10607  ax-pre-lttrn 10608  ax-pre-ltadd 10609  ax-pre-mulgt0 10610  ax-pre-sup 10611  ax-addf 10612 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-isom 6336  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7395  df-ofr 7396  df-om 7568  df-1st 7678  df-2nd 7679  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-2o 8093  df-oadd 8096  df-er 8279  df-map 8398  df-pm 8399  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-fi 8866  df-sup 8897  df-inf 8898  df-oi 8965  df-dju 9321  df-card 9359  df-pnf 10673  df-mnf 10674  df-xr 10675  df-ltxr 10676  df-le 10677  df-sub 10868  df-neg 10869  df-div 11294  df-nn 11633  df-2 11695  df-3 11696  df-n0 11893  df-z 11977  df-uz 12239  df-q 12344  df-rp 12385  df-xneg 12502  df-xadd 12503  df-xmul 12504  df-ioo 12737  df-ico 12739  df-icc 12740  df-fz 12893  df-fzo 13036  df-fl 13164  df-seq 13372  df-exp 13433  df-hash 13694  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-clim 14844  df-rlim 14845  df-sum 15042  df-rest 16695  df-topgen 16716  df-psmet 20091  df-xmet 20092  df-met 20093  df-bl 20094  df-mopn 20095  df-top 21513  df-topon 21530  df-bases 21565  df-cmp 22006  df-cncf 23497  df-ovol 24082  df-vol 24083  df-mbf 24237  df-itg1 24238  df-itg2 24239  df-0p 24288 This theorem is referenced by:  itggt0cn  35167
 Copyright terms: Public domain W3C validator