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

Theorem itg2gt0cn 33083
 Description: itg2gt0 23428 holds on functions continuous on an open interval in the absence of ax-cc 9202. 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 10031 . . . 4 0 ∈ ℝ*
21a1i 11 . . 3 (𝜑 → 0 ∈ ℝ*)
3 imassrn 5440 . . . . 5 (𝐹 “ (𝑋(,)𝑌)) ⊆ ran 𝐹
4 itg2gt0cn.3 . . . . . . 7 (𝜑𝐹:ℝ⟶(0[,)+∞))
5 frn 6012 . . . . . . 7 (𝐹:ℝ⟶(0[,)+∞) → ran 𝐹 ⊆ (0[,)+∞))
64, 5syl 17 . . . . . 6 (𝜑 → ran 𝐹 ⊆ (0[,)+∞))
7 icossxr 12197 . . . . . 6 (0[,)+∞) ⊆ ℝ*
86, 7syl6ss 3600 . . . . 5 (𝜑 → ran 𝐹 ⊆ ℝ*)
93, 8syl5ss 3599 . . . 4 (𝜑 → (𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*)
10 supxrcl 12085 . . . 4 ((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
119, 10syl 17 . . 3 (𝜑 → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
12 itg2gt0cn.2 . . . . . 6 (𝜑𝑋 < 𝑌)
13 ltrelxr 10044 . . . . . . . . . 10 < ⊆ (ℝ* × ℝ*)
1413ssbri 4662 . . . . . . . . 9 (𝑋 < 𝑌𝑋(ℝ* × ℝ*)𝑌)
1512, 14syl 17 . . . . . . . 8 (𝜑𝑋(ℝ* × ℝ*)𝑌)
16 brxp 5112 . . . . . . . 8 (𝑋(ℝ* × ℝ*)𝑌 ↔ (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
1715, 16sylib 208 . . . . . . 7 (𝜑 → (𝑋 ∈ ℝ*𝑌 ∈ ℝ*))
18 ioon0 12140 . . . . . . 7 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
1917, 18syl 17 . . . . . 6 (𝜑 → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
2012, 19mpbird 247 . . . . 5 (𝜑 → (𝑋(,)𝑌) ≠ ∅)
21 itg2gt0cn.5 . . . . . 6 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹𝑥))
2221ralrimiva 2965 . . . . 5 (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
23 r19.2z 4037 . . . . 5 (((𝑋(,)𝑌) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)) → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
2420, 22, 23syl2anc 692 . . . 4 (𝜑 → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥))
25 supxrlub 12095 . . . . . 6 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
269, 1, 25sylancl 693 . . . . 5 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
27 ffn 6004 . . . . . . 7 (𝐹:ℝ⟶(0[,)+∞) → 𝐹 Fn ℝ)
284, 27syl 17 . . . . . 6 (𝜑𝐹 Fn ℝ)
29 ioossre 12174 . . . . . 6 (𝑋(,)𝑌) ⊆ ℝ
30 breq2 4622 . . . . . . 7 (𝑦 = (𝐹𝑥) → (0 < 𝑦 ↔ 0 < (𝐹𝑥)))
3130rexima 6452 . . . . . 6 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3228, 29, 31sylancl 693 . . . . 5 (𝜑 → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3326, 32bitrd 268 . . . 4 (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹𝑥)))
3424, 33mpbird 247 . . 3 (𝜑 → 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))
35 qbtwnxr 11973 . . 3 ((0 ∈ ℝ* ∧ sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ* ∧ 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
362, 11, 34, 35syl3anc 1323 . 2 (𝜑 → ∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
37 qre 11737 . . . . . . . . 9 (𝑦 ∈ ℚ → 𝑦 ∈ ℝ)
3837adantr 481 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
39 simpr 477 . . . . . . . 8 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 0 < 𝑦)
4038, 39elrpd 11813 . . . . . . 7 ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ+)
4140anim1i 591 . . . . . 6 (((𝑦 ∈ ℚ ∧ 0 < 𝑦) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
4241anasss 678 . . . . 5 ((𝑦 ∈ ℚ ∧ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
43 simplr 791 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝑦 ∈ ℝ+)
44 rpxr 11784 . . . . . . . . . . 11 (𝑦 ∈ ℝ+𝑦 ∈ ℝ*)
45 supxrlub 12095 . . . . . . . . . . 11 (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*𝑦 ∈ ℝ*) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
469, 44, 45syl2an 494 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
47 breq2 4622 . . . . . . . . . . . . 13 (𝑧 = (𝐹𝑥) → (𝑦 < 𝑧𝑦 < (𝐹𝑥)))
4847rexima 6452 . . . . . . . . . . . 12 ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
4928, 29, 48sylancl 693 . . . . . . . . . . 11 (𝜑 → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
5049adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
5146, 50bitrd 268 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥)))
521a1i 11 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 ∈ ℝ*)
53 ioorp 12190 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) = ℝ+
54 ioossicc 12198 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) ⊆ (0[,]+∞)
5553, 54eqsstr3i 3620 . . . . . . . . . . . . . . . . . . 19 + ⊆ (0[,]+∞)
5655sseli 3584 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+𝑦 ∈ (0[,]+∞))
57 0e0iccpnf 12222 . . . . . . . . . . . . . . . . . 18 0 ∈ (0[,]+∞)
58 ifcl 4107 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
5956, 57, 58sylancl 693 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+ → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
6059adantr 481 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
61 eqid 2626 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
6260, 61fmptd 6341 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
63 itg2cl 23400 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6462, 63syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
6564ad5antlr 770 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
66 ifcl 4107 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6756, 57, 66sylancl 693 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+ → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
6867adantr 481 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ+𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
69 eqid 2626 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
7068, 69fmptd 6341 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
71 itg2cl 23400 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
7270, 71syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
7372ad5antlr 770 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
74 rpre 11783 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
7574ad4antlr 768 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ ℝ)
76 ioombl 23235 . . . . . . . . . . . . . . . . . . 19 (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol
77 mblvol 23200 . . . . . . . . . . . . . . . . . . 19 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . 18 (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
79 elioore 12144 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ)
8079ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ)
81 rpre 11783 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
8281adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈ ℝ)
8380, 82resubcld 10403 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ)
8483adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ)
8583rexrd 10034 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) ∈ ℝ*)
8685adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) ∈ ℝ*)
8717simpld 475 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 ∈ ℝ*)
8887ad5antr 769 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ*)
8917simprd 479 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌 ∈ ℝ*)
9089ad5antr 769 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑌 ∈ ℝ*)
9187ad4antr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 ∈ ℝ*)
92 xrltnle 10050 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
9385, 91, 92syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑥𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥𝑧)))
9493biimpar 502 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → (𝑥𝑧) < 𝑋)
9512ad5antr 769 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 < 𝑌)
96 xrre2 11943 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑥𝑧) ∈ ℝ*𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) < 𝑋𝑋 < 𝑌)) → 𝑋 ∈ ℝ)
9786, 88, 90, 94, 95, 96syl32anc 1331 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥𝑧)) → 𝑋 ∈ ℝ)
9884, 97ifclda 4097 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ)
9989ad5antr 769 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ*)
10082, 80readdcld 10014 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ)
101100adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
102 mnfxr 10041 . . . . . . . . . . . . . . . . . . . . . . . 24 -∞ ∈ ℝ*
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → -∞ ∈ ℝ*)
104 mnfle 11913 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∈ ℝ* → -∞ ≤ 𝑋)
10587, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → -∞ ≤ 𝑋)
106103, 87, 89, 105, 12xrlelttrd 11935 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → -∞ < 𝑌)
107106ad5antr 769 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → -∞ < 𝑌)
108 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ≤ (𝑧 + 𝑥))
109 xrre 11942 . . . . . . . . . . . . . . . . . . . . 21 (((𝑌 ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ) ∧ (-∞ < 𝑌𝑌 ≤ (𝑧 + 𝑥))) → 𝑌 ∈ ℝ)
11099, 101, 107, 108, 109syl22anc 1324 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ)
111100adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
112110, 111ifclda 4097 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ)
11380rexrd 10034 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ*)
11489ad4antr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑌 ∈ ℝ*)
115 rpgt0 11788 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℝ+ → 0 < 𝑧)
116115adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑧)
11782, 80ltsubposd 10558 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧 ↔ (𝑥𝑧) < 𝑥))
118116, 117mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑥)
119 eliooord 12172 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑥𝑥 < 𝑌))
120119simprd 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 < 𝑌)
121120ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < 𝑌)
12285, 113, 114, 118, 121xrlttrd 11934 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < 𝑌)
12382, 80ltaddpos2d 10557 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧𝑥 < (𝑧 + 𝑥)))
124116, 123mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < (𝑧 + 𝑥))
12583, 80, 100, 118, 124lttrd 10143 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < (𝑧 + 𝑥))
126 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < 𝑌 ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
127 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥𝑧) < (𝑧 + 𝑥) ↔ (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
128126, 127ifboth 4101 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑧) < 𝑌 ∧ (𝑥𝑧) < (𝑧 + 𝑥)) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
129122, 125, 128syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
13012ad4antr 767 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑌)
131100rexrd 10034 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ*)
132119simpld 475 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (𝑋(,)𝑌) → 𝑋 < 𝑥)
133132ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑥)
13491, 113, 131, 133, 124xrlttrd 11934 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < (𝑧 + 𝑥))
135 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < 𝑌𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
136 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < (𝑧 + 𝑥) ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
137135, 136ifboth 4101 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 < 𝑌𝑋 < (𝑧 + 𝑥)) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
138130, 134, 137syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
139 breq1 4621 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑧) = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → ((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
140 breq1 4621 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) → (𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
141139, 140ifboth 4101 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∧ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
142129, 138, 141syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
14398, 112, 142ltled 10130 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
144 ovolioo 23238 . . . . . . . . . . . . . . . . . . 19 ((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ∈ ℝ ∧ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ ∧ if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14598, 112, 143, 144syl3anc 1323 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol*‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
14678, 145syl5eq 2672 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
147112, 98resubcld 10403 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)) ∈ ℝ)
148146, 147eqeltrd 2704 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ)
149 rpgt0 11788 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+ → 0 < 𝑦)
150149ad4antlr 768 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑦)
15198, 112posdifd 10559 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋))))
152142, 151mpbid 222 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)))
153152, 146breqtrrd 4646 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
15475, 148, 150, 153mulgt0d 10137 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
155 iooin 12148 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 ∈ ℝ*𝑌 ∈ ℝ*) ∧ ((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*)) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
15691, 114, 85, 131, 155syl22anc 1324 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
157156eleq2d 2689 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ 𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
158157ifbid 4085 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))
159158mpteq2dv 4710 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)))
160159fveq2d 6154 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))))
16176a1i 11 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol)
162 rpge0 11789 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
163 elrege0 12217 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦))
16474, 162, 163sylanbrc 697 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+𝑦 ∈ (0[,)+∞))
165164ad4antlr 768 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ (0[,)+∞))
166 itg2const 23408 . . . . . . . . . . . . . . . . 17 (((if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol ∧ (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ ∧ 𝑦 ∈ (0[,)+∞)) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
167161, 148, 165, 166syl3anc 1323 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
168160, 167eqtrd 2660 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥𝑧), (𝑥𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
169154, 168breqtrrd 4646 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
170169adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
17162ad5antlr 770 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
17270ad5antlr 770 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
173 oveq1 6612 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 = 𝑤 → (𝑢𝑥) = (𝑤𝑥))
174173fveq2d 6154 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = 𝑤 → (abs‘(𝑢𝑥)) = (abs‘(𝑤𝑥)))
175174breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑤 → ((abs‘(𝑢𝑥)) < 𝑧 ↔ (abs‘(𝑤𝑥)) < 𝑧))
176 fveq2 6150 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑤 → (𝐹𝑢) = (𝐹𝑤))
177176oveq1d 6620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 = 𝑤 → ((𝐹𝑢) − (𝐹𝑥)) = ((𝐹𝑤) − (𝐹𝑥)))
178177fveq2d 6154 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = 𝑤 → (abs‘((𝐹𝑢) − (𝐹𝑥))) = (abs‘((𝐹𝑤) − (𝐹𝑥))))
179178breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑤 → ((abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
180175, 179imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑤 → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ↔ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
181180rspccva 3299 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
182 breq1 4621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
183 breq1 4621 . . . . . . . . . . . . . . . . . . . . . . 23 (0 = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
18474leidd 10539 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℝ+𝑦𝑦)
185184ad6antlr 772 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦𝑦)
18679ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑥 ∈ ℝ)
18781ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 𝑧 ∈ ℝ)
188186, 187resubcld 10403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ)
189188rexrd 10034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑥𝑧) ∈ ℝ*)
190187, 186readdcld 10014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ)
191190rexrd 10034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ*)
192 elioo2 12155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
193189, 191, 192syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
194 3anass 1040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑤 ∈ ℝ ∧ (𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
195193, 194syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
196 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
19779ad5antlr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℝ)
198196, 197resubcld 10403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑤𝑥) ∈ ℝ)
19981ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℝ)
200198, 199absltd 14097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ (-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧)))
201199renegcld 10402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → -𝑧 ∈ ℝ)
202197, 201, 196ltaddsub2d 10573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ -𝑧 < (𝑤𝑥)))
203197recnd 10013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℂ)
204199recnd 10013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℂ)
205203, 204negsubd 10343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑥 + -𝑧) = (𝑥𝑧))
206205breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ (𝑥𝑧) < 𝑤))
207202, 206bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (-𝑧 < (𝑤𝑥) ↔ (𝑥𝑧) < 𝑤))
208196, 197, 199ltsubaddd 10568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑤𝑥) < 𝑧𝑤 < (𝑧 + 𝑥)))
209207, 208anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((-𝑧 < (𝑤𝑥) ∧ (𝑤𝑥) < 𝑧) ↔ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
210200, 209bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤𝑥)) < 𝑧 ↔ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥))))
211210pm5.32da 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧) ↔ (𝑤 ∈ ℝ ∧ ((𝑥𝑧) < 𝑤𝑤 < (𝑧 + 𝑥)))))
212195, 211bitr4d 271 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)))
213212biimpa 501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧))
214 pm3.35 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((abs‘(𝑤𝑥)) < 𝑧 ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
215214ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧) → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))
21674ad6antlr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ∈ ℝ)
217 rge0ssre 12219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0[,)+∞) ⊆ ℝ
2184ad4antr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
219218ffvelrnda 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
220217, 219sseldi 3586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ ℝ)
221220adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑤) ∈ ℝ)
2224adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑦 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
223222ffvelrnda 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
224217, 223sseldi 3586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
22579, 224sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℝ)
226225ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
227220, 226resubcld 10403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑤) − (𝐹𝑥)) ∈ ℝ)
22874ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
229225, 228resubcld 10403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
230229ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹𝑥) − 𝑦) ∈ ℝ)
231227, 230absltd 14097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
232225recnd 10013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹𝑥) ∈ ℂ)
233 rpcn 11785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
234233ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
235232, 234negsubdi2d 10353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
236235ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → -((𝐹𝑥) − 𝑦) = (𝑦 − (𝐹𝑥)))
237236breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
238237anbi1d 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((-((𝐹𝑥) − 𝑦) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦)) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
239231, 238bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦) ↔ ((𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)) ∧ ((𝐹𝑤) − (𝐹𝑥)) < ((𝐹𝑥) − 𝑦))))
240239simprbda 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥)))
241225ad4antr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝐹𝑥) ∈ ℝ)
242216, 221, 241ltsub1d 10581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → (𝑦 < (𝐹𝑤) ↔ (𝑦 − (𝐹𝑥)) < ((𝐹𝑤) − (𝐹𝑥))))
243240, 242mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 < (𝐹𝑤))
244216, 221, 243ltled 10130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) → 𝑦 ≤ (𝐹𝑤))
245215, 244sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
246245an4s 868 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ (𝑤 ∈ ℝ ∧ (abs‘(𝑤𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹𝑤))
247213, 246syldan 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ (𝐹𝑤))
248247iftrued 4071 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) = 𝑦)
249185, 248breqtrrd 4646 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
250 0le0 11055 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ≤ 0
251 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 𝑦 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
252 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0)))
253251, 252ifboth 4101 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ≤ 𝑦 ∧ 0 ≤ 0) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
254162, 250, 253sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℝ+ → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
255254ad6antlr 772 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ ¬ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))) → 0 ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
256182, 183, 249, 255ifbothda 4100 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
257181, 256sylan2 491 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌))) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
258257anassrs 679 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
259 iftrue 4069 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
260259adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
261 iftrue 4069 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
262261adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹𝑤), 𝑦, 0))
263258, 260, 2623brtr4d 4650 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0))
264263ex 450 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)))
265250a1i 11 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑋(,)𝑌) → 0 ≤ 0)
266 iffalse 4072 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = 0)
267 iffalse 4072 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0) = 0)
268265, 266, 2673brtr4d 4650 . . . . . . . . . . . . . . . . . 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 3779 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))))
271 ifbi 4084 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
272270, 271ax-mp 5 . . . . . . . . . . . . . . . . . 18 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)
273 ifan 4111 . . . . . . . . . . . . . . . . . 18 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
274272, 273eqtri 2648 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
275 fveq2 6150 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑤 → (𝐹𝑣) = (𝐹𝑤))
276275breq2d 4630 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑤 → (𝑦 ≤ (𝐹𝑣) ↔ 𝑦 ≤ (𝐹𝑤)))
277276elrab 3351 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)))
278 ifbi 4084 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤))) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0))
279277, 278ax-mp 5 . . . . . . . . . . . . . . . . . 18 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0)
280 ifan 4111 . . . . . . . . . . . . . . . . . 18 if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹𝑤)), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
281279, 280eqtri 2648 . . . . . . . . . . . . . . . . 17 if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹𝑤), 𝑦, 0), 0)
282269, 274, 2813brtr4g 4652 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
283282ralrimivw 2966 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))
284 reex 9972 . . . . . . . . . . . . . . . . 17 ℝ ∈ V
285284a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ℝ ∈ V)
28659ad6antlr 772 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
28767ad6antlr 772 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
288 eqidd 2627 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))
289 eqidd 2627 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
290285, 286, 287, 288, 289ofrfval2 6869 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
291283, 290mpbird 247 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
292 itg2le 23407 . . . . . . . . . . . . . 14 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
293171, 172, 291, 292syl3anc 1323 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
29452, 65, 73, 170, 293xrltletrd 11936 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
295 itg2gt0cn.cn . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
296295ad3antrrr 765 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
297 simplr 791 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 𝑥 ∈ (𝑋(,)𝑌))
298 fssres 6029 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:ℝ⟶(0[,)+∞) ∧ (𝑋(,)𝑌) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
29929, 298mpan2 706 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:ℝ⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
300 fss 6015 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
301217, 300mpan2 706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
3024, 299, 3013syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
303302adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℝ+) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
304303ffvelrnda 6316 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ∈ ℝ)
305304, 228resubcld 10403 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
306305adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
307228, 304posdifd 10559 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
308307biimpa 501 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))
309306, 308elrpd 11813 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+)
310 cncfi 22600 . . . . . . . . . . . . . . . 16 (((𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ 𝑥 ∈ (𝑋(,)𝑌) ∧ (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
311296, 297, 309, 310syl3anc 1323 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
312311ex 450 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))))
313 fvres 6165 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
314313breq2d 4630 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑋(,)𝑌) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
315314adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹𝑥)))
316 fvres 6165 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
317316adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹𝑢))
318313ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹𝑥))
319317, 318oveq12d 6623 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) = ((𝐹𝑢) − (𝐹𝑥)))
320319fveq2d 6154 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) = (abs‘((𝐹𝑢) − (𝐹𝑥))))
321313oveq1d 6620 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝑋(,)𝑌) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
322321ad2antlr 762 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹𝑥) − 𝑦))
323320, 322breq12d 4631 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ↔ (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
324323imbi2d 330 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
325324ralbidva 2984 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
326325rexbidv 3050 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
327312, 315, 3263imtr3d 282 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹𝑥) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦))))
328327imp 445 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → ∃𝑧 ∈ ℝ+𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢𝑥)) < 𝑧 → (abs‘((𝐹𝑢) − (𝐹𝑥))) < ((𝐹𝑥) − 𝑦)))
329294, 328r19.29a 3076 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹𝑥)) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
330329ex 450 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
331330rexlimdva 3029 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → (∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
33251, 331sylbid 230 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))))
333332imp 445 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))))
33470ad2antlr 762 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
335 icossicc 12199 . . . . . . . . . 10 (0[,)+∞) ⊆ (0[,]+∞)
336 fss 6015 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
3374, 335, 336sylancl 693 . . . . . . . . 9 (𝜑𝐹:ℝ⟶(0[,]+∞))
338337ad2antrr 761 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹:ℝ⟶(0[,]+∞))
339 breq1 4621 . . . . . . . . . . . 12 (𝑦 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (𝑦 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
340 breq1 4621 . . . . . . . . . . . 12 (0 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) → (0 ≤ (𝐹𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
341277simprbi 480 . . . . . . . . . . . . 13 (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)} → 𝑦 ≤ (𝐹𝑤))
342341adantl 482 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 𝑦 ≤ (𝐹𝑤))
3434ffvelrnda 6316 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ℝ) → (𝐹𝑤) ∈ (0[,)+∞))
344 elrege0 12217 . . . . . . . . . . . . . . 15 ((𝐹𝑤) ∈ (0[,)+∞) ↔ ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
345343, 344sylib 208 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ℝ) → ((𝐹𝑤) ∈ ℝ ∧ 0 ≤ (𝐹𝑤)))
346345simprd 479 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ) → 0 ≤ (𝐹𝑤))
347346adantr 481 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ ¬ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}) → 0 ≤ (𝐹𝑤))
348339, 340, 342, 347ifbothda 4100 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
349348ralrimiva 2965 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
350349ad2antrr 761 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤))
351284a1i 11 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ℝ ∈ V)
35267ad3antlr 766 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
353 fvex 6160 . . . . . . . . . . 11 (𝐹𝑤) ∈ V
354353a1i 11 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → (𝐹𝑤) ∈ V)
355 eqidd 2627 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)))
3564feqmptd 6207 . . . . . . . . . . 11 (𝜑𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
357356ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹𝑤)))
358351, 352, 354, 355, 357ofrfval2 6869 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹 ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0) ≤ (𝐹𝑤)))
359350, 358mpbird 247 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹)
360 itg2le 23407 . . . . . . . 8 (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0)) ∘𝑟𝐹) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
361334, 338, 359, 360syl3anc 1323 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))
36243, 333, 361jca32 557 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
363362expl 647 . . . . 5 (𝜑 → ((𝑦 ∈ ℝ+𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)))))
36442, 363syl5 34 . . . 4 (𝜑 → ((𝑦 ∈ ℚ ∧ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)))))
365364reximdv2 3013 . . 3 (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹))))
3661a1i 11 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → 0 ∈ ℝ*)
36772adantl 482 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ*)
368 itg2cl 23400 . . . . . . 7 (𝐹:ℝ⟶(0[,]+∞) → (∫2𝐹) ∈ ℝ*)
369337, 368syl 17 . . . . . 6 (𝜑 → (∫2𝐹) ∈ ℝ*)
370369adantr 481 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → (∫2𝐹) ∈ ℝ*)
371 xrltletr 11932 . . . . 5 ((0 ∈ ℝ* ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∈ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
372366, 367, 370, 371syl3anc 1323 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
373372rexlimdva 3029 . . 3 (𝜑 → (∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹𝑣)}, 𝑦, 0))) ≤ (∫2𝐹)) → 0 < (∫2𝐹)))
374365, 373syld 47 . 2 (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2𝐹)))
37536, 374mpd 15 1 (𝜑 → 0 < (∫2𝐹))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1992   ≠ wne 2796  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3191   ∩ cin 3559   ⊆ wss 3560  ∅c0 3896  ifcif 4063   class class class wbr 4618   ↦ cmpt 4678   × cxp 5077  dom cdm 5079  ran crn 5080   ↾ cres 5081   “ cima 5082   Fn wfn 5845  ⟶wf 5846  ‘cfv 5850  (class class class)co 6605   ∘𝑟 cofr 6850  supcsup 8291  ℂcc 9879  ℝcr 9880  0cc0 9881   + caddc 9884   · cmul 9886  +∞cpnf 10016  -∞cmnf 10017  ℝ*cxr 10018   < clt 10019   ≤ cle 10020   − cmin 10211  -cneg 10212  ℚcq 11732  ℝ+crp 11776  (,)cioo 12114  [,)cico 12116  [,]cicc 12117  abscabs 13903  –cn→ccncf 22582  vol*covol 23133  volcvol 23134  ∫2citg2 23286 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-inf2 8483  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959  ax-addf 9960 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-disj 4589  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-isom 5859  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-of 6851  df-ofr 6852  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-er 7688  df-map 7805  df-pm 7806  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-fi 8262  df-sup 8293  df-inf 8294  df-oi 8360  df-card 8710  df-cda 8935  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-n0 11238  df-z 11323  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12118  df-ico 12120  df-icc 12121  df-fz 12266  df-fzo 12404  df-fl 12530  df-seq 12739  df-exp 12798  df-hash 13055  df-cj 13768  df-re 13769  df-im 13770  df-sqrt 13904  df-abs 13905  df-clim 14148  df-rlim 14149  df-sum 14346  df-rest 15999  df-topgen 16020  df-psmet 19652  df-xmet 19653  df-met 19654  df-bl 19655  df-mopn 19656  df-top 20616  df-bases 20617  df-topon 20618  df-cmp 21095  df-cncf 22584  df-ovol 23135  df-vol 23136  df-mbf 23289  df-itg1 23290  df-itg2 23291  df-0p 23338 This theorem is referenced by:  itggt0cn  33100
 Copyright terms: Public domain W3C validator