itg2gt0cn

Description: itg2gt0 holds on functions continuous on an open interval in the absence of ax-cc . The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017)

	Ref	Expression
Hypotheses	itg2gt0cn.2	$⊢ φ \to X < Y$
	itg2gt0cn.3	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2gt0cn.5	$⊢ (φ \land x \in (X, Y)) \to 0 < F (x)$
	itg2gt0cn.cn	$⊢ φ \to ({F ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ$
Assertion	itg2gt0cn	$⊢ φ \to 0 < \int^{2} (F)$

Proof

Step	Hyp	Ref	Expression
1		itg2gt0cn.2	$⊢ φ \to X < Y$
2		itg2gt0cn.3	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		itg2gt0cn.5	$⊢ (φ \land x \in (X, Y)) \to 0 < F (x)$
4		itg2gt0cn.cn	$⊢ φ \to ({F ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ$
5		0xr	$⊢ 0 \in ℝ^{*}$
6		imassrn	$⊢ F [(X, Y)] \subseteq ran F$
7	2	frnd	$⊢ φ \to ran F \subseteq [0, +∞)$
8		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
9	7 8	sstrdi	$⊢ φ \to ran F \subseteq ℝ^{*}$
10	6 9	sstrid	$⊢ φ \to F [(X, Y)] \subseteq ℝ^{*}$
11		supxrcl	$⊢ F [(X, Y)] \subseteq ℝ^{} \to sup (F [(X, Y)] ℝ^{} <) \in ℝ^{*}$
12	10 11	syl	$⊢ φ \to sup (F [(X, Y)] ℝ^{} <) \in ℝ^{}$
13		ltrelxr	$⊢ < \subseteq ℝ^{} \times ℝ^{}$
14	13	ssbri	$⊢ X < Y \to X (ℝ^{} \times ℝ^{}) Y$
15	1 14	syl	$⊢ φ \to X (ℝ^{} \times ℝ^{}) Y$
16		brxp	$⊢ X (ℝ^{} \times ℝ^{}) Y \leftrightarrow (X \in ℝ^{} \land Y \in ℝ^{})$
17	15 16	sylib	$⊢ φ \to (X \in ℝ^{} \land Y \in ℝ^{})$
18		ioon0	$⊢ (X \in ℝ^{} \land Y \in ℝ^{}) \to ((X, Y) \neq \emptyset \leftrightarrow X < Y)$
19	17 18	syl	$⊢ φ \to ((X, Y) \neq \emptyset \leftrightarrow X < Y)$
20	1 19	mpbird	$⊢ φ \to (X, Y) \neq \emptyset$
21	3	ralrimiva	$⊢ φ \to \forall x \in (X, Y) 0 < F (x)$
22		r19.2z	$⊢ ((X, Y) \neq \emptyset \land \forall x \in (X, Y) 0 < F (x)) \to \exists x \in (X, Y) 0 < F (x)$
23	20 21 22	syl2anc	$⊢ φ \to \exists x \in (X, Y) 0 < F (x)$
24		supxrlub	$⊢ (F [(X, Y)] \subseteq ℝ^{} \land 0 \in ℝ^{}) \to (0 < sup (F [(X, Y)] ℝ^{*} <) \leftrightarrow \exists y \in F [(X, Y)] 0 < y)$
25	10 5 24	sylancl	$⊢ φ \to (0 < sup (F [(X, Y)] ℝ^{*} <) \leftrightarrow \exists y \in F [(X, Y)] 0 < y)$
26	2	ffnd	$⊢ φ \to F Fn ℝ$
27		ioossre	$⊢ (X, Y) \subseteq ℝ$
28		breq2	$⊢ y = F (x) \to (0 < y \leftrightarrow 0 < F (x))$
29	28	rexima	$⊢ (F Fn ℝ \land (X, Y) \subseteq ℝ) \to (\exists y \in F [(X, Y)] 0 < y \leftrightarrow \exists x \in (X, Y) 0 < F (x))$
30	26 27 29	sylancl	$⊢ φ \to (\exists y \in F [(X, Y)] 0 < y \leftrightarrow \exists x \in (X, Y) 0 < F (x))$
31	25 30	bitrd	$⊢ φ \to (0 < sup (F [(X, Y)] ℝ^{*} <) \leftrightarrow \exists x \in (X, Y) 0 < F (x))$
32	23 31	mpbird	$⊢ φ \to 0 < sup (F [(X, Y)] ℝ^{*} <)$
33		qbtwnxr	$⊢ (0 \in ℝ^{} \land sup (F [(X, Y)] ℝ^{} <) \in ℝ^{} \land 0 < sup (F [(X, Y)] ℝ^{} <)) \to \exists y \in ℚ (0 < y \land y < sup (F [(X, Y)] ℝ^{*} <))$
34	5 12 32 33	mp3an2i	$⊢ φ \to \exists y \in ℚ (0 < y \land y < sup (F [(X, Y)] ℝ^{*} <))$
35		qre	$⊢ y \in ℚ \to y \in ℝ$
36	35	adantr	$⊢ (y \in ℚ \land 0 < y) \to y \in ℝ$
37		simpr	$⊢ (y \in ℚ \land 0 < y) \to 0 < y$
38	36 37	elrpd	$⊢ (y \in ℚ \land 0 < y) \to y \in ℝ^{+}$
39	38	anim1i	$⊢ ((y \in ℚ \land 0 < y) \land y < sup (F [(X, Y)] ℝ^{} <)) \to (y \in ℝ^{+} \land y < sup (F [(X, Y)] ℝ^{} <))$
40	39	anasss	$⊢ (y \in ℚ \land (0 < y \land y < sup (F [(X, Y)] ℝ^{} <))) \to (y \in ℝ^{+} \land y < sup (F [(X, Y)] ℝ^{} <))$
41		simplr	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to y \in ℝ^{+}$
42		rpxr	$⊢ y \in ℝ^{+} \to y \in ℝ^{*}$
43		supxrlub	$⊢ (F [(X, Y)] \subseteq ℝ^{} \land y \in ℝ^{}) \to (y < sup (F [(X, Y)] ℝ^{*} <) \leftrightarrow \exists z \in F [(X, Y)] y < z)$
44	10 42 43	syl2an	$⊢ (φ \land y \in ℝ^{+}) \to (y < sup (F [(X, Y)] ℝ^{*} <) \leftrightarrow \exists z \in F [(X, Y)] y < z)$
45		breq2	$⊢ z = F (x) \to (y < z \leftrightarrow y < F (x))$
46	45	rexima	$⊢ (F Fn ℝ \land (X, Y) \subseteq ℝ) \to (\exists z \in F [(X, Y)] y < z \leftrightarrow \exists x \in (X, Y) y < F (x))$
47	26 27 46	sylancl	$⊢ φ \to (\exists z \in F [(X, Y)] y < z \leftrightarrow \exists x \in (X, Y) y < F (x))$
48	47	adantr	$⊢ (φ \land y \in ℝ^{+}) \to (\exists z \in F [(X, Y)] y < z \leftrightarrow \exists x \in (X, Y) y < F (x))$
49	44 48	bitrd	$⊢ (φ \land y \in ℝ^{+}) \to (y < sup (F [(X, Y)] ℝ^{*} <) \leftrightarrow \exists x \in (X, Y) y < F (x))$
50	5	a1i	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to 0 \in ℝ^{*}$
51		ioorp	$⊢ (0, +∞) = ℝ^{+}$
52		ioossicc	$⊢ (0, +∞) \subseteq [0, +∞]$
53	51 52	eqsstrri	$⊢ ℝ^{+} \subseteq [0, +∞]$
54	53	sseli	$⊢ y \in ℝ^{+} \to y \in [0, +∞]$
55		0e0iccpnf	$⊢ 0 \in [0, +∞]$
56		ifcl	$⊢ (y \in [0, +∞] \land 0 \in [0, +∞]) \to if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) \in [0, +∞]$
57	54 55 56	sylancl	$⊢ y \in ℝ^{+} \to if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) \in [0, +∞]$
58	57	adantr	$⊢ (y \in ℝ^{+} \land w \in ℝ) \to if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) \in [0, +∞]$
59	58	fmpttd	$⊢ y \in ℝ^{+} \to (w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) : ℝ ⟶ [0, +∞]$
60		itg2cl	$⊢ (w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) : ℝ ⟶ [0, +∞] \to \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0))) \in ℝ^{*}$
61	59 60	syl	$⊢ y \in ℝ^{+} \to \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0))) \in ℝ^{*}$
62	61	ad5antlr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0))) \in ℝ^{*}$
63		ifcl	$⊢ (y \in [0, +∞] \land 0 \in [0, +∞]) \to if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \in [0, +∞]$
64	54 55 63	sylancl	$⊢ y \in ℝ^{+} \to if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \in [0, +∞]$
65	64	adantr	$⊢ (y \in ℝ^{+} \land w \in ℝ) \to if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \in [0, +∞]$
66	65	fmpttd	$⊢ y \in ℝ^{+} \to (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) : ℝ ⟶ [0, +∞]$
67		itg2cl	$⊢ (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) : ℝ ⟶ [0, +∞] \to \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \in ℝ^{*}$
68	66 67	syl	$⊢ y \in ℝ^{+} \to \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \in ℝ^{*}$
69	68	ad5antlr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \in ℝ^{*}$
70		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
71	70	ad4antlr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to y \in ℝ$
72		ioombl	$⊢ (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)) \in dom vol$
73		mblvol	$⊢ (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)) \in dom vol \to vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))) = {vol}^{*} ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)))$
74	72 73	ax-mp	$⊢ vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))) = {vol}^{*} ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)))$
75		elioore	$⊢ x \in (X, Y) \to x \in ℝ$
76	75	ad3antlr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x \in ℝ$
77		rpre	$⊢ z \in ℝ^{+} \to z \in ℝ$
78	77	adantl	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to z \in ℝ$
79	76 78	resubcld	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x - z \in ℝ$
80	79	adantr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land X \leq x - z) \to x - z \in ℝ$
81	79	rexrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x - z \in ℝ^{*}$
82	81	adantr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \neg X \leq x - z) \to x - z \in ℝ^{*}$
83	17	simpld	$⊢ φ \to X \in ℝ^{*}$
84	83	ad5antr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \neg X \leq x - z) \to X \in ℝ^{*}$
85	17	simprd	$⊢ φ \to Y \in ℝ^{*}$
86	85	ad5antr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \neg X \leq x - z) \to Y \in ℝ^{*}$
87	83	ad4antr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to X \in ℝ^{*}$
88		xrltnle	$⊢ (x - z \in ℝ^{} \land X \in ℝ^{}) \to (x - z < X \leftrightarrow \neg X \leq x - z)$
89	81 87 88	syl2anc	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to (x - z < X \leftrightarrow \neg X \leq x - z)$
90	89	biimpar	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \neg X \leq x - z) \to x - z < X$
91	1	ad5antr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \neg X \leq x - z) \to X < Y$
92		xrre2	$⊢ ((x - z \in ℝ^{} \land X \in ℝ^{} \land Y \in ℝ^{*}) \land (x - z < X \land X < Y)) \to X \in ℝ$
93	82 84 86 90 91 92	syl32anc	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \neg X \leq x - z) \to X \in ℝ$
94	80 93	ifclda	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to if (X \leq x - z, x - z, X) \in ℝ$
95	85	ad5antr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land Y \leq z + x) \to Y \in ℝ^{*}$
96	78 76	readdcld	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to z + x \in ℝ$
97	96	adantr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land Y \leq z + x) \to z + x \in ℝ$
98		mnfxr	$⊢ −∞ \in ℝ^{*}$
99	98	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
100		mnfle	$⊢ X \in ℝ^{*} \to −∞ \leq X$
101	83 100	syl	$⊢ φ \to −∞ \leq X$
102	99 83 85 101 1	xrlelttrd	$⊢ φ \to −∞ < Y$
103	102	ad5antr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land Y \leq z + x) \to −∞ < Y$
104		simpr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land Y \leq z + x) \to Y \leq z + x$
105		xrre	$⊢ ((Y \in ℝ^{*} \land z + x \in ℝ) \land (−∞ < Y \land Y \leq z + x)) \to Y \in ℝ$
106	95 97 103 104 105	syl22anc	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land Y \leq z + x) \to Y \in ℝ$
107	96	adantr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \neg Y \leq z + x) \to z + x \in ℝ$
108	106 107	ifclda	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to if (Y \leq z + x, Y, z + x) \in ℝ$
109	76	rexrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x \in ℝ^{*}$
110	85	ad4antr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to Y \in ℝ^{*}$
111		rpgt0	$⊢ z \in ℝ^{+} \to 0 < z$
112	111	adantl	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to 0 < z$
113	78 76	ltsubposd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to (0 < z \leftrightarrow x - z < x)$
114	112 113	mpbid	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x - z < x$
115		eliooord	$⊢ x \in (X, Y) \to (X < x \land x < Y)$
116	115	simprd	$⊢ x \in (X, Y) \to x < Y$
117	116	ad3antlr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x < Y$
118	81 109 110 114 117	xrlttrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x - z < Y$
119	78 76	ltaddpos2d	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to (0 < z \leftrightarrow x < z + x)$
120	112 119	mpbid	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x < z + x$
121	79 76 96 114 120	lttrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x - z < z + x$
122		breq2	$⊢ Y = if (Y \leq z + x, Y, z + x) \to (x - z < Y \leftrightarrow x - z < if (Y \leq z + x, Y, z + x))$
123		breq2	$⊢ z + x = if (Y \leq z + x, Y, z + x) \to (x - z < z + x \leftrightarrow x - z < if (Y \leq z + x, Y, z + x))$
124	122 123	ifboth	$⊢ (x - z < Y \land x - z < z + x) \to x - z < if (Y \leq z + x, Y, z + x)$
125	118 121 124	syl2anc	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to x - z < if (Y \leq z + x, Y, z + x)$
126	1	ad4antr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to X < Y$
127	96	rexrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to z + x \in ℝ^{*}$
128	115	simpld	$⊢ x \in (X, Y) \to X < x$
129	128	ad3antlr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to X < x$
130	87 109 127 129 120	xrlttrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to X < z + x$
131		breq2	$⊢ Y = if (Y \leq z + x, Y, z + x) \to (X < Y \leftrightarrow X < if (Y \leq z + x, Y, z + x))$
132		breq2	$⊢ z + x = if (Y \leq z + x, Y, z + x) \to (X < z + x \leftrightarrow X < if (Y \leq z + x, Y, z + x))$
133	131 132	ifboth	$⊢ (X < Y \land X < z + x) \to X < if (Y \leq z + x, Y, z + x)$
134	126 130 133	syl2anc	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to X < if (Y \leq z + x, Y, z + x)$
135		breq1	$⊢ x - z = if (X \leq x - z, x - z, X) \to (x - z < if (Y \leq z + x, Y, z + x) \leftrightarrow if (X \leq x - z, x - z, X) < if (Y \leq z + x, Y, z + x))$
136		breq1	$⊢ X = if (X \leq x - z, x - z, X) \to (X < if (Y \leq z + x, Y, z + x) \leftrightarrow if (X \leq x - z, x - z, X) < if (Y \leq z + x, Y, z + x))$
137	135 136	ifboth	$⊢ (x - z < if (Y \leq z + x, Y, z + x) \land X < if (Y \leq z + x, Y, z + x)) \to if (X \leq x - z, x - z, X) < if (Y \leq z + x, Y, z + x)$
138	125 134 137	syl2anc	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to if (X \leq x - z, x - z, X) < if (Y \leq z + x, Y, z + x)$
139	94 108 138	ltled	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to if (X \leq x - z, x - z, X) \leq if (Y \leq z + x, Y, z + x)$
140		ovolioo	$⊢ (if (X \leq x - z, x - z, X) \in ℝ \land if (Y \leq z + x, Y, z + x) \in ℝ \land if (X \leq x - z, x - z, X) \leq if (Y \leq z + x, Y, z + x)) \to {vol}^{*} ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))) = if (Y \leq z + x, Y, z + x) - if (X \leq x - z, x - z, X)$
141	94 108 139 140	syl3anc	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to {vol}^{*} ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))) = if (Y \leq z + x, Y, z + x) - if (X \leq x - z, x - z, X)$
142	74 141	eqtrid	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))) = if (Y \leq z + x, Y, z + x) - if (X \leq x - z, x - z, X)$
143	108 94	resubcld	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to if (Y \leq z + x, Y, z + x) - if (X \leq x - z, x - z, X) \in ℝ$
144	142 143	eqeltrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))) \in ℝ$
145		rpgt0	$⊢ y \in ℝ^{+} \to 0 < y$
146	145	ad4antlr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to 0 < y$
147	94 108	posdifd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to (if (X \leq x - z, x - z, X) < if (Y \leq z + x, Y, z + x) \leftrightarrow 0 < if (Y \leq z + x, Y, z + x) - if (X \leq x - z, x - z, X))$
148	138 147	mpbid	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to 0 < if (Y \leq z + x, Y, z + x) - if (X \leq x - z, x - z, X)$
149	148 142	breqtrrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to 0 < vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)))$
150	71 144 146 149	mulgt0d	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to 0 < y vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)))$
151		iooin	$⊢ ((X \in ℝ^{} \land Y \in ℝ^{}) \land (x - z \in ℝ^{} \land z + x \in ℝ^{})) \to (X, Y) \cap (x - z, z + x) = (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))$
152	87 110 81 127 151	syl22anc	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to (X, Y) \cap (x - z, z + x) = (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))$
153	152	eleq2d	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to (w \in ((X, Y) \cap (x - z, z + x)) \leftrightarrow w \in (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)))$
154	153	ifbid	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) = if (w \in (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)), y, 0)$
155	154	mpteq2dv	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to (w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) = (w \in ℝ ⟼ if (w \in (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)), y, 0))$
156	155	fveq2d	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0))) = \int^{2} ((w \in ℝ ⟼ if (w \in (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)), y, 0)))$
157		rpge0	$⊢ y \in ℝ^{+} \to 0 \leq y$
158		elrege0	$⊢ y \in [0, +∞) \leftrightarrow (y \in ℝ \land 0 \leq y)$
159	70 157 158	sylanbrc	$⊢ y \in ℝ^{+} \to y \in [0, +∞)$
160	159	ad4antlr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to y \in [0, +∞)$
161		itg2const	$⊢ ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)) \in dom vol \land vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x))) \in ℝ \land y \in [0, +∞)) \to \int^{2} ((w \in ℝ ⟼ if (w \in (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)), y, 0))) = y vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)))$
162	72 144 160 161	mp3an2i	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to \int^{2} ((w \in ℝ ⟼ if (w \in (if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)), y, 0))) = y vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)))$
163	156 162	eqtrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0))) = y vol ((if (X \leq x - z, x - z, X), if (Y \leq z + x, Y, z + x)))$
164	150 163	breqtrrd	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to 0 < \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)))$
165	164	adantr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to 0 < \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)))$
166	59	ad5antlr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to (w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) : ℝ ⟶ [0, +∞]$
167	66	ad5antlr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) : ℝ ⟶ [0, +∞]$
168		fvoveq1	$⊢ u = w \to \|u - x\| = \|w - x\|$
169	168	breq1d	$⊢ u = w \to (\|u - x\| < z \leftrightarrow \|w - x\| < z)$
170	169	imbrov2fvoveq	$⊢ u = w \to ((\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y) \leftrightarrow (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y))$
171	170	rspccva	$⊢ (\forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y) \land w \in (X, Y)) \to (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)$
172		breq1	$⊢ y = if (w \in (x - z, z + x), y, 0) \to (y \leq if (y \leq F (w), y, 0) \leftrightarrow if (w \in (x - z, z + x), y, 0) \leq if (y \leq F (w), y, 0))$
173		breq1	$⊢ 0 = if (w \in (x - z, z + x), y, 0) \to (0 \leq if (y \leq F (w), y, 0) \leftrightarrow if (w \in (x - z, z + x), y, 0) \leq if (y \leq F (w), y, 0))$
174	70	leidd	$⊢ y \in ℝ^{+} \to y \leq y$
175	174	ad6antlr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in (x - z, z + x)) \to y \leq y$
176	75	ad4antlr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to x \in ℝ$
177	77	ad2antlr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to z \in ℝ$
178	176 177	resubcld	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to x - z \in ℝ$
179	178	rexrd	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to x - z \in ℝ^{*}$
180	177 176	readdcld	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to z + x \in ℝ$
181	180	rexrd	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to z + x \in ℝ^{*}$
182		elioo2	$⊢ (x - z \in ℝ^{} \land z + x \in ℝ^{}) \to (w \in (x - z, z + x) \leftrightarrow (w \in ℝ \land x - z < w \land w < z + x))$
183	179 181 182	syl2anc	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to (w \in (x - z, z + x) \leftrightarrow (w \in ℝ \land x - z < w \land w < z + x))$
184		3anass	$⊢ (w \in ℝ \land x - z < w \land w < z + x) \leftrightarrow (w \in ℝ \land (x - z < w \land w < z + x))$
185	183 184	bitrdi	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to (w \in (x - z, z + x) \leftrightarrow (w \in ℝ \land (x - z < w \land w < z + x)))$
186		simpr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to w \in ℝ$
187	75	ad5antlr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to x \in ℝ$
188	186 187	resubcld	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to w - x \in ℝ$
189	77	ad3antlr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to z \in ℝ$
190	188 189	absltd	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to (\|w - x\| < z \leftrightarrow (- z < w - x \land w - x < z))$
191	189	renegcld	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to - z \in ℝ$
192	187 191 186	ltaddsub2d	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to (x + (- z) < w \leftrightarrow - z < w - x)$
193	187	recnd	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to x \in ℂ$
194	189	recnd	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to z \in ℂ$
195	193 194	negsubd	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to x + (- z) = x - z$
196	195	breq1d	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to (x + (- z) < w \leftrightarrow x - z < w)$
197	192 196	bitr3d	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to (- z < w - x \leftrightarrow x - z < w)$
198	186 187 189	ltsubaddd	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to (w - x < z \leftrightarrow w < z + x)$
199	197 198	anbi12d	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to ((- z < w - x \land w - x < z) \leftrightarrow (x - z < w \land w < z + x))$
200	190 199	bitrd	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in ℝ) \to (\|w - x\| < z \leftrightarrow (x - z < w \land w < z + x))$
201	200	pm5.32da	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to ((w \in ℝ \land \|w - x\| < z) \leftrightarrow (w \in ℝ \land (x - z < w \land w < z + x)))$
202	185 201	bitr4d	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to (w \in (x - z, z + x) \leftrightarrow (w \in ℝ \land \|w - x\| < z))$
203	202	biimpa	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in (x - z, z + x)) \to (w \in ℝ \land \|w - x\| < z)$
204		pm3.35	$⊢ (\|w - x\| < z \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to \|F (w) - F (x)\| < F (x) - y$
205	204	ancoms	$⊢ ((\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y) \land \|w - x\| < z) \to \|F (w) - F (x)\| < F (x) - y$
206	70	ad6antlr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \land \|F (w) - F (x)\| < F (x) - y) \to y \in ℝ$
207		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
208	2	ad4antr	$⊢ ((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \to F : ℝ ⟶ [0, +∞)$
209	208	ffvelcdmda	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to F (w) \in [0, +∞)$
210	207 209	sselid	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to F (w) \in ℝ$
211	210	adantr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \land \|F (w) - F (x)\| < F (x) - y) \to F (w) \in ℝ$
212	2	adantr	$⊢ (φ \land y \in ℝ^{+}) \to F : ℝ ⟶ [0, +∞)$
213	212	ffvelcdmda	$⊢ ((φ \land y \in ℝ^{+}) \land x \in ℝ) \to F (x) \in [0, +∞)$
214	207 213	sselid	$⊢ ((φ \land y \in ℝ^{+}) \land x \in ℝ) \to F (x) \in ℝ$
215	75 214	sylan2	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to F (x) \in ℝ$
216	215	ad3antrrr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to F (x) \in ℝ$
217	210 216	resubcld	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to F (w) - F (x) \in ℝ$
218	70	ad2antlr	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to y \in ℝ$
219	215 218	resubcld	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to F (x) - y \in ℝ$
220	219	ad3antrrr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to F (x) - y \in ℝ$
221	217 220	absltd	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to (\|F (w) - F (x)\| < F (x) - y \leftrightarrow (- (F (x) - y) < F (w) - F (x) \land F (w) - F (x) < F (x) - y))$
222	215	recnd	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to F (x) \in ℂ$
223		rpcn	$⊢ y \in ℝ^{+} \to y \in ℂ$
224	223	ad2antlr	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to y \in ℂ$
225	222 224	negsubdi2d	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to - (F (x) - y) = y - F (x)$
226	225	ad3antrrr	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to - (F (x) - y) = y - F (x)$
227	226	breq1d	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to (- (F (x) - y) < F (w) - F (x) \leftrightarrow y - F (x) < F (w) - F (x))$
228	227	anbi1d	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to ((- (F (x) - y) < F (w) - F (x) \land F (w) - F (x) < F (x) - y) \leftrightarrow (y - F (x) < F (w) - F (x) \land F (w) - F (x) < F (x) - y))$
229	221 228	bitrd	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \to (\|F (w) - F (x)\| < F (x) - y \leftrightarrow (y - F (x) < F (w) - F (x) \land F (w) - F (x) < F (x) - y))$
230	229	simprbda	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \land \|F (w) - F (x)\| < F (x) - y) \to y - F (x) < F (w) - F (x)$
231	215	ad4antr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \land \|F (w) - F (x)\| < F (x) - y) \to F (x) \in ℝ$
232	206 211 231	ltsub1d	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \land \|F (w) - F (x)\| < F (x) - y) \to (y < F (w) \leftrightarrow y - F (x) < F (w) - F (x))$
233	230 232	mpbird	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \land \|F (w) - F (x)\| < F (x) - y) \to y < F (w)$
234	206 211 233	ltled	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \land \|F (w) - F (x)\| < F (x) - y) \to y \leq F (w)$
235	205 234	sylan2	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land w \in ℝ) \land ((\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y) \land \|w - x\| < z)) \to y \leq F (w)$
236	235	an4s	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land (w \in ℝ \land \|w - x\| < z)) \to y \leq F (w)$
237	203 236	syldan	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in (x - z, z + x)) \to y \leq F (w)$
238	237	iftrued	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in (x - z, z + x)) \to if (y \leq F (w), y, 0) = y$
239	175 238	breqtrrd	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land w \in (x - z, z + x)) \to y \leq if (y \leq F (w), y, 0)$
240		0le0	$⊢ 0 \leq 0$
241		breq2	$⊢ y = if (y \leq F (w), y, 0) \to (0 \leq y \leftrightarrow 0 \leq if (y \leq F (w), y, 0))$
242		breq2	$⊢ 0 = if (y \leq F (w), y, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (y \leq F (w), y, 0))$
243	241 242	ifboth	$⊢ (0 \leq y \land 0 \leq 0) \to 0 \leq if (y \leq F (w), y, 0)$
244	157 240 243	sylancl	$⊢ y \in ℝ^{+} \to 0 \leq if (y \leq F (w), y, 0)$
245	244	ad6antlr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \land \neg w \in (x - z, z + x)) \to 0 \leq if (y \leq F (w), y, 0)$
246	172 173 239 245	ifbothda	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\|w - x\| < z \to \|F (w) - F (x)\| < F (x) - y)) \to if (w \in (x - z, z + x), y, 0) \leq if (y \leq F (w), y, 0)$
247	171 246	sylan2	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land (\forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y) \land w \in (X, Y))) \to if (w \in (x - z, z + x), y, 0) \leq if (y \leq F (w), y, 0)$
248	247	anassrs	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \land w \in (X, Y)) \to if (w \in (x - z, z + x), y, 0) \leq if (y \leq F (w), y, 0)$
249		iftrue	$⊢ w \in (X, Y) \to if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0) = if (w \in (x - z, z + x), y, 0)$
250	249	adantl	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \land w \in (X, Y)) \to if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0) = if (w \in (x - z, z + x), y, 0)$
251		iftrue	$⊢ w \in (X, Y) \to if (w \in (X, Y), if (y \leq F (w), y, 0), 0) = if (y \leq F (w), y, 0)$
252	251	adantl	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \land w \in (X, Y)) \to if (w \in (X, Y), if (y \leq F (w), y, 0), 0) = if (y \leq F (w), y, 0)$
253	248 250 252	3brtr4d	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \land w \in (X, Y)) \to if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0) \leq if (w \in (X, Y), if (y \leq F (w), y, 0), 0)$
254	253	ex	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to (w \in (X, Y) \to if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0) \leq if (w \in (X, Y), if (y \leq F (w), y, 0), 0))$
255	240	a1i	$⊢ \neg w \in (X, Y) \to 0 \leq 0$
256		iffalse	$⊢ \neg w \in (X, Y) \to if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0) = 0$
257		iffalse	$⊢ \neg w \in (X, Y) \to if (w \in (X, Y), if (y \leq F (w), y, 0), 0) = 0$
258	255 256 257	3brtr4d	$⊢ \neg w \in (X, Y) \to if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0) \leq if (w \in (X, Y), if (y \leq F (w), y, 0), 0)$
259	254 258	pm2.61d1	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0) \leq if (w \in (X, Y), if (y \leq F (w), y, 0), 0)$
260		elin	$⊢ w \in ((X, Y) \cap (x - z, z + x)) \leftrightarrow (w \in (X, Y) \land w \in (x - z, z + x))$
261		ifbi	$⊢ (w \in ((X, Y) \cap (x - z, z + x)) \leftrightarrow (w \in (X, Y) \land w \in (x - z, z + x))) \to if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) = if ((w \in (X, Y) \land w \in (x - z, z + x)), y, 0)$
262	260 261	ax-mp	$⊢ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) = if ((w \in (X, Y) \land w \in (x - z, z + x)), y, 0)$
263		ifan	$⊢ if ((w \in (X, Y) \land w \in (x - z, z + x)), y, 0) = if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0)$
264	262 263	eqtri	$⊢ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) = if (w \in (X, Y), if (w \in (x - z, z + x), y, 0), 0)$
265		fveq2	$⊢ v = w \to F (v) = F (w)$
266	265	breq2d	$⊢ v = w \to (y \leq F (v) \leftrightarrow y \leq F (w))$
267	266	elrab	$⊢ w \in \{v \in (X, Y) \| y \leq F (v)\} \leftrightarrow (w \in (X, Y) \land y \leq F (w))$
268		ifbi	$⊢ (w \in \{v \in (X, Y) \| y \leq F (v)\} \leftrightarrow (w \in (X, Y) \land y \leq F (w))) \to if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) = if ((w \in (X, Y) \land y \leq F (w)), y, 0)$
269	267 268	ax-mp	$⊢ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) = if ((w \in (X, Y) \land y \leq F (w)), y, 0)$
270		ifan	$⊢ if ((w \in (X, Y) \land y \leq F (w)), y, 0) = if (w \in (X, Y), if (y \leq F (w), y, 0), 0)$
271	269 270	eqtri	$⊢ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) = if (w \in (X, Y), if (y \leq F (w), y, 0), 0)$
272	259 264 271	3brtr4g	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) \leq if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)$
273	272	ralrimivw	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to \forall w \in ℝ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) \leq if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)$
274		reex	$⊢ ℝ \in V$
275	274	a1i	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to ℝ \in V$
276	57	ad6antlr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \land w \in ℝ) \to if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) \in [0, +∞]$
277	64	ad6antlr	$⊢ ((((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \land w \in ℝ) \to if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \in [0, +∞]$
278		eqidd	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to (w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) = (w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0))$
279		eqidd	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) = (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))$
280	275 276 277 278 279	ofrfval2	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) \leq_{f} (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) \leftrightarrow \forall w \in ℝ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0) \leq if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))$
281	273 280	mpbird	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to (w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) \leq_{f} (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))$
282		itg2le	$⊢ ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) : ℝ ⟶ [0, +∞] \land (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) : ℝ ⟶ [0, +∞] \land (w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0)) \leq_{f} (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \to \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0))) \leq \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)))$
283	166 167 281 282	syl3anc	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to \int^{2} ((w \in ℝ ⟼ if (w \in ((X, Y) \cap (x - z, z + x)), y, 0))) \leq \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)))$
284	50 62 69 165 283	xrltletrd	$⊢ (((((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \land z \in ℝ^{+}) \land \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)) \to 0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)))$
285	4	ad3antrrr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < ({F ↾}_{(X, Y)}) (x)) \to ({F ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ$
286		simplr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < ({F ↾}_{(X, Y)}) (x)) \to x \in (X, Y)$
287		fssres	$⊢ (F : ℝ ⟶ [0, +∞) \land (X, Y) \subseteq ℝ) \to ({F ↾}_{(X, Y)}) : (X, Y) ⟶ [0, +∞)$
288	27 287	mpan2	$⊢ F : ℝ ⟶ [0, +∞) \to ({F ↾}_{(X, Y)}) : (X, Y) ⟶ [0, +∞)$
289		fss	$⊢ (({F ↾}_{(X, Y)}) : (X, Y) ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to ({F ↾}_{(X, Y)}) : (X, Y) ⟶ ℝ$
290	207 289	mpan2	$⊢ ({F ↾}_{(X, Y)}) : (X, Y) ⟶ [0, +∞) \to ({F ↾}_{(X, Y)}) : (X, Y) ⟶ ℝ$
291	2 288 290	3syl	$⊢ φ \to ({F ↾}_{(X, Y)}) : (X, Y) ⟶ ℝ$
292	291	adantr	$⊢ (φ \land y \in ℝ^{+}) \to ({F ↾}_{(X, Y)}) : (X, Y) ⟶ ℝ$
293	292	ffvelcdmda	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to ({F ↾}_{(X, Y)}) (x) \in ℝ$
294	293 218	resubcld	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to ({F ↾}_{(X, Y)}) (x) - y \in ℝ$
295	294	adantr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < ({F ↾}_{(X, Y)}) (x)) \to ({F ↾}_{(X, Y)}) (x) - y \in ℝ$
296	218 293	posdifd	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to (y < ({F ↾}_{(X, Y)}) (x) \leftrightarrow 0 < ({F ↾}_{(X, Y)}) (x) - y)$
297	296	biimpa	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < ({F ↾}_{(X, Y)}) (x)) \to 0 < ({F ↾}_{(X, Y)}) (x) - y$
298	295 297	elrpd	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < ({F ↾}_{(X, Y)}) (x)) \to ({F ↾}_{(X, Y)}) (x) - y \in ℝ^{+}$
299		cncfi	$⊢ (({F ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ \land x \in (X, Y) \land ({F ↾}_{(X, Y)}) (x) - y \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall u \in (X, Y) (\|u - x\| < z \to \|({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x)\| < ({F ↾}_{(X, Y)}) (x) - y)$
300	285 286 298 299	syl3anc	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < ({F ↾}_{(X, Y)}) (x)) \to \exists z \in ℝ^{+} \forall u \in (X, Y) (\|u - x\| < z \to \|({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x)\| < ({F ↾}_{(X, Y)}) (x) - y)$
301	300	ex	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to (y < ({F ↾}_{(X, Y)}) (x) \to \exists z \in ℝ^{+} \forall u \in (X, Y) (\|u - x\| < z \to \|({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x)\| < ({F ↾}_{(X, Y)}) (x) - y))$
302		fvres	$⊢ x \in (X, Y) \to ({F ↾}_{(X, Y)}) (x) = F (x)$
303	302	breq2d	$⊢ x \in (X, Y) \to (y < ({F ↾}_{(X, Y)}) (x) \leftrightarrow y < F (x))$
304	303	adantl	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to (y < ({F ↾}_{(X, Y)}) (x) \leftrightarrow y < F (x))$
305		fvres	$⊢ u \in (X, Y) \to ({F ↾}_{(X, Y)}) (u) = F (u)$
306	305	adantl	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land u \in (X, Y)) \to ({F ↾}_{(X, Y)}) (u) = F (u)$
307	302	ad2antlr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land u \in (X, Y)) \to ({F ↾}_{(X, Y)}) (x) = F (x)$
308	306 307	oveq12d	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land u \in (X, Y)) \to ({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x) = F (u) - F (x)$
309	308	fveq2d	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land u \in (X, Y)) \to \|({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x)\| = \|F (u) - F (x)\|$
310	302	oveq1d	$⊢ x \in (X, Y) \to ({F ↾}_{(X, Y)}) (x) - y = F (x) - y$
311	310	ad2antlr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land u \in (X, Y)) \to ({F ↾}_{(X, Y)}) (x) - y = F (x) - y$
312	309 311	breq12d	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land u \in (X, Y)) \to (\|({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x)\| < ({F ↾}_{(X, Y)}) (x) - y \leftrightarrow \|F (u) - F (x)\| < F (x) - y)$
313	312	imbi2d	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land u \in (X, Y)) \to ((\|u - x\| < z \to \|({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x)\| < ({F ↾}_{(X, Y)}) (x) - y) \leftrightarrow (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y))$
314	313	ralbidva	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to (\forall u \in (X, Y) (\|u - x\| < z \to \|({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x)\| < ({F ↾}_{(X, Y)}) (x) - y) \leftrightarrow \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y))$
315	314	rexbidv	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to (\exists z \in ℝ^{+} \forall u \in (X, Y) (\|u - x\| < z \to \|({F ↾}_{(X, Y)}) (u) - ({F ↾}_{(X, Y)}) (x)\| < ({F ↾}_{(X, Y)}) (x) - y) \leftrightarrow \exists z \in ℝ^{+} \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y))$
316	301 304 315	3imtr3d	$⊢ ((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \to (y < F (x) \to \exists z \in ℝ^{+} \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y))$
317	316	imp	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \to \exists z \in ℝ^{+} \forall u \in (X, Y) (\|u - x\| < z \to \|F (u) - F (x)\| < F (x) - y)$
318	284 317	r19.29a	$⊢ (((φ \land y \in ℝ^{+}) \land x \in (X, Y)) \land y < F (x)) \to 0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)))$
319	318	rexlimdva2	$⊢ (φ \land y \in ℝ^{+}) \to (\exists x \in (X, Y) y < F (x) \to 0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))))$
320	49 319	sylbid	$⊢ (φ \land y \in ℝ^{+}) \to (y < sup (F [(X, Y)] ℝ^{*} <) \to 0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))))$
321	320	imp	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to 0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)))$
322	66	ad2antlr	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) : ℝ ⟶ [0, +∞]$
323		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
324		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F : ℝ ⟶ [0, +∞]$
325	2 323 324	sylancl	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
326	325	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to F : ℝ ⟶ [0, +∞]$
327		breq1	$⊢ y = if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \to (y \leq F (w) \leftrightarrow if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \leq F (w))$
328		breq1	$⊢ 0 = if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \to (0 \leq F (w) \leftrightarrow if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \leq F (w))$
329	267	simprbi	$⊢ w \in \{v \in (X, Y) \| y \leq F (v)\} \to y \leq F (w)$
330	329	adantl	$⊢ ((φ \land w \in ℝ) \land w \in \{v \in (X, Y) \| y \leq F (v)\}) \to y \leq F (w)$
331	2	ffvelcdmda	$⊢ (φ \land w \in ℝ) \to F (w) \in [0, +∞)$
332		elrege0	$⊢ F (w) \in [0, +∞) \leftrightarrow (F (w) \in ℝ \land 0 \leq F (w))$
333	331 332	sylib	$⊢ (φ \land w \in ℝ) \to (F (w) \in ℝ \land 0 \leq F (w))$
334	333	simprd	$⊢ (φ \land w \in ℝ) \to 0 \leq F (w)$
335	334	adantr	$⊢ ((φ \land w \in ℝ) \land \neg w \in \{v \in (X, Y) \| y \leq F (v)\}) \to 0 \leq F (w)$
336	327 328 330 335	ifbothda	$⊢ (φ \land w \in ℝ) \to if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \leq F (w)$
337	336	ralrimiva	$⊢ φ \to \forall w \in ℝ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \leq F (w)$
338	337	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to \forall w \in ℝ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \leq F (w)$
339	274	a1i	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to ℝ \in V$
340	64	ad3antlr	$⊢ (((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \land w \in ℝ) \to if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \in [0, +∞]$
341		fvexd	$⊢ (((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \land w \in ℝ) \to F (w) \in V$
342		eqidd	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) = (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))$
343	2	feqmptd	$⊢ φ \to F = (w \in ℝ ⟼ F (w))$
344	343	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to F = (w \in ℝ ⟼ F (w))$
345	339 340 341 342 344	ofrfval2	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) \leq_{f} F \leftrightarrow \forall w \in ℝ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0) \leq F (w))$
346	338 345	mpbird	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) \leq_{f} F$
347		itg2le	$⊢ ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) : ℝ ⟶ [0, +∞] \land F : ℝ ⟶ [0, +∞] \land (w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0)) \leq_{f} F) \to \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F)$
348	322 326 346 347	syl3anc	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F)$
349	41 321 348	jca32	$⊢ ((φ \land y \in ℝ^{+}) \land y < sup (F [(X, Y)] ℝ^{*} <)) \to (y \in ℝ^{+} \land (0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \land \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F)))$
350	349	expl	$⊢ φ \to ((y \in ℝ^{+} \land y < sup (F [(X, Y)] ℝ^{*} <)) \to (y \in ℝ^{+} \land (0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \land \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F))))$
351	40 350	syl5	$⊢ φ \to ((y \in ℚ \land (0 < y \land y < sup (F [(X, Y)] ℝ^{*} <))) \to (y \in ℝ^{+} \land (0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \land \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F))))$
352	351	reximdv2	$⊢ φ \to (\exists y \in ℚ (0 < y \land y < sup (F [(X, Y)] ℝ^{*} <)) \to \exists y \in ℝ^{+} (0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \land \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F)))$
353	68	adantl	$⊢ (φ \land y \in ℝ^{+}) \to \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \in ℝ^{*}$
354		itg2cl	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) \in ℝ^{*}$
355	325 354	syl	$⊢ φ \to \int^{2} (F) \in ℝ^{*}$
356	355	adantr	$⊢ (φ \land y \in ℝ^{+}) \to \int^{2} (F) \in ℝ^{*}$
357		xrltletr	$⊢ (0 \in ℝ^{} \land \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \in ℝ^{} \land \int^{2} (F) \in ℝ^{*}) \to ((0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \land \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F)) \to 0 < \int^{2} (F))$
358	5 353 356 357	mp3an2i	$⊢ (φ \land y \in ℝ^{+}) \to ((0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \land \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F)) \to 0 < \int^{2} (F))$
359	358	rexlimdva	$⊢ φ \to (\exists y \in ℝ^{+} (0 < \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \land \int^{2} ((w \in ℝ ⟼ if (w \in \{v \in (X, Y) \| y \leq F (v)\}, y, 0))) \leq \int^{2} (F)) \to 0 < \int^{2} (F))$
360	352 359	syld	$⊢ φ \to (\exists y \in ℚ (0 < y \land y < sup (F [(X, Y)] ℝ^{*} <)) \to 0 < \int^{2} (F))$
361	34 360	mpd	$⊢ φ \to 0 < \int^{2} (F)$

Metamath Proof Explorer

Theorem itg2gt0cn

Proof