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 34499
Description: itg2gt0 24048 holds on functions continuous on an open interval in the absence of ax-cc 9710. 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 10541 . . 3 0 ∈ ℝ*
2 imassrn 5824 . . . . 5 (𝐹 “ (𝑋(,)𝑌)) ⊆ ran 𝐹
3 itg2gt0cn.3 . . . . . . 7 (𝜑𝐹:ℝ⟶(0[,)+∞))
43frnd 6396 . . . . . 6 (𝜑 → ran 𝐹 ⊆ (0[,)+∞))
5 icossxr 12675 . . . . . 6 (0[,)+∞) ⊆ ℝ*
64, 5syl6ss 3907 . . . . 5 (𝜑 → ran 𝐹 ⊆ ℝ*)
72, 6sstrid 3906 . . . 4 (𝜑 → (𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*)
8 supxrcl 12562 . . . 4 ((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
97, 8syl 17 . . 3 (𝜑 → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
10 itg2gt0cn.2 . . . . . 6 (𝜑𝑋 < 𝑌)
11 ltrelxr 10555 . . . . . . . . . 10 < ⊆ (ℝ* × ℝ*)
1211ssbri 5013 . . . . . . . . 9 (𝑋 < 𝑌𝑋(ℝ* × ℝ*)𝑌)
1310, 12syl 17 . . . . . . . 8 (𝜑𝑋(ℝ* × ℝ*)𝑌)
14 brxp 5496 . . . . . . . 8 (𝑋(ℝ* × ℝ*)𝑌 ↔ (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
1513, 14sylib 219 . . . . . . 7 (𝜑 → (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
16 ioon0 12618 . . . . . . 7 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
1715, 16syl 17 . . . . . 6 (𝜑 → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
1810, 17mpbird 258 . . . . 5 (𝜑 → (𝑋(,)𝑌) ≠ ∅)
19 itg2gt0cn.5 . . . . . 6 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹𝑥))
2019ralrimiva 3151 . . . . 5 (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
21 r19.2z 4360 . . . . 5 (((𝑋(,)𝑌) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)) → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
2218, 20, 21syl2anc 584 . . . 4 (𝜑 → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
23 supxrlub 12572 . . . . . 6 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
247, 1, 23sylancl 586 . . . . 5 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
253ffnd 6390 . . . . . 6 (𝜑𝐹 Fn ℝ)
26 ioossre 12652 . . . . . 6 (𝑋(,)𝑌) ⊆ ℝ
27 breq2 4972 . . . . . . 7 (𝑦 = (𝐹𝑥) → (0 < 𝑦 ↔ 0 < (𝐹𝑥)))
2827rexima 6871 . . . . . 6 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
2925, 26, 28sylancl 586 . . . . 5 (𝜑 → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3024, 29bitrd 280 . . . 4 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3122, 30mpbird 258 . . 3 (𝜑 → 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))
32 qbtwnxr 12447 . . 3 ((0 ∈ ℝ* ∧ sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ* ∧ 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
331, 9, 31, 32mp3an2i 1458 . 2 (𝜑 → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
34 qre 12206 . . . . . . . . 9 (𝑦 ∈ ℚ → 𝑦 ∈ ℝ)
3534adantr 481 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
36 simpr 485 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 0 < 𝑦)
3735, 36elrpd 12282 . . . . . . 7 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ+)
3837anim1i 614 . . . . . 6 (((𝑦 ∈ ℚ ∧ 0 < 𝑦) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
3938anasss 467 . . . . 5 ((𝑦 ∈ ℚ ∧ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
40 simplr 765 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝑦 ∈ ℝ+)
41 rpxr 12252 . . . . . . . . . . 11 (𝑦 ∈ ℝ+𝑦 ∈ ℝ*)
42 supxrlub 12572 . . . . . . . . . . 11 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*𝑦 ∈ ℝ*) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
437, 41, 42syl2an 595 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
44 breq2 4972 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑥) → (𝑦 < 𝑧𝑦 < (𝐹𝑥)))
4544rexima 6871 . . . . . . . . . . . 12 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4625, 26, 45sylancl 586 . . . . . . . . . . 11 (𝜑 → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4746adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4843, 47bitrd 280 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
491a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 ∈ ℝ*)
50 ioorp 12668 . . . . . . . . . . . . . . . . . . 19 (0(,)+∞) = ℝ+
51 ioossicc 12676 . . . . . . . . . . . . . . . . . . 19 (0(,)+∞) ⊆ (0[,]+∞)
5250, 51eqsstrri 3929 . . . . . . . . . . . . . . . . . 18 + ⊆ (0[,]+∞)
5352sseli 3891 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ (0[,]+∞))
54 0e0iccpnf 12701 . . . . . . . . . . . . . . . . 17 0 ∈ (0[,]+∞)
55 ifcl 4431 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5653, 54, 55sylancl 586 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5756adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5857fmpttd 6749 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
59 itg2cl 24020 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6058, 59syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6160ad5antlr 731 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
62 ifcl 4431 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6353, 54, 62sylancl 586 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6463adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6564fmpttd 6749 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
66 itg2cl 24020 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
6765, 66syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
6867ad5antlr 731 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
69 rpre 12251 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
7069ad4antlr 729 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ ℝ)
71 ioombl 23853 . . . . . . . . . . . . . . . . . 18 (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol
72 mblvol 23818 . . . . . . . . . . . . . . . . . 18 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
7371, 72ax-mp 5 . . . . . . . . . . . . . . . . 17 (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
74 elioore 12622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ)
7574ad3antlr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ)
76 rpre 12251 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
7776adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈ ℝ)
7875, 77resubcld 10922 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ)
7978adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ)
8078rexrd 10544 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ*)
8180adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ*)
8215simpld 495 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ*)
8382ad5antr 730 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ*)
8415simprd 496 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑌 ∈ ℝ*)
8584ad5antr 730 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑌 ∈ ℝ*)
8682ad4antr 728 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 ∈ ℝ*)
87 xrltnle 10561 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
8880, 86, 87syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
8988biimpar 478 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) < 𝑋)
9010ad5antr 730 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 < 𝑌)
91 xrre2 12417 . . . . . . . . . . . . . . . . . . . 20 ((((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) < 𝑋𝑋 < 𝑌)) → 𝑋 ∈ ℝ)
9281, 83, 85, 89, 90, 91syl32anc 1371 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ)
9379, 92ifclda 4421 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ)
9484ad5antr 730 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ*)
9577, 75readdcld 10523 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ)
9695adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
97 mnfxr 10551 . . . . . . . . . . . . . . . . . . . . . . 23 -∞ ∈ ℝ*
9897a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -∞ ∈ ℝ*)
99 mnfle 12383 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 ∈ ℝ* → -∞ ≤ 𝑋)
10082, 99syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -∞ ≤ 𝑋)
10198, 82, 84, 100, 10xrlelttrd 12407 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → -∞ < 𝑌)
102101ad5antr 730 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → -∞ < 𝑌)
103 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ≤ (𝑧 + 𝑥))
104 xrre 12416 . . . . . . . . . . . . . . . . . . . 20 (((𝑌 ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ) ∧ (-∞ < 𝑌𝑌 ≤ (𝑧 + 𝑥))) → 𝑌 ∈ ℝ)
10594, 96, 102, 103, 104syl22anc 835 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ)
10695adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
107105, 106ifclda 4421 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ)
10875rexrd 10544 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ*)
10984ad4antr 728 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑌 ∈ ℝ*)
110 rpgt0 12255 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ+ → 0 < 𝑧)
111110adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑧)
11277, 75ltsubposd 11080 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧 ↔ (𝑥𝑧) < 𝑥))
113111, 112mpbid 233 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑥)
114 eliooord 12650 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑥𝑥 < 𝑌))
115114simprd 496 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 < 𝑌)
116115ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < 𝑌)
11780, 108, 109, 113, 116xrlttrd 12406 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑌)
11877, 75ltaddpos2d 11079 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧𝑥 < (𝑧 + 𝑥)))
119111, 118mpbid 233 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < (𝑧 + 𝑥))
12078, 75, 95, 113, 119lttrd 10654 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < (𝑧 + 𝑥))
121 breq2 4972 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < 𝑌 ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
122 breq2 4972 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < (𝑧 + 𝑥) ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
123121, 122ifboth 4425 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑧) < 𝑌 ∧ (𝑥𝑧) < (𝑧 + 𝑥)) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
124117, 120, 123syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
12510ad4antr 728 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑌)
12695rexrd 10544 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ*)
127114simpld 495 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝑋(,)𝑌) → 𝑋 < 𝑥)
128127ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑥)
12986, 108, 126, 128, 119xrlttrd 12406 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < (𝑧 + 𝑥))
130 breq2 4972 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < 𝑌𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
131 breq2 4972 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < (𝑧 + 𝑥) ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
132130, 131ifboth 4425 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 < 𝑌𝑋 < (𝑧 + 𝑥)) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
133125, 129, 132syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
134 breq1 4971 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑧) = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → ((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
135 breq1 4971 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → (𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
136134, 135ifboth 4425 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∧ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
137124, 133, 136syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
13893, 107, 137ltled 10641 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
139 ovolioo 23856 . . . . . . . . . . . . . . . . . 18 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ ∧ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ ∧ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14093, 107, 138, 139syl3anc 1364 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14173, 140syl5eq 2845 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
142107, 93resubcld 10922 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)) ∈ ℝ)
143141, 142eqeltrd 2885 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ)
144 rpgt0 12255 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ → 0 < 𝑦)
145144ad4antlr 729 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑦)
14693, 107posdifd 11081 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋))))
147137, 146mpbid 233 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
148147, 141breqtrrd 4996 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
14970, 143, 145, 148mulgt0d 10648 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
150 iooin 12626 . . . . . . . . . . . . . . . . . . . 20 (((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*)) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
15186, 109, 80, 126, 150syl22anc 835 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
152151eleq2d 2870 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ 𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
153152ifbid 4409 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))
154153mpteq2dv 5063 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)))
155154fveq2d 6549 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))))
156 rpge0 12256 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
157 elrege0 12696 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦))
15869, 156, 157sylanbrc 583 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ (0[,)+∞))
159158ad4antlr 729 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ (0[,)+∞))
160 itg2const 24028 . . . . . . . . . . . . . . . 16 (((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol ∧ (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ ∧ 𝑦 ∈ (0[,)+∞)) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
16171, 143, 159, 160mp3an2i 1458 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
162155, 161eqtrd 2833 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
163149, 162breqtrrd 4996 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
164163adantr 481 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
16558ad5antlr 731 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
16665ad5antlr 731 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
167 fvoveq1 7046 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑤 → (abs‘(𝑢𝑥)) = (abs‘(𝑤𝑥)))
168167breq1d 4978 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑤 → ((abs‘(𝑢𝑥)) < 𝑧 ↔ (abs‘(𝑤𝑥)) < 𝑧))
169168imbrov2fvoveq 7048 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑤 → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ↔ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
170169rspccva 3560 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
171 breq1 4971 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
172 breq1 4971 . . . . . . . . . . . . . . . . . . . . . 22 (0 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
17369leidd 11060 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℝ+𝑦𝑦)
174173ad6antlr 733 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦𝑦)
17574ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑥 ∈ ℝ)
17676ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑧 ∈ ℝ)
177175, 176resubcld 10922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ)
178177rexrd 10544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ*)
179176, 175readdcld 10523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ)
180179rexrd 10544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ*)
181 elioo2 12633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
182178, 180, 181syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
183 3anass 1088 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
184182, 183syl6bb 288 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
185 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
18674ad5antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℝ)
187185, 186resubcld 10922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑤𝑥) ∈ ℝ)
18876ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℝ)
189187, 188absltd 14627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ (-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧)))
190188renegcld 10921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → -𝑧 ∈ ℝ)
191186, 190, 185ltaddsub2d 11095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ -𝑧 < (𝑤𝑥)))
192186recnd 10522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℂ)
193188recnd 10522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℂ)
194192, 193negsubd 10857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑥 + -𝑧) = (𝑥𝑧))
195194breq1d 4978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ (𝑥𝑧) < 𝑤))
196191, 195bitr3d 282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (-𝑧 < (𝑤𝑥) ↔ (𝑥𝑧) < 𝑤))
197185, 186, 188ltsubaddd 11090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑤𝑥) < 𝑧𝑤 < (𝑧 + 𝑥)))
198196, 197anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧) ↔ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
199189, 198bitrd 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
200199pm5.32da 579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
201184, 200bitr4d 283 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)))
202201biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧))
203 pm3.35 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘(𝑤𝑥)) < 𝑧 ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
204203ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
20569ad6antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ∈ ℝ)
206 rge0ssre 12698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0[,)+∞) ⊆ ℝ
2073ad4antr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
208207ffvelrnda 6723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
209206, 208sseldi 3893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ ℝ)
210209adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑤) ∈ ℝ)
2113adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑦 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
212211ffvelrnda 6723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
213206, 212sseldi 3893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
21474, 213sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℝ)
215214ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
216209, 215resubcld 10922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑤) − (𝐹𝑥)) ∈ ℝ)
21769ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
218214, 217resubcld 10922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
219218ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
220216, 219absltd 14627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
221214recnd 10522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℂ)
222 rpcn 12253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
223222ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
224221, 223negsubdi2d 10867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
225224ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
226225breq1d 4978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
227226anbi1d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦)) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
228220, 227bitrd 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
229228simprbda 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)))
230214ad4antr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑥) ∈ ℝ)
231205, 210, 230ltsub1d 11103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 < (𝐹𝑤) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
232229, 231mpbird 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 < (𝐹𝑤))
233205, 210, 232ltled 10641 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ≤ (𝐹𝑤))
234204, 233sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
235234an4s 656 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
236202, 235syldan 591 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ (𝐹𝑤))
237236iftrued 4395 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) = 𝑦)
238174, 237breqtrrd 4996 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
239 0le0 11592 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
240 breq2 4972 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 𝑦 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
241 breq2 4972 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
242240, 241ifboth 4425 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ≤ 𝑦 ∧ 0 ≤ 0) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
243156, 239, 242sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℝ+ → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
244243ad6antlr 733 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ ¬ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
245171, 172, 238, 244ifbothda 4424 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
246170, 245sylan2 592 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
247246anassrs 468 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
248 iftrue 4393 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
249248adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
250 iftrue 4393 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
251250adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
252247, 249, 2513brtr4d 5000 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
253252ex 413 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)))
254239a1i 11 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → 0 ≤ 0)
255 iffalse 4396 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = 0)
256 iffalse 4396 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = 0)
257254, 255, 2563brtr4d 5000 . . . . . . . . . . . . . . . . 17 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
258253, 257pm2.61d1 181 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
259 elin 4096 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))))
260 ifbi 4408 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
261259, 260ax-mp 5 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)
262 ifan 4438 . . . . . . . . . . . . . . . . 17 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
263261, 262eqtri 2821 . . . . . . . . . . . . . . . 16 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
264 fveq2 6545 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑤 → (𝐹𝑣) = (𝐹𝑤))
265264breq2d 4980 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑦 ≤ (𝐹𝑣) ↔ 𝑦 ≤ (𝐹𝑤)))
266265elrab 3621 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)))
267 ifbi 4408 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤))) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0))
268266, 267ax-mp 5 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0)
269 ifan 4438 . . . . . . . . . . . . . . . . 17 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
270268, 269eqtri 2821 . . . . . . . . . . . . . . . 16 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
271258, 263, 2703brtr4g 5002 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
272271ralrimivw 3152 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
273 reex 10481 . . . . . . . . . . . . . . . 16 ℝ ∈ V
274273a1i 11 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ℝ ∈ V)
27556ad6antlr 733 . . . . . . . . . . . . . . 15 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
27663ad6antlr 733 . . . . . . . . . . . . . . 15 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
277 eqidd 2798 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))
278 eqidd 2798 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
279274, 275, 276, 277, 278ofrfval2 7292 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
280272, 279mpbird 258 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
281 itg2le 24027 . . . . . . . . . . . . 13 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
282165, 166, 280, 281syl3anc 1364 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
28349, 61, 68, 164, 282xrltletrd 12408 . . . . . . . . . . 11 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
284 itg2gt0cn.cn . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
285284ad3antrrr 726 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
286 simplr 765 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 𝑥 ∈ (𝑋(,)𝑌))
287 fssres 6419 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:ℝ⟶(0[,)+∞) ∧ (𝑋(,)𝑌) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
28826, 287mpan2 687 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℝ⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
289 fss 6402 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
290206, 289mpan2 687 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
2913, 288, 2903syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
292291adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
293292ffvelrnda 6723 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ∈ ℝ)
294293, 217resubcld 10922 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
295294adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
296217, 293posdifd 11081 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
297296biimpa 477 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))
298295, 297elrpd 12282 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+)
299 cncfi 23189 . . . . . . . . . . . . . . 15 (((𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ 𝑥 ∈ (𝑋(,)𝑌) ∧ (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
300285, 286, 298, 299syl3anc 1364 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
301300ex 413 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))))
302 fvres 6564 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
303302breq2d 4980 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑋(,)𝑌) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
304303adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
305 fvres 6564 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
306305adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
307302ad2antlr 723 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
308306, 307oveq12d 7041 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) = ((𝐹𝑢) − (𝐹𝑥)))
309308fveq2d 6549 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) = (abs‘((𝐹𝑢) − (𝐹𝑥))))
310302oveq1d 7038 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑋(,)𝑌) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
311310ad2antlr 723 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
312309, 311breq12d 4981 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ↔ (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
313312imbi2d 342 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
314313ralbidva 3165 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
315314rexbidv 3262 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
316301, 304, 3153imtr3d 294 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
317316imp 407 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
318283, 317r19.29a 3254 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
319318rexlimdva2 3252 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
32048, 319sylbid 241 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
321320imp 407 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
32265ad2antlr 723 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
323 icossicc 12678 . . . . . . . . . 10 (0[,)+∞) ⊆ (0[,]+∞)
324 fss 6402 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
3253, 323, 324sylancl 586 . . . . . . . . 9 (𝜑𝐹:ℝ⟶(0[,]+∞))
326325ad2antrr 722 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹:ℝ⟶(0[,]+∞))
327 breq1 4971 . . . . . . . . . . . 12 (𝑦 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (𝑦 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
328 breq1 4971 . . . . . . . . . . . 12 (0 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (0 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
329266simprbi 497 . . . . . . . . . . . . 13 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} → 𝑦 ≤ (𝐹𝑤))
330329adantl 482 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 𝑦 ≤ (𝐹𝑤))
3313ffvelrnda 6723 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
332 elrege0 12696 . . . . . . . . . . . . . . 15 ((𝐹𝑤) ∈ (0[,)+∞) ↔ ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
333331, 332sylib 219 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ℝ) → ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
334333simprd 496 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ) → 0 ≤ (𝐹𝑤))
335334adantr 481 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ ¬ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 0 ≤ (𝐹𝑤))
336327, 328, 330, 335ifbothda 4424 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
337336ralrimiva 3151 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
338337ad2antrr 722 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
339273a1i 11 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ℝ ∈ V)
34063ad3antlr 727 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
341 fvexd 6560 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ V)
342 eqidd 2798 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
3433feqmptd 6608 . . . . . . . . . . 11 (𝜑𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
344343ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
345339, 340, 341, 342, 344ofrfval2 7292 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹 ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
346338, 345mpbird 258 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹)
347 itg2le 24027 . . . . . . . 8 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
348322, 326, 346, 347syl3anc 1364 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
34940, 321, 348jca32 516 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
350349expl 458 . . . . 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 3236 . . 3 (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
35367adantl 482 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
354 itg2cl 24020 . . . . . . 7 (𝐹:ℝ⟶(0[,]+∞) → (∫2𝐹) ∈ ℝ*)
355325, 354syl 17 . . . . . 6 (𝜑 → (∫2𝐹) ∈ ℝ*)
356355adantr 481 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2𝐹) ∈ ℝ*)
357 xrltletr 12404 . . . . 5 ((0 ∈ ℝ* ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
3581, 353, 356, 357mp3an2i 1458 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
359358rexlimdva 3249 . . 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 207  wa 396  w3a 1080   = wceq 1525  wcel 2083  wne 2986  wral 3107  wrex 3108  {crab 3111  Vcvv 3440  cin 3864  wss 3865  c0 4217  ifcif 4387   class class class wbr 4968  cmpt 5047   × cxp 5448  dom cdm 5450  ran crn 5451  cres 5452  cima 5453   Fn wfn 6227  wf 6228  cfv 6232  (class class class)co 7023  𝑟 cofr 7273  supcsup 8757  cc 10388  cr 10389  0cc0 10390   + caddc 10393   · cmul 10395  +∞cpnf 10525  -∞cmnf 10526  *cxr 10527   < clt 10528  cle 10529  cmin 10723  -cneg 10724  cq 12201  +crp 12243  (,)cioo 12592  [,)cico 12594  [,]cicc 12595  abscabs 14431  cnccncf 23171  vol*covol 23750  volcvol 23751  2citg2 23904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468  ax-addf 10469
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-disj 4937  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-of 7274  df-ofr 7275  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-er 8146  df-map 8265  df-pm 8266  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-fi 8728  df-sup 8759  df-inf 8760  df-oi 8827  df-dju 9183  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-n0 11752  df-z 11836  df-uz 12098  df-q 12202  df-rp 12244  df-xneg 12361  df-xadd 12362  df-xmul 12363  df-ioo 12596  df-ico 12598  df-icc 12599  df-fz 12747  df-fzo 12888  df-fl 13016  df-seq 13224  df-exp 13284  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-clim 14683  df-rlim 14684  df-sum 14881  df-rest 16529  df-topgen 16550  df-psmet 20223  df-xmet 20224  df-met 20225  df-bl 20226  df-mopn 20227  df-top 21190  df-topon 21207  df-bases 21242  df-cmp 21683  df-cncf 23173  df-ovol 23752  df-vol 23753  df-mbf 23907  df-itg1 23908  df-itg2 23909  df-0p 23958
This theorem is referenced by:  itggt0cn  34516
  Copyright terms: Public domain W3C validator