Theorem itg2gt0cn 32635

Description: itg2gt0 23333 holds on functions continuous on an open interval in the absence of ax-cc 9140. 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.

Step	Hyp	Ref	Expression
1		0xr 9965	. . . 4 ⊢ 0 ∈ ℝ*
2	1	a1i 11	. . 3 ⊢ (𝜑 → 0 ∈ ℝ*)
3		imassrn 5396	. . . . 5 ⊢ (𝐹 “ (𝑋(,)𝑌)) ⊆ ran 𝐹
4		itg2gt0cn.3	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
5		frn 5966	. . . . . . 7 ⊢ (𝐹:ℝ⟶(0[,)+∞) → ran 𝐹 ⊆ (0[,)+∞))
6	4, 5	syl 17	. . . . . 6 ⊢ (𝜑 → ran 𝐹 ⊆ (0[,)+∞))
7		icossxr 12129	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ*
8	6, 7	syl6ss 3580	. . . . 5 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ*)
9	3, 8	syl5ss 3579	. . . 4 ⊢ (𝜑 → (𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ*)
10		supxrcl 12017	. . . 4 ⊢ ((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
11	9, 10	syl 17	. . 3 ⊢ (𝜑 → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ*)
12		itg2gt0cn.2	. . . . . 6 ⊢ (𝜑 → 𝑋 < 𝑌)
13		ltrelxr 9978	. . . . . . . . . 10 ⊢ < ⊆ (ℝ* × ℝ*)
14	13	ssbri 4627	. . . . . . . . 9 ⊢ (𝑋 < 𝑌 → 𝑋(ℝ* × ℝ*)𝑌)
15	12, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋(ℝ* × ℝ*)𝑌)
16		brxp 5071	. . . . . . . 8 ⊢ (𝑋(ℝ* × ℝ*)𝑌 ↔ (𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ*))
17	15, 16	sylib 207	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ*))
18		ioon0 12072	. . . . . . 7 ⊢ ((𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ*) → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
19	17, 18	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌))
20	12, 19	mpbird 246	. . . . 5 ⊢ (𝜑 → (𝑋(,)𝑌) ≠ ∅)
21		itg2gt0cn.5	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹‘𝑥))
22	21	ralrimiva 2949	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))
23		r19.2z 4012	. . . . 5 ⊢ (((𝑋(,)𝑌) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))
24	20, 22, 23	syl2anc 691	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))
25		supxrlub 12027	. . . . . 6 ⊢ (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
26	9, 1, 25	sylancl 693	. . . . 5 ⊢ (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦))
27		ffn 5958	. . . . . . 7 ⊢ (𝐹:ℝ⟶(0[,)+∞) → 𝐹 Fn ℝ)
28	4, 27	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 Fn ℝ)
29		ioossre 12106	. . . . . 6 ⊢ (𝑋(,)𝑌) ⊆ ℝ
30		breq2 4587	. . . . . . 7 ⊢ (𝑦 = (𝐹‘𝑥) → (0 < 𝑦 ↔ 0 < (𝐹‘𝑥)))
31	30	rexima 6401	. . . . . 6 ⊢ ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)))
32	28, 29, 31	sylancl 693	. . . . 5 ⊢ (𝜑 → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)))
33	26, 32	bitrd 267	. . . 4 ⊢ (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)))
34	24, 33	mpbird 246	. . 3 ⊢ (𝜑 → 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))
35		qbtwnxr 11905	. . 3 ⊢ ((0 ∈ ℝ* ∧ sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈ ℝ* ∧ 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
36	2, 11, 34, 35	syl3anc 1318	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
37		qre 11669	. . . . . . . . 9 ⊢ (𝑦 ∈ ℚ → 𝑦 ∈ ℝ)
38	37	adantr 480	. . . . . . . 8 ⊢ ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
39		simpr 476	. . . . . . . 8 ⊢ ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 0 < 𝑦)
40	38, 39	elrpd 11745	. . . . . . 7 ⊢ ((𝑦 ∈ ℚ ∧ 0 < 𝑦) → 𝑦 ∈ ℝ+)
41	40	anim1i 590	. . . . . 6 ⊢ (((𝑦 ∈ ℚ ∧ 0 < 𝑦) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
42	41	anasss 677	. . . . 5 ⊢ ((𝑦 ∈ ℚ ∧ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+ ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )))
43		simplr 788	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝑦 ∈ ℝ+)
44		rpxr 11716	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ*)
45		supxrlub 12027	. . . . . . . . . . 11 ⊢ (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
46	9, 44, 45	syl2an 493	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧))
47		breq2 4587	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹‘𝑥) → (𝑦 < 𝑧 ↔ 𝑦 < (𝐹‘𝑥)))
48	47	rexima 6401	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥)))
49	28, 29, 48	sylancl 693	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥)))
50	49	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥)))
51	46, 50	bitrd 267	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥)))
52	1	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 ∈ ℝ*)
53		ioorp 12122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0(,)+∞) = ℝ+
54		ioossicc 12130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0(,)+∞) ⊆ (0[,]+∞)
55	53, 54	eqsstr3i 3599	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ+ ⊆ (0[,]+∞)
56	55	sseli 3564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ (0[,]+∞))
57		0e0iccpnf 12154	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ (0[,]+∞)
58		ifcl 4080	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
59	56, 57, 58	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ+ → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
60	59	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
61		eqid 2610	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
62	60, 61	fmptd 6292	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
63		itg2cl 23305	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
64	62, 63	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
65	64	ad5antlr 767	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈ ℝ*)
66		ifcl 4080	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
67	56, 57, 66	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ+ → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
68	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
69		eqid 2610	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))
70	68, 69	fmptd 6292	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ+ → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
71		itg2cl 23305	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈ ℝ*)
72	70, 71	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈ ℝ*)
73	72	ad5antlr 767	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈ ℝ*)
74		rpre 11715	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
75	74	ad4antlr 765	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ ℝ)
76		ioombl 23140	. . . . . . . . . . . . . . . . . . 19 ⊢ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol
77		mblvol 23105	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol → (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
78	76, 77	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
79		elioore 12076	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ)
80	79	ad3antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ)
81		rpre 11715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ)
82	81	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈ ℝ)
83	80, 82	resubcld 10337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) ∈ ℝ)
84	83	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) ∈ ℝ)
85	83	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) ∈ ℝ*)
86	85	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) ∈ ℝ*)
87	17	simpld 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑋 ∈ ℝ*)
88	87	ad5antr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 ∈ ℝ*)
89	17	simprd 478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑌 ∈ ℝ*)
90	89	ad5antr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥 − 𝑧)) → 𝑌 ∈ ℝ*)
91	87	ad4antr 764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 ∈ ℝ*)
92		xrltnle 9984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 − 𝑧) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) → ((𝑥 − 𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥 − 𝑧)))
93	85, 91, 92	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑥 − 𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥 − 𝑧)))
94	93	biimpar 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) < 𝑋)
95	12	ad5antr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 < 𝑌)
96		xrre2 11875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑥 − 𝑧) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ*) ∧ ((𝑥 − 𝑧) < 𝑋 ∧ 𝑋 < 𝑌)) → 𝑋 ∈ ℝ)
97	86, 88, 90, 94, 95, 96	syl32anc 1326	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 ∈ ℝ)
98	84, 97	ifclda 4070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ∈ ℝ)
99	89	ad5antr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ*)
100	82, 80	readdcld 9948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ)
101	100	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
102		mnfxr 9975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ -∞ ∈ ℝ*
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → -∞ ∈ ℝ*)
104		mnfle 11845	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑋 ∈ ℝ* → -∞ ≤ 𝑋)
105	87, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → -∞ ≤ 𝑋)
106	103, 87, 89, 105, 12	xrlelttrd 11867	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → -∞ < 𝑌)
107	106	ad5antr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → -∞ < 𝑌)
108		simpr 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ≤ (𝑧 + 𝑥))
109		xrre 11874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑌 ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ) ∧ (-∞ < 𝑌 ∧ 𝑌 ≤ (𝑧 + 𝑥))) → 𝑌 ∈ ℝ)
110	99, 101, 107, 108, 109	syl22anc 1319	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ)
111	100	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ)
112	110, 111	ifclda 4070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ)
113	80	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ ℝ*)
114	89	ad4antr 764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑌 ∈ ℝ*)
115		rpgt0 11720	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ ℝ+ → 0 < 𝑧)
116	115	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑧)
117	82, 80	ltsubposd 10492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧 ↔ (𝑥 − 𝑧) < 𝑥))
118	116, 117	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < 𝑥)
119		eliooord 12104	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑥 ∧ 𝑥 < 𝑌))
120	119	simprd 478	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 < 𝑌)
121	120	ad3antlr 763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < 𝑌)
122	85, 113, 114, 118, 121	xrlttrd 11866	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < 𝑌)
123	82, 80	ltaddpos2d 10491	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 < 𝑧 ↔ 𝑥 < (𝑧 + 𝑥)))
124	116, 123	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < (𝑧 + 𝑥))
125	83, 80, 100, 118, 124	lttrd 10077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < (𝑧 + 𝑥))
126		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥 − 𝑧) < 𝑌 ↔ (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
127		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥 − 𝑧) < (𝑧 + 𝑥) ↔ (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
128	126, 127	ifboth 4074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 − 𝑧) < 𝑌 ∧ (𝑥 − 𝑧) < (𝑧 + 𝑥)) → (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
129	122, 125, 128	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
130	12	ad4antr 764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑌)
131	100	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ*)
132	119	simpld 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑋 < 𝑥)
133	132	ad3antlr 763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑥)
134	91, 113, 131, 133, 124	xrlttrd 11866	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < (𝑧 + 𝑥))
135		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < 𝑌 ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
136		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < (𝑧 + 𝑥) ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
137	135, 136	ifboth 4074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 < 𝑌 ∧ 𝑋 < (𝑧 + 𝑥)) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
138	130, 134, 137	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
139		breq1 4586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 − 𝑧) = if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) → ((𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
140		breq1 4586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) → (𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
141	139, 140	ifboth 4074	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∧ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
142	129, 138, 141	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
143	98, 112, 142	ltled 10064	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))
144		ovolioo 23143	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ∈ ℝ ∧ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ ∧ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)))
145	98, 112, 143, 144	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)))
146	78, 145	syl5eq 2656	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)))
147	112, 98	resubcld 10337	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)) ∈ ℝ)
148	146, 147	eqeltrd 2688	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ)
149		rpgt0 11720	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ+ → 0 < 𝑦)
150	149	ad4antlr 765	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < 𝑦)
151	98, 112	posdifd 10493	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))))
152	142, 151	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)))
153	152, 146	breqtrrd 4611	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
154	75, 148, 150, 153	mulgt0d 10071	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
155		iooin 12080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ*) ∧ ((𝑥 − 𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*)) → ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
156	91, 114, 85, 131, 155	syl22anc 1319	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))
157	156	eleq2d 2673	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ 𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))
158	157	ifbid 4058	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))
159	158	mpteq2dv 4673	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)))
160	159	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))))
161	76	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol)
162		rpge0 11721	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
163		elrege0 12149	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦))
164	74, 162, 163	sylanbrc 695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ (0[,)+∞))
165	164	ad4antlr 765	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈ (0[,)+∞))
166		itg2const 23313	. . . . . . . . . . . . . . . . 17 ⊢ (((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol ∧ (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ ∧ 𝑦 ∈ (0[,)+∞)) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
167	161, 148, 165, 166	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
168	160, 167	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))))
169	154, 168	breqtrrd 4611	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
170	169	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))))
171	62	ad5antlr 767	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞))
172	70	ad5antlr 767	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
173		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 = 𝑤 → (𝑢 − 𝑥) = (𝑤 − 𝑥))
174	173	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = 𝑤 → (abs‘(𝑢 − 𝑥)) = (abs‘(𝑤 − 𝑥)))
175	174	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑤 → ((abs‘(𝑢 − 𝑥)) < 𝑧 ↔ (abs‘(𝑤 − 𝑥)) < 𝑧))
176		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑤 → (𝐹‘𝑢) = (𝐹‘𝑤))
177	176	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 = 𝑤 → ((𝐹‘𝑢) − (𝐹‘𝑥)) = ((𝐹‘𝑤) − (𝐹‘𝑥)))
178	177	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))))
179	178	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑤 → ((abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦) ↔ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))
180	175, 179	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑤 → (((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ↔ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))))
181	180	rspccva 3281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))
182		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (𝑦 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)))
183		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)))
184	74	leidd 10473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≤ 𝑦)
185	184	ad6antlr 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ 𝑦)
186	79	ad4antlr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 𝑥 ∈ ℝ)
187	81	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 𝑧 ∈ ℝ)
188	186, 187	resubcld 10337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑥 − 𝑧) ∈ ℝ)
189	188	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑥 − 𝑧) ∈ ℝ*)
190	187, 186	readdcld 9948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ)
191	190	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ*)
192		elioo2 12087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 − 𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))
193	189, 191, 192	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))
194		3anass 1035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))
195	193, 194	syl6bb 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))))
196		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
197	79	ad5antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℝ)
198	196, 197	resubcld 10337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑤 − 𝑥) ∈ ℝ)
199	81	ad3antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℝ)
200	198, 199	absltd 14016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤 − 𝑥)) < 𝑧 ↔ (-𝑧 < (𝑤 − 𝑥) ∧ (𝑤 − 𝑥) < 𝑧)))
201	199	renegcld 10336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → -𝑧 ∈ ℝ)
202	197, 201, 196	ltaddsub2d 10507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ -𝑧 < (𝑤 − 𝑥)))
203	197	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℂ)
204	199	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℂ)
205	203, 204	negsubd 10277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑥 + -𝑧) = (𝑥 − 𝑧))
206	205	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ (𝑥 − 𝑧) < 𝑤))
207	202, 206	bitr3d 269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (-𝑧 < (𝑤 − 𝑥) ↔ (𝑥 − 𝑧) < 𝑤))
208	196, 197, 199	ltsubaddd 10502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑤 − 𝑥) < 𝑧 ↔ 𝑤 < (𝑧 + 𝑥)))
209	207, 208	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((-𝑧 < (𝑤 − 𝑥) ∧ (𝑤 − 𝑥) < 𝑧) ↔ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))
210	200, 209	bitrd 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤 − 𝑥)) < 𝑧 ↔ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))
211	210	pm5.32da 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))))
212	195, 211	bitr4d 270	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)))
213	212	biimpa 500	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧))
214		pm3.35 609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((abs‘(𝑤 − 𝑥)) < 𝑧 ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))
215	214	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ (abs‘(𝑤 − 𝑥)) < 𝑧) → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))
216	74	ad6antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 ∈ ℝ)
217		rge0ssre 12151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0[,)+∞) ⊆ ℝ
218	4	ad4antr 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
219	218	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ (0[,)+∞))
220	217, 219	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ ℝ)
221	220	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝐹‘𝑤) ∈ ℝ)
222	4	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
223	222	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
224	217, 223	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
225	79, 224	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑥) ∈ ℝ)
226	225	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
227	220, 226	resubcld 10337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑤) − (𝐹‘𝑥)) ∈ ℝ)
228	74	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
229	225, 228	resubcld 10337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹‘𝑥) − 𝑦) ∈ ℝ)
230	229	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑥) − 𝑦) ∈ ℝ)
231	227, 230	absltd 14016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦) ↔ (-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦))))
232	225	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑥) ∈ ℂ)
233		rpcn 11717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
234	233	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
235	232, 234	negsubdi2d 10287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → -((𝐹‘𝑥) − 𝑦) = (𝑦 − (𝐹‘𝑥)))
236	235	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → -((𝐹‘𝑥) − 𝑦) = (𝑦 − (𝐹‘𝑥)))
237	236	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ↔ (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥))))
238	237	anbi1d 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)) ↔ ((𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦))))
239	231, 238	bitrd 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦) ↔ ((𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦))))
240	239	simprbda 651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)))
241	225	ad4antr 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝐹‘𝑥) ∈ ℝ)
242	216, 221, 241	ltsub1d 10515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝑦 < (𝐹‘𝑤) ↔ (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥))))
243	240, 242	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 < (𝐹‘𝑤))
244	216, 221, 243	ltled 10064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 ≤ (𝐹‘𝑤))
245	215, 244	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧ (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹‘𝑤))
246	245	an4s 865	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹‘𝑤))
247	213, 246	syldan 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ (𝐹‘𝑤))
248	247	iftrued 4044	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) = 𝑦)
249	185, 248	breqtrrd 4611	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
250		0le0 10987	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ≤ 0
251		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) → (0 ≤ 𝑦 ↔ 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)))
252		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)))
253	251, 252	ifboth 4074	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 ≤ 𝑦 ∧ 0 ≤ 0) → 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
254	162, 250, 253	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℝ+ → 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
255	254	ad6antlr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ ¬ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
256	182, 183, 249, 255	ifbothda 4073	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
257	181, 256	sylan2 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌))) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
258	257	anassrs 678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
259		iftrue 4042	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
260	259	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0))
261		iftrue 4042	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
262	261	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))
263	258, 260, 262	3brtr4d 4615	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0))
264	263	ex 449	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)))
265	250	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑤 ∈ (𝑋(,)𝑌) → 0 ≤ 0)
266		iffalse 4045	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = 0)
267		iffalse 4045	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = 0)
268	265, 266, 267	3brtr4d 4615	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0))
269	264, 268	pm2.61d1 170	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0))
270		elin 3758	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))))
271		ifbi 4057	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))
272	270, 271	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)
273		ifan 4084	. . . . . . . . . . . . . . . . . 18 ⊢ if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
274	272, 273	eqtri 2632	. . . . . . . . . . . . . . . . 17 ⊢ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0)
275		fveq2 6103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑤 → (𝐹‘𝑣) = (𝐹‘𝑤))
276	275	breq2d 4595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑤 → (𝑦 ≤ (𝐹‘𝑣) ↔ 𝑦 ≤ (𝐹‘𝑤)))
277	276	elrab 3331	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)))
278		ifbi 4057	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤))) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0))
279	277, 278	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0)
280		ifan 4084	. . . . . . . . . . . . . . . . . 18 ⊢ if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)
281	279, 280	eqtri 2632	. . . . . . . . . . . . . . . . 17 ⊢ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)
282	269, 274, 281	3brtr4g 4617	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))
283	282	ralrimivw 2950	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))
284		reex 9906	. . . . . . . . . . . . . . . . 17 ⊢ ℝ ∈ V
285	284	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ℝ ∈ V)
286	59	ad6antlr 769	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞))
287	67	ad6antlr 769	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
288		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))
289		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))
290	285, 286, 287, 288, 289	ofrfval2 6813	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))
291	283, 290	mpbird 246	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))
292		itg2le 23312	. . . . . . . . . . . . . 14 ⊢ (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))
293	171, 172, 291, 292	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))
294	52, 65, 73, 170, 293	xrltletrd 11868	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))
295		itg2gt0cn.cn	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
296	295	ad3antrrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
297		simplr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 𝑥 ∈ (𝑋(,)𝑌))
298		fssres 5983	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (𝑋(,)𝑌) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
299	29, 298	mpan2 703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹:ℝ⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞))
300		fss 5969	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
301	217, 300	mpan2 703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
302	4, 299, 301	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
303	302	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ)
304	303	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ∈ ℝ)
305	304, 228	resubcld 10337	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
306	305	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ)
307	228, 304	posdifd 10493	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
308	307	biimpa 500	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))
309	306, 308	elrpd 11745	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+)
310		cncfi 22505	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ 𝑥 ∈ (𝑋(,)𝑌) ∧ (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
311	296, 297, 309, 310	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))
312	311	ex 449	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))))
313		fvres 6117	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹‘𝑥))
314	313	breq2d 4595	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹‘𝑥)))
315	314	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹‘𝑥)))
316		fvres 6117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹‘𝑢))
317	316	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹‘𝑢))
318	313	ad2antlr 759	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹‘𝑥))
319	317, 318	oveq12d 6567	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) = ((𝐹‘𝑢) − (𝐹‘𝑥)))
320	319	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))))
321	313	oveq1d 6564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹‘𝑥) − 𝑦))
322	321	ad2antlr 759	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹‘𝑥) − 𝑦))
323	320, 322	breq12d 4596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ↔ (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))
324	323	imbi2d 329	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))))
325	324	ralbidva 2968	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))))
326	325	rexbidv 3034	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))))
327	312, 315, 326	3imtr3d 281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹‘𝑥) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))))
328	327	imp 444	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))
329	294, 328	r19.29a 3060	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))
330	329	ex 449	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹‘𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))))
331	330	rexlimdva 3013	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))))
332	51, 331	sylbid 229	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))))
333	332	imp 444	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))
334	70	ad2antlr 759	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞))
335		icossicc 12131	. . . . . . . . . 10 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
336		fss 5969	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
337	4, 335, 336	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))
338	337	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹:ℝ⟶(0[,]+∞))
339		breq1 4586	. . . . . . . . . . . 12 ⊢ (𝑦 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) → (𝑦 ≤ (𝐹‘𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)))
340		breq1 4586	. . . . . . . . . . . 12 ⊢ (0 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) → (0 ≤ (𝐹‘𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)))
341	277	simprbi 479	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} → 𝑦 ≤ (𝐹‘𝑤))
342	341	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}) → 𝑦 ≤ (𝐹‘𝑤))
343	4	ffvelrnda 6267	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ (0[,)+∞))
344		elrege0 12149	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑤) ∈ (0[,)+∞) ↔ ((𝐹‘𝑤) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑤)))
345	343, 344	sylib 207	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑤) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑤)))
346	345	simprd 478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → 0 ≤ (𝐹‘𝑤))
347	346	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ¬ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}) → 0 ≤ (𝐹‘𝑤))
348	339, 340, 342, 347	ifbothda 4073	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))
349	348	ralrimiva 2949	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))
350	349	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))
351	284	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ℝ ∈ V)
352	67	ad3antlr 763	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞))
353		fvex 6113	. . . . . . . . . . 11 ⊢ (𝐹‘𝑤) ∈ V
354	353	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ V)
355		eqidd 2611	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))
356	4	feqmptd 6159	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹‘𝑤)))
357	356	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹‘𝑤)))
358	351, 352, 354, 355, 357	ofrfval2 6813	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)))
359	350, 358	mpbird 246	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘𝑟 ≤ 𝐹)
360		itg2le 23312	. . . . . . . 8 ⊢ (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘𝑟 ≤ 𝐹) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹))
361	334, 338, 359, 360	syl3anc 1318	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹))
362	43, 333, 361	jca32 556	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹))))
363	362	expl 646	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ ℝ+ ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)))))
364	42, 363	syl5 33	. . . 4 ⊢ (𝜑 → ((𝑦 ∈ ℚ ∧ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) → (𝑦 ∈ ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)))))
365	364	reximdv2 2997	. . 3 ⊢ (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → ∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹))))
366	1	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 0 ∈ ℝ*)
367	72	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈ ℝ*)
368		itg2cl 23305	. . . . . . 7 ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
369	337, 368	syl 17	. . . . . 6 ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ*)
370	369	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∫2‘𝐹) ∈ ℝ*)
371		xrltletr 11864	. . . . 5 ⊢ ((0 ∈ ℝ* ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈ ℝ* ∧ (∫2‘𝐹) ∈ ℝ*) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 < (∫2‘𝐹)))
372	366, 367, 370, 371	syl3anc 1318	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 < (∫2‘𝐹)))
373	372	rexlimdva 3013	. . 3 ⊢ (𝜑 → (∃𝑦 ∈ ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 < (∫2‘𝐹)))
374	365, 373	syld 46	. 2 ⊢ (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0 < (∫2‘𝐹)))
375	36, 374	mpd 15	1 ⊢ (𝜑 → 0 < (∫2‘𝐹))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘_𝑟 cofr 6794  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815   + caddc 9818   · cmul 9820  +∞cpnf 9950  -∞cmnf 9951  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146  ℚcq 11664  ℝ⁺crp 11708  (,)cioo 12046  [,)cico 12048  [,]cicc 12049  abscabs 13822  –cn→ccncf 22487  vol*covol 23038  volcvol 23039  ∫₂citg2 23191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-cncf 22489  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195  df-itg2 23196  df-0p 23243

This theorem is referenced by:  itggt0cn  32652