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 33595
Description: itg2gt0 23572 holds on functions continuous on an open interval in the absence of ax-cc 9295. 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 10124 . . . 4 0 ∈ ℝ*
21a1i 11 . . 3 (𝜑 → 0 ∈ ℝ*)
3 imassrn 5512 . . . . 5 (𝐹 “ (𝑋(,)𝑌)) ⊆ ran 𝐹
4 itg2gt0cn.3 . . . . . . 7 (𝜑𝐹:ℝ⟶(0[,)+∞))
5 frn 6091 . . . . . . 7 (𝐹:ℝ⟶(0[,)+∞) → ran 𝐹 ⊆ (0[,)+∞))
64, 5syl 17 . . . . . 6 (𝜑 → ran 𝐹 ⊆ (0[,)+∞))
7 icossxr 12296 . . . . . 6 (0[,)+∞) ⊆ ℝ*
86, 7syl6ss 3648 . . . . 5 (𝜑 → ran 𝐹 ⊆ ℝ*)
93, 8syl5ss 3647 . . . 4 (𝜑 → (𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*)
10 supxrcl 12183 . . . 4 ((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
119, 10syl 17 . . 3 (𝜑 → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
12 itg2gt0cn.2 . . . . . 6 (𝜑𝑋 < 𝑌)
13 ltrelxr 10137 . . . . . . . . . 10 < ⊆ (ℝ* × ℝ*)
1413ssbri 4730 . . . . . . . . 9 (𝑋 < 𝑌𝑋(ℝ* × ℝ*)𝑌)
1512, 14syl 17 . . . . . . . 8 (𝜑𝑋(ℝ* × ℝ*)𝑌)
16 brxp 5181 . . . . . . . 8 (𝑋(ℝ* × ℝ*)𝑌 ↔ (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
1715, 16sylib 208 . . . . . . 7 (𝜑 → (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
18 ioon0 12239 . . . . . . 7 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
1917, 18syl 17 . . . . . 6 (𝜑 → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
2012, 19mpbird 247 . . . . 5 (𝜑 → (𝑋(,)𝑌) ≠ ∅)
21 itg2gt0cn.5 . . . . . 6 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹𝑥))
2221ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
23 r19.2z 4093 . . . . 5 (((𝑋(,)𝑌) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)) → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
2420, 22, 23syl2anc 694 . . . 4 (𝜑 → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
25 supxrlub 12193 . . . . . 6 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
269, 1, 25sylancl 695 . . . . 5 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
27 ffn 6083 . . . . . . 7 (𝐹:ℝ⟶(0[,)+∞) → 𝐹 Fn ℝ)
284, 27syl 17 . . . . . 6 (𝜑𝐹 Fn ℝ)
29 ioossre 12273 . . . . . 6 (𝑋(,)𝑌) ⊆ ℝ
30 breq2 4689 . . . . . . 7 (𝑦 = (𝐹𝑥) → (0 < 𝑦 ↔ 0 < (𝐹𝑥)))
3130rexima 6537 . . . . . 6 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3228, 29, 31sylancl 695 . . . . 5 (𝜑 → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3326, 32bitrd 268 . . . 4 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3424, 33mpbird 247 . . 3 (𝜑 → 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))
35 qbtwnxr 12069 . . 3 ((0 ∈ ℝ* ∧ sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ* ∧ 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
362, 11, 34, 35syl3anc 1366 . 2 (𝜑 → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
37 qre 11831 . . . . . . . . 9 (𝑦 ∈ ℚ → 𝑦 ∈ ℝ)
3837adantr 480 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
39 simpr 476 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 0 < 𝑦)
4038, 39elrpd 11907 . . . . . . 7 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ+)
4140anim1i 591 . . . . . 6 (((𝑦 ∈ ℚ ∧ 0 < 𝑦) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
4241anasss 680 . . . . 5 ((𝑦 ∈ ℚ ∧ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
43 simplr 807 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝑦 ∈ ℝ+)
44 rpxr 11878 . . . . . . . . . . 11 (𝑦 ∈ ℝ+𝑦 ∈ ℝ*)
45 supxrlub 12193 . . . . . . . . . . 11 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*𝑦 ∈ ℝ*) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
469, 44, 45syl2an 493 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
47 breq2 4689 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑥) → (𝑦 < 𝑧𝑦 < (𝐹𝑥)))
4847rexima 6537 . . . . . . . . . . . 12 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4928, 29, 48sylancl 695 . . . . . . . . . . 11 (𝜑 → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
5049adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
5146, 50bitrd 268 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
521a1i 11 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 ∈ ℝ*)
53 ioorp 12289 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) = ℝ+
54 ioossicc 12297 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) ⊆ (0[,]+∞)
5553, 54eqsstr3i 3669 . . . . . . . . . . . . . . . . . . 19 + ⊆ (0[,]+∞)
5655sseli 3632 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+𝑦 ∈ (0[,]+∞))
57 0e0iccpnf 12321 . . . . . . . . . . . . . . . . . 18 0 ∈ (0[,]+∞)
58 ifcl 4163 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5956, 57, 58sylancl 695 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+ → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
6059adantr 480 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
61 eqid 2651 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
6260, 61fmptd 6425 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
63 itg2cl 23544 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6462, 63syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6564ad5antlr 775 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
66 ifcl 4163 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6756, 57, 66sylancl 695 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+ → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6867adantr 480 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
69 eqid 2651 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
7068, 69fmptd 6425 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
71 itg2cl 23544 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
7270, 71syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
7372ad5antlr 775 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
74 rpre 11877 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
7574ad4antlr 771 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ ℝ)
76 ioombl 23379 . . . . . . . . . . . . . . . . . . 19 (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol
77 mblvol 23344 . . . . . . . . . . . . . . . . . . 19 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . 18 (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
79 elioore 12243 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ)
8079ad3antlr 767 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ)
81 rpre 11877 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
8281adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈ ℝ)
8380, 82resubcld 10496 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ)
8483adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ)
8583rexrd 10127 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ*)
8685adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ*)
8717simpld 474 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 ∈ ℝ*)
8887ad5antr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ*)
8917simprd 478 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌 ∈ ℝ*)
9089ad5antr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑌 ∈ ℝ*)
9187ad4antr 769 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 ∈ ℝ*)
92 xrltnle 10143 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
9385, 91, 92syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
9493biimpar 501 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) < 𝑋)
9512ad5antr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 < 𝑌)
96 xrre2 12039 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) < 𝑋𝑋 < 𝑌)) → 𝑋 ∈ ℝ)
9786, 88, 90, 94, 95, 96syl32anc 1374 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ)
9884, 97ifclda 4153 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ)
9989ad5antr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ*)
10082, 80readdcld 10107 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ)
101100adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
102 mnfxr 10134 . . . . . . . . . . . . . . . . . . . . . . . 24 -∞ ∈ ℝ*
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → -∞ ∈ ℝ*)
104 mnfle 12007 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∈ ℝ* → -∞ ≤ 𝑋)
10587, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → -∞ ≤ 𝑋)
106103, 87, 89, 105, 12xrlelttrd 12029 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -∞ < 𝑌)
107106ad5antr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → -∞ < 𝑌)
108 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ≤ (𝑧 + 𝑥))
109 xrre 12038 . . . . . . . . . . . . . . . . . . . . 21 (((𝑌 ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ) ∧ (-∞ < 𝑌𝑌 ≤ (𝑧 + 𝑥))) → 𝑌 ∈ ℝ)
11099, 101, 107, 108, 109syl22anc 1367 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ)
111100adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
112110, 111ifclda 4153 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ)
11380rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ*)
11489ad4antr 769 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑌 ∈ ℝ*)
115 rpgt0 11882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℝ+ → 0 < 𝑧)
116115adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑧)
11782, 80ltsubposd 10651 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧 ↔ (𝑥𝑧) < 𝑥))
118116, 117mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑥)
119 eliooord 12271 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑥𝑥 < 𝑌))
120119simprd 478 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 < 𝑌)
121120ad3antlr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < 𝑌)
12285, 113, 114, 118, 121xrlttrd 12028 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑌)
12382, 80ltaddpos2d 10650 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧𝑥 < (𝑧 + 𝑥)))
124116, 123mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < (𝑧 + 𝑥))
12583, 80, 100, 118, 124lttrd 10236 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < (𝑧 + 𝑥))
126 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < 𝑌 ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
127 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < (𝑧 + 𝑥) ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
128126, 127ifboth 4157 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑧) < 𝑌 ∧ (𝑥𝑧) < (𝑧 + 𝑥)) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
129122, 125, 128syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
13012ad4antr 769 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑌)
131100rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ*)
132119simpld 474 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (𝑋(,)𝑌) → 𝑋 < 𝑥)
133132ad3antlr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑥)
13491, 113, 131, 133, 124xrlttrd 12028 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < (𝑧 + 𝑥))
135 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < 𝑌𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
136 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < (𝑧 + 𝑥) ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
137135, 136ifboth 4157 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 < 𝑌𝑋 < (𝑧 + 𝑥)) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
138130, 134, 137syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
139 breq1 4688 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑧) = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → ((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
140 breq1 4688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → (𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
141139, 140ifboth 4157 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∧ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
142129, 138, 141syl2anc 694 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
14398, 112, 142ltled 10223 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
144 ovolioo 23382 . . . . . . . . . . . . . . . . . . 19 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ ∧ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ ∧ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14598, 112, 143, 144syl3anc 1366 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14678, 145syl5eq 2697 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
147112, 98resubcld 10496 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)) ∈ ℝ)
148146, 147eqeltrd 2730 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ)
149 rpgt0 11882 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+ → 0 < 𝑦)
150149ad4antlr 771 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑦)
15198, 112posdifd 10652 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋))))
152142, 151mpbid 222 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
153152, 146breqtrrd 4713 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
15475, 148, 150, 153mulgt0d 10230 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
155 iooin 12247 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*)) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
15691, 114, 85, 131, 155syl22anc 1367 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
157156eleq2d 2716 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ 𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
158157ifbid 4141 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))
159158mpteq2dv 4778 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)))
160159fveq2d 6233 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))))
16176a1i 11 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol)
162 rpge0 11883 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
163 elrege0 12316 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦))
16474, 162, 163sylanbrc 699 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+𝑦 ∈ (0[,)+∞))
165164ad4antlr 771 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ (0[,)+∞))
166 itg2const 23552 . . . . . . . . . . . . . . . . 17 (((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol ∧ (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ ∧ 𝑦 ∈ (0[,)+∞)) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
167161, 148, 165, 166syl3anc 1366 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
168160, 167eqtrd 2685 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
169154, 168breqtrrd 4713 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
170169adantr 480 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
17162ad5antlr 775 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
17270ad5antlr 775 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
173 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 = 𝑤 → (𝑢𝑥) = (𝑤𝑥))
174173fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = 𝑤 → (abs‘(𝑢𝑥)) = (abs‘(𝑤𝑥)))
175174breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑤 → ((abs‘(𝑢𝑥)) < 𝑧 ↔ (abs‘(𝑤𝑥)) < 𝑧))
176 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑤 → (𝐹𝑢) = (𝐹𝑤))
177176oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 = 𝑤 → ((𝐹𝑢) − (𝐹𝑥)) = ((𝐹𝑤) − (𝐹𝑥)))
178177fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = 𝑤 → (abs‘((𝐹𝑢) − (𝐹𝑥))) = (abs‘((𝐹𝑤) − (𝐹𝑥))))
179178breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑤 → ((abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
180175, 179imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑤 → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ↔ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
181180rspccva 3339 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
182 breq1 4688 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
183 breq1 4688 . . . . . . . . . . . . . . . . . . . . . . 23 (0 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
18474leidd 10632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℝ+𝑦𝑦)
185184ad6antlr 779 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦𝑦)
18679ad4antlr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑥 ∈ ℝ)
18781ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑧 ∈ ℝ)
188186, 187resubcld 10496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ)
189188rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ*)
190187, 186readdcld 10107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ)
191190rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ*)
192 elioo2 12254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
193189, 191, 192syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
194 3anass 1059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
195193, 194syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
196 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
19779ad5antlr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℝ)
198196, 197resubcld 10496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑤𝑥) ∈ ℝ)
19981ad3antlr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℝ)
200198, 199absltd 14212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ (-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧)))
201199renegcld 10495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → -𝑧 ∈ ℝ)
202197, 201, 196ltaddsub2d 10666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ -𝑧 < (𝑤𝑥)))
203197recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℂ)
204199recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℂ)
205203, 204negsubd 10436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑥 + -𝑧) = (𝑥𝑧))
206205breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ (𝑥𝑧) < 𝑤))
207202, 206bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (-𝑧 < (𝑤𝑥) ↔ (𝑥𝑧) < 𝑤))
208196, 197, 199ltsubaddd 10661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑤𝑥) < 𝑧𝑤 < (𝑧 + 𝑥)))
209207, 208anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧) ↔ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
210200, 209bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
211210pm5.32da 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
212195, 211bitr4d 271 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)))
213212biimpa 500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧))
214 pm3.35 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((abs‘(𝑤𝑥)) < 𝑧 ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
215214ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
21674ad6antlr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ∈ ℝ)
217 rge0ssre 12318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0[,)+∞) ⊆ ℝ
2184ad4antr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
219218ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
220217, 219sseldi 3634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ ℝ)
221220adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑤) ∈ ℝ)
2224adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑦 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
223222ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
224217, 223sseldi 3634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
22579, 224sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℝ)
226225ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
227220, 226resubcld 10496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑤) − (𝐹𝑥)) ∈ ℝ)
22874ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
229225, 228resubcld 10496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
230229ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
231227, 230absltd 14212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
232225recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℂ)
233 rpcn 11879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
234233ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
235232, 234negsubdi2d 10446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
236235ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
237236breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
238237anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦)) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
239231, 238bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
240239simprbda 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)))
241225ad4antr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑥) ∈ ℝ)
242216, 221, 241ltsub1d 10674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 < (𝐹𝑤) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
243240, 242mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 < (𝐹𝑤))
244216, 221, 243ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ≤ (𝐹𝑤))
245215, 244sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
246245an4s 886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
247213, 246syldan 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ (𝐹𝑤))
248247iftrued 4127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) = 𝑦)
249185, 248breqtrrd 4713 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
250 0le0 11148 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ≤ 0
251 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 𝑦 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
252 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
253251, 252ifboth 4157 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ≤ 𝑦 ∧ 0 ≤ 0) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
254162, 250, 253sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℝ+ → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
255254ad6antlr 779 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ ¬ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
256182, 183, 249, 255ifbothda 4156 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
257181, 256sylan2 490 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
258257anassrs 681 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
259 iftrue 4125 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
260259adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
261 iftrue 4125 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
262261adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
263258, 260, 2623brtr4d 4717 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
264263ex 449 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)))
265250a1i 11 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑋(,)𝑌) → 0 ≤ 0)
266 iffalse 4128 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = 0)
267 iffalse 4128 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = 0)
268265, 266, 2673brtr4d 4717 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
269264, 268pm2.61d1 171 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
270 elin 3829 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))))
271 ifbi 4140 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
272270, 271ax-mp 5 . . . . . . . . . . . . . . . . . 18 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)
273 ifan 4167 . . . . . . . . . . . . . . . . . 18 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
274272, 273eqtri 2673 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
275 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑤 → (𝐹𝑣) = (𝐹𝑤))
276275breq2d 4697 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑤 → (𝑦 ≤ (𝐹𝑣) ↔ 𝑦 ≤ (𝐹𝑤)))
277276elrab 3396 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)))
278 ifbi 4140 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤))) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0))
279277, 278ax-mp 5 . . . . . . . . . . . . . . . . . 18 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0)
280 ifan 4167 . . . . . . . . . . . . . . . . . 18 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
281279, 280eqtri 2673 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
282269, 274, 2813brtr4g 4719 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
283282ralrimivw 2996 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
284 reex 10065 . . . . . . . . . . . . . . . . 17 ℝ ∈ V
285284a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ℝ ∈ V)
28659ad6antlr 779 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
28767ad6antlr 779 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
288 eqidd 2652 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))
289 eqidd 2652 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
290285, 286, 287, 288, 289ofrfval2 6957 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
291283, 290mpbird 247 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
292 itg2le 23551 . . . . . . . . . . . . . 14 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
293171, 172, 291, 292syl3anc 1366 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
29452, 65, 73, 170, 293xrltletrd 12030 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
295 itg2gt0cn.cn . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
296295ad3antrrr 766 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
297 simplr 807 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 𝑥 ∈ (𝑋(,)𝑌))
298 fssres 6108 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:ℝ⟶(0[,)+∞) ∧ (𝑋(,)𝑌) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
29929, 298mpan2 707 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:ℝ⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
300 fss 6094 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
301217, 300mpan2 707 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
3024, 299, 3013syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
303302adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℝ+) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
304303ffvelrnda 6399 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ∈ ℝ)
305304, 228resubcld 10496 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
306305adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
307228, 304posdifd 10652 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
308307biimpa 500 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))
309306, 308elrpd 11907 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+)
310 cncfi 22744 . . . . . . . . . . . . . . . 16 (((𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ 𝑥 ∈ (𝑋(,)𝑌) ∧ (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
311296, 297, 309, 310syl3anc 1366 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
312311ex 449 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))))
313 fvres 6245 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
314313breq2d 4697 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑋(,)𝑌) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
315314adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
316 fvres 6245 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
317316adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
318313ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
319317, 318oveq12d 6708 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) = ((𝐹𝑢) − (𝐹𝑥)))
320319fveq2d 6233 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) = (abs‘((𝐹𝑢) − (𝐹𝑥))))
321313oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝑋(,)𝑌) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
322321ad2antlr 763 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
323320, 322breq12d 4698 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ↔ (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
324323imbi2d 329 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
325324ralbidva 3014 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
326325rexbidv 3081 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
327312, 315, 3263imtr3d 282 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
328327imp 444 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
329294, 328r19.29a 3107 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
330329ex 449 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
331330rexlimdva 3060 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
33251, 331sylbid 230 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
333332imp 444 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
33470ad2antlr 763 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
335 icossicc 12298 . . . . . . . . . 10 (0[,)+∞) ⊆ (0[,]+∞)
336 fss 6094 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
3374, 335, 336sylancl 695 . . . . . . . . 9 (𝜑𝐹:ℝ⟶(0[,]+∞))
338337ad2antrr 762 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹:ℝ⟶(0[,]+∞))
339 breq1 4688 . . . . . . . . . . . 12 (𝑦 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (𝑦 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
340 breq1 4688 . . . . . . . . . . . 12 (0 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (0 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
341277simprbi 479 . . . . . . . . . . . . 13 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} → 𝑦 ≤ (𝐹𝑤))
342341adantl 481 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 𝑦 ≤ (𝐹𝑤))
3434ffvelrnda 6399 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
344 elrege0 12316 . . . . . . . . . . . . . . 15 ((𝐹𝑤) ∈ (0[,)+∞) ↔ ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
345343, 344sylib 208 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ℝ) → ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
346345simprd 478 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ) → 0 ≤ (𝐹𝑤))
347346adantr 480 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ ¬ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 0 ≤ (𝐹𝑤))
348339, 340, 342, 347ifbothda 4156 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
349348ralrimiva 2995 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
350349ad2antrr 762 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
351284a1i 11 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ℝ ∈ V)
35267ad3antlr 767 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
353 fvexd 6241 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ V)
354 eqidd 2652 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
3554feqmptd 6288 . . . . . . . . . . 11 (𝜑𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
356355ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
357351, 352, 353, 354, 356ofrfval2 6957 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹 ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
358350, 357mpbird 247 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹)
359 itg2le 23551 . . . . . . . 8 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
360334, 338, 358, 359syl3anc 1366 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
36143, 333, 360jca32 557 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
362361expl 647 . . . . 5 (𝜑 → ((𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)))))
36342, 362syl5 34 . . . 4 (𝜑 → ((𝑦 ∈ ℚ ∧ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)))))
364363reximdv2 3043 . . 3 (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
3651a1i 11 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → 0 ∈ ℝ*)
36672adantl 481 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
367 itg2cl 23544 . . . . . . 7 (𝐹:ℝ⟶(0[,]+∞) → (∫2𝐹) ∈ ℝ*)
368337, 367syl 17 . . . . . 6 (𝜑 → (∫2𝐹) ∈ ℝ*)
369368adantr 480 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2𝐹) ∈ ℝ*)
370 xrltletr 12026 . . . . 5 ((0 ∈ ℝ* ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
371365, 366, 369, 370syl3anc 1366 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
372371rexlimdva 3060 . . 3 (𝜑 → (∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
373364, 372syld 47 . 2 (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2𝐹)))
37436, 373mpd 15 1 (𝜑 → 0 < (∫2𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cin 3606  wss 3607  c0 3948  ifcif 4119   class class class wbr 4685  cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144  cres 5145  cima 5146   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  𝑟 cofr 6938  supcsup 8387  cc 9972  cr 9973  0cc0 9974   + caddc 9977   · cmul 9979  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111   < clt 10112  cle 10113  cmin 10304  -cneg 10305  cq 11826  +crp 11870  (,)cioo 12213  [,)cico 12215  [,]cicc 12216  abscabs 14018  cnccncf 22726  vol*covol 23277  volcvol 23278  2citg2 23430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-ofr 6940  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-rest 16130  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cmp 21238  df-cncf 22728  df-ovol 23279  df-vol 23280  df-mbf 23433  df-itg1 23434  df-itg2 23435  df-0p 23482
This theorem is referenced by:  itggt0cn  33612
  Copyright terms: Public domain W3C validator