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

Theorem itg2gt0cn 35569
Description: itg2gt0 24658 holds on functions continuous on an open interval in the absence of ax-cc 10049. 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 10880 . . 3 0 ∈ ℝ*
2 imassrn 5940 . . . . 5 (𝐹 “ (𝑋(,)𝑌)) ⊆ ran 𝐹
3 itg2gt0cn.3 . . . . . . 7 (𝜑𝐹:ℝ⟶(0[,)+∞))
43frnd 6553 . . . . . 6 (𝜑 → ran 𝐹 ⊆ (0[,)+∞))
5 icossxr 13020 . . . . . 6 (0[,)+∞) ⊆ ℝ*
64, 5sstrdi 3913 . . . . 5 (𝜑 → ran 𝐹 ⊆ ℝ*)
72, 6sstrid 3912 . . . 4 (𝜑 → (𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*)
8 supxrcl 12905 . . . 4 ((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
97, 8syl 17 . . 3 (𝜑 → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
10 itg2gt0cn.2 . . . . . 6 (𝜑𝑋 < 𝑌)
11 ltrelxr 10894 . . . . . . . . . 10 < ⊆ (ℝ* × ℝ*)
1211ssbri 5098 . . . . . . . . 9 (𝑋 < 𝑌𝑋(ℝ* × ℝ*)𝑌)
1310, 12syl 17 . . . . . . . 8 (𝜑𝑋(ℝ* × ℝ*)𝑌)
14 brxp 5598 . . . . . . . 8 (𝑋(ℝ* × ℝ*)𝑌 ↔ (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
1513, 14sylib 221 . . . . . . 7 (𝜑 → (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
16 ioon0 12961 . . . . . . 7 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
1715, 16syl 17 . . . . . 6 (𝜑 → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
1810, 17mpbird 260 . . . . 5 (𝜑 → (𝑋(,)𝑌) ≠ ∅)
19 itg2gt0cn.5 . . . . . 6 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹𝑥))
2019ralrimiva 3105 . . . . 5 (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
21 r19.2z 4406 . . . . 5 (((𝑋(,)𝑌) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)) → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
2218, 20, 21syl2anc 587 . . . 4 (𝜑 → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
23 supxrlub 12915 . . . . . 6 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
247, 1, 23sylancl 589 . . . . 5 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
253ffnd 6546 . . . . . 6 (𝜑𝐹 Fn ℝ)
26 ioossre 12996 . . . . . 6 (𝑋(,)𝑌) ⊆ ℝ
27 breq2 5057 . . . . . . 7 (𝑦 = (𝐹𝑥) → (0 < 𝑦 ↔ 0 < (𝐹𝑥)))
2827rexima 7053 . . . . . 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 12790 . . 3 ((0 ∈ ℝ* ∧ sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ* ∧ 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
331, 9, 31, 32mp3an2i 1468 . 2 (𝜑 → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
34 qre 12549 . . . . . . . . 9 (𝑦 ∈ ℚ → 𝑦 ∈ ℝ)
3534adantr 484 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
36 simpr 488 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 0 < 𝑦)
3735, 36elrpd 12625 . . . . . . 7 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ+)
3837anim1i 618 . . . . . 6 (((𝑦 ∈ ℚ ∧ 0 < 𝑦) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
3938anasss 470 . . . . 5 ((𝑦 ∈ ℚ ∧ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
40 simplr 769 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝑦 ∈ ℝ+)
41 rpxr 12595 . . . . . . . . . . 11 (𝑦 ∈ ℝ+𝑦 ∈ ℝ*)
42 supxrlub 12915 . . . . . . . . . . 11 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*𝑦 ∈ ℝ*) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
437, 41, 42syl2an 599 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
44 breq2 5057 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑥) → (𝑦 < 𝑧𝑦 < (𝐹𝑥)))
4544rexima 7053 . . . . . . . . . . . 12 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4625, 26, 45sylancl 589 . . . . . . . . . . 11 (𝜑 → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4746adantr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4843, 47bitrd 282 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
491a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 ∈ ℝ*)
50 ioorp 13013 . . . . . . . . . . . . . . . . . . 19 (0(,)+∞) = ℝ+
51 ioossicc 13021 . . . . . . . . . . . . . . . . . . 19 (0(,)+∞) ⊆ (0[,]+∞)
5250, 51eqsstrri 3936 . . . . . . . . . . . . . . . . . 18 + ⊆ (0[,]+∞)
5352sseli 3896 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ (0[,]+∞))
54 0e0iccpnf 13047 . . . . . . . . . . . . . . . . 17 0 ∈ (0[,]+∞)
55 ifcl 4484 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5653, 54, 55sylancl 589 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5756adantr 484 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5857fmpttd 6932 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
59 itg2cl 24630 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6058, 59syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6160ad5antlr 735 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
62 ifcl 4484 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6353, 54, 62sylancl 589 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6463adantr 484 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6564fmpttd 6932 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
66 itg2cl 24630 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
6765, 66syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
6867ad5antlr 735 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
69 rpre 12594 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
7069ad4antlr 733 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ ℝ)
71 ioombl 24462 . . . . . . . . . . . . . . . . . 18 (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol
72 mblvol 24427 . . . . . . . . . . . . . . . . . 18 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
7371, 72ax-mp 5 . . . . . . . . . . . . . . . . 17 (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
74 elioore 12965 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ)
7574ad3antlr 731 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ)
76 rpre 12594 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
7776adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈ ℝ)
7875, 77resubcld 11260 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ)
7978adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ)
8078rexrd 10883 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ*)
8180adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ*)
8215simpld 498 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ*)
8382ad5antr 734 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ*)
8415simprd 499 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑌 ∈ ℝ*)
8584ad5antr 734 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑌 ∈ ℝ*)
8682ad4antr 732 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 ∈ ℝ*)
87 xrltnle 10900 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
8880, 86, 87syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
8988biimpar 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) < 𝑋)
9010ad5antr 734 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 < 𝑌)
91 xrre2 12760 . . . . . . . . . . . . . . . . . . . 20 ((((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) < 𝑋𝑋 < 𝑌)) → 𝑋 ∈ ℝ)
9281, 83, 85, 89, 90, 91syl32anc 1380 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ)
9379, 92ifclda 4474 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ)
9484ad5antr 734 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ*)
9577, 75readdcld 10862 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ)
9695adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
97 mnfxr 10890 . . . . . . . . . . . . . . . . . . . . . . 23 -∞ ∈ ℝ*
9897a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -∞ ∈ ℝ*)
99 mnfle 12726 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 ∈ ℝ* → -∞ ≤ 𝑋)
10082, 99syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -∞ ≤ 𝑋)
10198, 82, 84, 100, 10xrlelttrd 12750 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → -∞ < 𝑌)
102101ad5antr 734 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → -∞ < 𝑌)
103 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ≤ (𝑧 + 𝑥))
104 xrre 12759 . . . . . . . . . . . . . . . . . . . 20 (((𝑌 ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ) ∧ (-∞ < 𝑌𝑌 ≤ (𝑧 + 𝑥))) → 𝑌 ∈ ℝ)
10594, 96, 102, 103, 104syl22anc 839 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ)
10695adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
107105, 106ifclda 4474 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ)
10875rexrd 10883 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ*)
10984ad4antr 732 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑌 ∈ ℝ*)
110 rpgt0 12598 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ+ → 0 < 𝑧)
111110adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑧)
11277, 75ltsubposd 11418 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧 ↔ (𝑥𝑧) < 𝑥))
113111, 112mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑥)
114 eliooord 12994 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑥𝑥 < 𝑌))
115114simprd 499 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 < 𝑌)
116115ad3antlr 731 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < 𝑌)
11780, 108, 109, 113, 116xrlttrd 12749 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑌)
11877, 75ltaddpos2d 11417 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧𝑥 < (𝑧 + 𝑥)))
119111, 118mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < (𝑧 + 𝑥))
12078, 75, 95, 113, 119lttrd 10993 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < (𝑧 + 𝑥))
121 breq2 5057 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < 𝑌 ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
122 breq2 5057 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < (𝑧 + 𝑥) ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
123121, 122ifboth 4478 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑧) < 𝑌 ∧ (𝑥𝑧) < (𝑧 + 𝑥)) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
124117, 120, 123syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
12510ad4antr 732 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑌)
12695rexrd 10883 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ*)
127114simpld 498 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝑋(,)𝑌) → 𝑋 < 𝑥)
128127ad3antlr 731 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑥)
12986, 108, 126, 128, 119xrlttrd 12749 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < (𝑧 + 𝑥))
130 breq2 5057 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < 𝑌𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
131 breq2 5057 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < (𝑧 + 𝑥) ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
132130, 131ifboth 4478 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 < 𝑌𝑋 < (𝑧 + 𝑥)) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
133125, 129, 132syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
134 breq1 5056 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑧) = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → ((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
135 breq1 5056 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → (𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
136134, 135ifboth 4478 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∧ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
137124, 133, 136syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
13893, 107, 137ltled 10980 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
139 ovolioo 24465 . . . . . . . . . . . . . . . . . 18 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ ∧ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ ∧ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14093, 107, 138, 139syl3anc 1373 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14173, 140syl5eq 2790 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
142107, 93resubcld 11260 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)) ∈ ℝ)
143141, 142eqeltrd 2838 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ)
144 rpgt0 12598 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → 0 < 𝑦)
145144ad4antlr 733 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑦)
14693, 107posdifd 11419 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋))))
147137, 146mpbid 235 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
148147, 141breqtrrd 5081 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
14970, 143, 145, 148mulgt0d 10987 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
150 iooin 12969 . . . . . . . . . . . . . . . . . . . 20 (((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*)) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
15186, 109, 80, 126, 150syl22anc 839 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
152151eleq2d 2823 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ 𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
153152ifbid 4462 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))
154153mpteq2dv 5151 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)))
155154fveq2d 6721 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))))
156 rpge0 12599 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
157 elrege0 13042 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦))
15869, 156, 157sylanbrc 586 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ (0[,)+∞))
159158ad4antlr 733 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ (0[,)+∞))
160 itg2const 24638 . . . . . . . . . . . . . . . 16 (((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol ∧ (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ ∧ 𝑦 ∈ (0[,)+∞)) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
16171, 143, 159, 160mp3an2i 1468 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
162155, 161eqtrd 2777 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
163149, 162breqtrrd 5081 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
164163adantr 484 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
16558ad5antlr 735 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
16665ad5antlr 735 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
167 fvoveq1 7236 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑤 → (abs‘(𝑢𝑥)) = (abs‘(𝑤𝑥)))
168167breq1d 5063 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑤 → ((abs‘(𝑢𝑥)) < 𝑧 ↔ (abs‘(𝑤𝑥)) < 𝑧))
169168imbrov2fvoveq 7238 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑤 → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ↔ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
170169rspccva 3536 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
171 breq1 5056 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
172 breq1 5056 . . . . . . . . . . . . . . . . . . . . . 22 (0 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
17369leidd 11398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℝ+𝑦𝑦)
174173ad6antlr 737 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦𝑦)
17574ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑥 ∈ ℝ)
17676ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑧 ∈ ℝ)
177175, 176resubcld 11260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ)
178177rexrd 10883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ*)
179176, 175readdcld 10862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ)
180179rexrd 10883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ*)
181 elioo2 12976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
182178, 180, 181syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
183 3anass 1097 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
184182, 183bitrdi 290 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
185 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
18674ad5antlr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℝ)
187185, 186resubcld 11260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑤𝑥) ∈ ℝ)
18876ad3antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℝ)
189187, 188absltd 14993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ (-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧)))
190188renegcld 11259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → -𝑧 ∈ ℝ)
191186, 190, 185ltaddsub2d 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ -𝑧 < (𝑤𝑥)))
192186recnd 10861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℂ)
193188recnd 10861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℂ)
194192, 193negsubd 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑥 + -𝑧) = (𝑥𝑧))
195194breq1d 5063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ (𝑥𝑧) < 𝑤))
196191, 195bitr3d 284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (-𝑧 < (𝑤𝑥) ↔ (𝑥𝑧) < 𝑤))
197185, 186, 188ltsubaddd 11428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑤𝑥) < 𝑧𝑤 < (𝑧 + 𝑥)))
198196, 197anbi12d 634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 803 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘(𝑤𝑥)) < 𝑧 ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
204203ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
20569ad6antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ∈ ℝ)
206 rge0ssre 13044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0[,)+∞) ⊆ ℝ
2073ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
208207ffvelrnda 6904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
209206, 208sseldi 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ ℝ)
210209adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑤) ∈ ℝ)
2113adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑦 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
212211ffvelrnda 6904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
213206, 212sseldi 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
21474, 213sylan2 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℝ)
215214ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
216209, 215resubcld 11260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑤) − (𝐹𝑥)) ∈ ℝ)
21769ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
218214, 217resubcld 11260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
219218ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
220216, 219absltd 14993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
221214recnd 10861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℂ)
222 rpcn 12596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
223222ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
224221, 223negsubdi2d 11205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
225224ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
226225breq1d 5063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
227226anbi1d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦)) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
228220, 227bitrd 282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
229228simprbda 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)))
230214ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑥) ∈ ℝ)
231205, 210, 230ltsub1d 11441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 < (𝐹𝑤) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
232229, 231mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 < (𝐹𝑤))
233205, 210, 232ltled 10980 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ≤ (𝐹𝑤))
234204, 233sylan2 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
235234an4s 660 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
236202, 235syldan 594 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ (𝐹𝑤))
237236iftrued 4447 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) = 𝑦)
238174, 237breqtrrd 5081 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
239 0le0 11931 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
240 breq2 5057 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 𝑦 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
241 breq2 5057 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
242240, 241ifboth 4478 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ≤ 𝑦 ∧ 0 ≤ 0) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
243156, 239, 242sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℝ+ → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
244243ad6antlr 737 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ ¬ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
245171, 172, 238, 244ifbothda 4477 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
246170, 245sylan2 596 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
247246anassrs 471 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
248 iftrue 4445 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
249248adantl 485 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
250 iftrue 4445 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
251250adantl 485 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
252247, 249, 2513brtr4d 5085 . . . . . . . . . . . . . . . . . 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 4448 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = 0)
256 iffalse 4448 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = 0)
257254, 255, 2563brtr4d 5085 . . . . . . . . . . . . . . . . 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 3882 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))))
260 ifbi 4461 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
261259, 260ax-mp 5 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)
262 ifan 4492 . . . . . . . . . . . . . . . . 17 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
263261, 262eqtri 2765 . . . . . . . . . . . . . . . 16 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
264 fveq2 6717 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑤 → (𝐹𝑣) = (𝐹𝑤))
265264breq2d 5065 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑦 ≤ (𝐹𝑣) ↔ 𝑦 ≤ (𝐹𝑤)))
266265elrab 3602 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)))
267 ifbi 4461 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤))) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0))
268266, 267ax-mp 5 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0)
269 ifan 4492 . . . . . . . . . . . . . . . . 17 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
270268, 269eqtri 2765 . . . . . . . . . . . . . . . 16 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
271258, 263, 2703brtr4g 5087 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
272271ralrimivw 3106 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
273 reex 10820 . . . . . . . . . . . . . . . 16 ℝ ∈ V
274273a1i 11 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ℝ ∈ V)
27556ad6antlr 737 . . . . . . . . . . . . . . 15 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
27663ad6antlr 737 . . . . . . . . . . . . . . 15 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
277 eqidd 2738 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))
278 eqidd 2738 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
279274, 275, 276, 277, 278ofrfval2 7489 . . . . . . . . . . . . . 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 24637 . . . . . . . . . . . . 13 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘r ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
282165, 166, 280, 281syl3anc 1373 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
28349, 61, 68, 164, 282xrltletrd 12751 . . . . . . . . . . 11 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
284 itg2gt0cn.cn . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
285284ad3antrrr 730 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
286 simplr 769 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 𝑥 ∈ (𝑋(,)𝑌))
287 fssres 6585 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:ℝ⟶(0[,)+∞) ∧ (𝑋(,)𝑌) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
28826, 287mpan2 691 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℝ⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
289 fss 6562 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
290206, 289mpan2 691 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
2913, 288, 2903syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
292291adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
293292ffvelrnda 6904 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ∈ ℝ)
294293, 217resubcld 11260 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
295294adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
296217, 293posdifd 11419 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
297296biimpa 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))
298295, 297elrpd 12625 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+)
299 cncfi 23791 . . . . . . . . . . . . . . 15 (((𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ 𝑥 ∈ (𝑋(,)𝑌) ∧ (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
300285, 286, 298, 299syl3anc 1373 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
301300ex 416 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))))
302 fvres 6736 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
303302breq2d 5065 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑋(,)𝑌) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
304303adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
305 fvres 6736 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
306305adantl 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
307302ad2antlr 727 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
308306, 307oveq12d 7231 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) = ((𝐹𝑢) − (𝐹𝑥)))
309308fveq2d 6721 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) = (abs‘((𝐹𝑢) − (𝐹𝑥))))
310302oveq1d 7228 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑋(,)𝑌) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
311310ad2antlr 727 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
312309, 311breq12d 5066 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ↔ (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
313312imbi2d 344 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
314313ralbidva 3117 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
315314rexbidv 3216 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
316301, 304, 3153imtr3d 296 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
317316imp 410 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
318283, 317r19.29a 3208 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
319318rexlimdva2 3206 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
32048, 319sylbid 243 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
321320imp 410 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
32265ad2antlr 727 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
323 icossicc 13024 . . . . . . . . . 10 (0[,)+∞) ⊆ (0[,]+∞)
324 fss 6562 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
3253, 323, 324sylancl 589 . . . . . . . . 9 (𝜑𝐹:ℝ⟶(0[,]+∞))
326325ad2antrr 726 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹:ℝ⟶(0[,]+∞))
327 breq1 5056 . . . . . . . . . . . 12 (𝑦 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (𝑦 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
328 breq1 5056 . . . . . . . . . . . 12 (0 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (0 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
329266simprbi 500 . . . . . . . . . . . . 13 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} → 𝑦 ≤ (𝐹𝑤))
330329adantl 485 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 𝑦 ≤ (𝐹𝑤))
3313ffvelrnda 6904 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
332 elrege0 13042 . . . . . . . . . . . . . . 15 ((𝐹𝑤) ∈ (0[,)+∞) ↔ ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
333331, 332sylib 221 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ℝ) → ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
334333simprd 499 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ) → 0 ≤ (𝐹𝑤))
335334adantr 484 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ ¬ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 0 ≤ (𝐹𝑤))
336327, 328, 330, 335ifbothda 4477 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
337336ralrimiva 3105 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
338337ad2antrr 726 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
339273a1i 11 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ℝ ∈ V)
34063ad3antlr 731 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
341 fvexd 6732 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ V)
342 eqidd 2738 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
3433feqmptd 6780 . . . . . . . . . . 11 (𝜑𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
344343ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
345339, 340, 341, 342, 344ofrfval2 7489 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘r𝐹 ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
346338, 345mpbird 260 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘r𝐹)
347 itg2le 24637 . . . . . . . 8 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘r𝐹) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
348322, 326, 346, 347syl3anc 1373 . . . . . . 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 3190 . . 3 (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
35367adantl 485 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
354 itg2cl 24630 . . . . . . 7 (𝐹:ℝ⟶(0[,]+∞) → (∫2𝐹) ∈ ℝ*)
355325, 354syl 17 . . . . . 6 (𝜑 → (∫2𝐹) ∈ ℝ*)
356355adantr 484 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2𝐹) ∈ ℝ*)
357 xrltletr 12747 . . . . 5 ((0 ∈ ℝ* ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
3581, 353, 356, 357mp3an2i 1468 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
359358rexlimdva 3203 . . 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 1089   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  {crab 3065  Vcvv 3408  cin 3865  wss 3866  c0 4237  ifcif 4439   class class class wbr 5053  cmpt 5135   × cxp 5549  dom cdm 5551  ran crn 5552  cres 5553  cima 5554   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  r cofr 7468  supcsup 9056  cc 10727  cr 10728  0cc0 10729   + caddc 10732   · cmul 10734  +∞cpnf 10864  -∞cmnf 10865  *cxr 10866   < clt 10867  cle 10868  cmin 11062  -cneg 11063  cq 12544  +crp 12586  (,)cioo 12935  [,)cico 12937  [,]cicc 12938  abscabs 14797  cnccncf 23773  vol*covol 24359  volcvol 24360  2citg2 24513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807  ax-addf 10808
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-disj 5019  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-ofr 7470  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-er 8391  df-map 8510  df-pm 8511  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-fi 9027  df-sup 9058  df-inf 9059  df-oi 9126  df-dju 9517  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-q 12545  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-ioo 12939  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-fl 13367  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-clim 15049  df-rlim 15050  df-sum 15250  df-rest 16927  df-topgen 16948  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-mopn 20359  df-top 21791  df-topon 21808  df-bases 21843  df-cmp 22284  df-cncf 23775  df-ovol 24361  df-vol 24362  df-mbf 24516  df-itg1 24517  df-itg2 24518  df-0p 24567
This theorem is referenced by:  itggt0cn  35584
  Copyright terms: Public domain W3C validator