itg2addnclem3

Description: Lemma incomprehensible in isolation split off to shorten proof of itg2addnc . (Contributed by Brendan Leahy, 11-Mar-2018)

	Ref	Expression
Hypotheses	itg2addnc.f1	$⊢ φ \to F \in MblFn$
	itg2addnc.f2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2addnc.f3	$⊢ φ \to \int^{2} (F) \in ℝ$
	itg2addnc.g2	$⊢ φ \to G : ℝ ⟶ [0, +∞)$
	itg2addnc.g3	$⊢ φ \to \int^{2} (G) \in ℝ$
Assertion	itg2addnclem3	$⊢ φ \to (\exists h \in dom \int^{1} (\exists y \in ℝ^{+} (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \land s = \int^{1} (h)) \to \exists t \exists u (\exists f \in dom \int^{1} \exists g \in dom \int^{1} ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u))$

Proof

Step	Hyp	Ref	Expression
1		itg2addnc.f1	$⊢ φ \to F \in MblFn$
2		itg2addnc.f2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		itg2addnc.f3	$⊢ φ \to \int^{2} (F) \in ℝ$
4		itg2addnc.g2	$⊢ φ \to G : ℝ ⟶ [0, +∞)$
5		itg2addnc.g3	$⊢ φ \to \int^{2} (G) \in ℝ$
6	1 2	itg2addnclem2	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \in dom \int^{1}$
7	6	adantrr	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \in dom \int^{1}$
8		simplr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to h \in dom \int^{1}$
9		i1fsub	$⊢ (h \in dom \int^{1} \land (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \in dom \int^{1}) \to h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \in dom \int^{1}$
10	8 6 9	syl2anc	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \in dom \int^{1}$
11	10	adantrr	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \in dom \int^{1}$
12		3rp	$⊢ 3 \in ℝ^{+}$
13		rpdivcl	$⊢ (y \in ℝ^{+} \land 3 \in ℝ^{+}) \to \frac{y}{3} \in ℝ^{+}$
14	12 13	mpan2	$⊢ y \in ℝ^{+} \to \frac{y}{3} \in ℝ^{+}$
15	14	adantl	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to \frac{y}{3} \in ℝ^{+}$
16		fveq2	$⊢ x = z \to F (x) = F (z)$
17	16	fvoveq1d	$⊢ x = z \to ⌊\frac{F (x)}{\frac{y}{3}}⌋ = ⌊\frac{F (z)}{\frac{y}{3}}⌋$
18	17	oveq1d	$⊢ x = z \to ⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1 = ⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1$
19	18	oveq1d	$⊢ x = z \to (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3})$
20		fveq2	$⊢ x = z \to h (x) = h (z)$
21	19 20	breq12d	$⊢ x = z \to ((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \leftrightarrow (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z))$
22	20	neeq1d	$⊢ x = z \to (h (x) \neq 0 \leftrightarrow h (z) \neq 0)$
23	21 22	anbi12d	$⊢ x = z \to (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0) \leftrightarrow ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0))$
24	23 19 20	ifbieq12d	$⊢ x = z \to if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z))$
25		eqid	$⊢ (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))$
26		ovex	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \in V$
27		fvex	$⊢ h (z) \in V$
28	26 27	ifex	$⊢ if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \in V$
29	24 25 28	fvmpt	$⊢ z \in ℝ \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z))$
30	29	eqeq1d	$⊢ z \in ℝ \to ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0 \leftrightarrow if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0)$
31	29	oveq1d	$⊢ z \in ℝ \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})$
32	30 31	ifbieq2d	$⊢ z \in ℝ \to if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})) = if (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}))$
33	32	adantl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})) = if (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}))$
34		breq1	$⊢ 0 = if (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \to (0 \leq F (z) \leftrightarrow if (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \leq F (z))$
35		breq1	$⊢ if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) = if (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \to (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq F (z) \leftrightarrow if (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \leq F (z))$
36	2	ad2antrr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to F : ℝ ⟶ [0, +∞)$
37	36	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to F (z) \in [0, +∞)$
38		elrege0	$⊢ F (z) \in [0, +∞) \leftrightarrow (F (z) \in ℝ \land 0 \leq F (z))$
39	37 38	sylib	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (F (z) \in ℝ \land 0 \leq F (z))$
40	39	simprd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to 0 \leq F (z)$
41	40	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to 0 \leq F (z)$
42		df-ne	$⊢ if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \neq 0 \leftrightarrow \neg if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0$
43		neeq1	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \neq 0 \leftrightarrow if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \neq 0)$
44		oveq1	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})$
45	44	breq1d	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq F (z) \leftrightarrow if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq F (z))$
46	43 45	imbi12d	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \neq 0 \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq F (z)) \leftrightarrow (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \neq 0 \to if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq F (z)))$
47		neeq1	$⊢ h (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to (h (z) \neq 0 \leftrightarrow if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \neq 0)$
48		oveq1	$⊢ h (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to h (z) + (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})$
49	48	breq1d	$⊢ h (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to (h (z) + (\frac{y}{3}) \leq F (z) \leftrightarrow if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq F (z))$
50	47 49	imbi12d	$⊢ h (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to ((h (z) \neq 0 \to h (z) + (\frac{y}{3}) \leq F (z)) \leftrightarrow (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \neq 0 \to if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq F (z)))$
51		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
52	51 37	sseldi	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to F (z) \in ℝ$
53	14	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to \frac{y}{3} \in ℝ^{+}$
54	52 53	rerpdivcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to \frac{F (z)}{\frac{y}{3}} \in ℝ$
55		reflcl	$⊢ \frac{F (z)}{\frac{y}{3}} \in ℝ \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ \in ℝ$
56		peano2rem	$⊢ ⌊\frac{F (z)}{\frac{y}{3}}⌋ \in ℝ \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1 \in ℝ$
57	54 55 56	3syl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1 \in ℝ$
58	14	rpred	$⊢ y \in ℝ^{+} \to \frac{y}{3} \in ℝ$
59	58	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to \frac{y}{3} \in ℝ$
60	57 59	remulcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \in ℝ$
61		peano2rem	$⊢ \frac{F (z)}{\frac{y}{3}} \in ℝ \to (\frac{F (z)}{\frac{y}{3}}) - 1 \in ℝ$
62	54 61	syl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) - 1 \in ℝ$
63	62 59	remulcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3}) \in ℝ$
64	54 55	syl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ \in ℝ$
65		1red	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to 1 \in ℝ$
66		flle	$⊢ \frac{F (z)}{\frac{y}{3}} \in ℝ \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ \leq \frac{F (z)}{\frac{y}{3}}$
67	54 66	syl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ \leq \frac{F (z)}{\frac{y}{3}}$
68	64 54 65 67	lesub1dd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1 \leq (\frac{F (z)}{\frac{y}{3}}) - 1$
69	57 62 53	lemul1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1 \leq (\frac{F (z)}{\frac{y}{3}}) - 1 \leftrightarrow (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3}))$
70	68 69	mpbid	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3})$
71	60 63 59 70	leadd1dd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3}) + (\frac{y}{3})$
72	54	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to \frac{F (z)}{\frac{y}{3}} \in ℂ$
73		ax-1cn	$⊢ 1 \in ℂ$
74		subcl	$⊢ (\frac{F (z)}{\frac{y}{3}} \in ℂ \land 1 \in ℂ) \to (\frac{F (z)}{\frac{y}{3}}) - 1 \in ℂ$
75	72 73 74	sylancl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) - 1 \in ℂ$
76	73	a1i	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to 1 \in ℂ$
77	53	rpcnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to \frac{y}{3} \in ℂ$
78	75 76 77	adddird	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - 1 + 1) (\frac{y}{3}) = ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3}) + 1 (\frac{y}{3})$
79		npcan	$⊢ (\frac{F (z)}{\frac{y}{3}} \in ℂ \land 1 \in ℂ) \to (\frac{F (z)}{\frac{y}{3}}) - 1 + 1 = \frac{F (z)}{\frac{y}{3}}$
80	72 73 79	sylancl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) - 1 + 1 = \frac{F (z)}{\frac{y}{3}}$
81	80	oveq1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - 1 + 1) (\frac{y}{3}) = (\frac{F (z)}{\frac{y}{3}}) (\frac{y}{3})$
82	77	mulid2d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to 1 (\frac{y}{3}) = \frac{y}{3}$
83	82	oveq2d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3}) + 1 (\frac{y}{3}) = ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3}) + (\frac{y}{3})$
84	78 81 83	3eqtr3rd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3}) + (\frac{y}{3}) = (\frac{F (z)}{\frac{y}{3}}) (\frac{y}{3})$
85	52	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to F (z) \in ℂ$
86	53	rpne0d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to \frac{y}{3} \neq 0$
87	85 77 86	divcan1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) (\frac{y}{3}) = F (z)$
88	84 87	eqtrd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - 1) (\frac{y}{3}) + (\frac{y}{3}) = F (z)$
89	71 88	breqtrd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq F (z)$
90	89	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq F (z)$
91	90	a1d	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \to ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \neq 0 \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq F (z))$
92		ianor	$⊢ \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0) \leftrightarrow (\neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \lor \neg h (z) \neq 0)$
93	92	anbi1i	$⊢ (\neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0) \land h (z) \neq 0) \leftrightarrow ((\neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \lor \neg h (z) \neq 0) \land h (z) \neq 0)$
94		oranabs	$⊢ ((\neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \lor \neg h (z) \neq 0) \land h (z) \neq 0) \leftrightarrow (\neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)$
95	93 94	bitri	$⊢ (\neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0) \land h (z) \neq 0) \leftrightarrow (\neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)$
96		i1ff	$⊢ h \in dom \int^{1} \to h : ℝ ⟶ ℝ$
97	96	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to h : ℝ ⟶ ℝ$
98	97	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to h (z) \in ℝ$
99	98 59	readdcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to h (z) + (\frac{y}{3}) \in ℝ$
100	99	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to h (z) + (\frac{y}{3}) \in ℝ$
101	52	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to F (z) \in ℝ$
102	60 59	readdcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \in ℝ$
103	102	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \in ℝ$
104	98	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to h (z) \in ℝ$
105	60	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \in ℝ$
106	58	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to \frac{y}{3} \in ℝ$
107	98 60	ltnled	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (h (z) < (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leftrightarrow \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z))$
108	107	biimpar	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to h (z) < (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3})$
109	104 105 106 108	ltadd1dd	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to h (z) + (\frac{y}{3}) < (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3})$
110	89	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq F (z)$
111	100 103 101 109 110	ltletrd	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to h (z) + (\frac{y}{3}) < F (z)$
112	100 101 111	ltled	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z)) \to h (z) + (\frac{y}{3}) \leq F (z)$
113	112	adantrr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land (\neg (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \to h (z) + (\frac{y}{3}) \leq F (z)$
114	95 113	sylan2b	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land (\neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0) \land h (z) \neq 0)) \to h (z) + (\frac{y}{3}) \leq F (z)$
115	114	expr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \to (h (z) \neq 0 \to h (z) + (\frac{y}{3}) \leq F (z))$
116	46 50 91 115	ifbothda	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \neq 0 \to if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq F (z))$
117	42 116	syl5bir	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\neg if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0 \to if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq F (z))$
118	117	imp	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq F (z)$
119	34 35 41 118	ifbothda	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to if (if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \leq F (z)$
120	33 119	eqbrtrd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})) \leq F (z)$
121	120	ralrimiva	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to \forall z \in ℝ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})) \leq F (z)$
122		reex	$⊢ ℝ \in V$
123	122	a1i	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to ℝ \in V$
124		c0ex	$⊢ 0 \in V$
125		ovex	$⊢ (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3}) \in V$
126	124 125	ifex	$⊢ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})) \in V$
127	126	a1i	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})) \in V$
128		eqidd	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3}))) = (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})))$
129	2	feqmptd	$⊢ φ \to F = (z \in ℝ ⟼ F (z))$
130	129	ad2antrr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to F = (z \in ℝ ⟼ F (z))$
131	123 127 37 128 130	ofrfval2	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to ((z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3}))) \leq_{f} F \leftrightarrow \forall z \in ℝ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})) \leq F (z))$
132	121 131	mpbird	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3}))) \leq_{f} F$
133		oveq2	$⊢ c = \frac{y}{3} \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})$
134	133	ifeq2d	$⊢ c = \frac{y}{3} \to if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c) = if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3}))$
135	134	mpteq2dv	$⊢ c = \frac{y}{3} \to (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) = (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3})))$
136	135	breq1d	$⊢ c = \frac{y}{3} \to ((z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \leftrightarrow (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3}))) \leq_{f} F)$
137	136	rspcev	$⊢ (\frac{y}{3} \in ℝ^{+} \land (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + (\frac{y}{3}))) \leq_{f} F) \to \exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F$
138	15 132 137	syl2anc	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to \exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F$
139	138	adantrr	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to \exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F$
140	14	ad2antrl	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to \frac{y}{3} \in ℝ^{+}$
141	96	ffnd	$⊢ h \in dom \int^{1} \to h Fn ℝ$
142	141	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to h Fn ℝ$
143		ovex	$⊢ (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \in V$
144		fvex	$⊢ h (x) \in V$
145	143 144	ifex	$⊢ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) \in V$
146	145 25	fnmpti	$⊢ (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) Fn ℝ$
147	146	a1i	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) Fn ℝ$
148		inidm	$⊢ ℝ \cap ℝ = ℝ$
149		eqidd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to h (z) = h (z)$
150	29	adantl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z))$
151	142 147 123 123 148 149 150	ofval	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z))$
152	151	eqeq1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0 \leftrightarrow h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0)$
153	151	oveq1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}) = h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})$
154	152 153	ifbieq2d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) = if (h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}))$
155	154	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \to if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) = if (h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}))$
156		breq1	$⊢ 0 = if (h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \to (0 \leq G (z) \leftrightarrow if (h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \leq G (z))$
157		breq1	$⊢ h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) = if (h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \to (h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq G (z) \leftrightarrow if (h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \leq G (z))$
158	4	ad2antrr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to G : ℝ ⟶ [0, +∞)$
159	158	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to G (z) \in [0, +∞)$
160		elrege0	$⊢ G (z) \in [0, +∞) \leftrightarrow (G (z) \in ℝ \land 0 \leq G (z))$
161	159 160	sylib	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (G (z) \in ℝ \land 0 \leq G (z))$
162	161	simprd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to 0 \leq G (z)$
163	162	ad2antrr	$⊢ (((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \land h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to 0 \leq G (z)$
164		oveq2	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z))$
165	164	oveq1d	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) = h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})$
166	165	breq1d	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to (h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq G (z) \leftrightarrow h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq G (z))$
167		oveq2	$⊢ h (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to h (z) - h (z) = h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z))$
168	167	oveq1d	$⊢ h (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to h (z) - h (z) + (\frac{y}{3}) = h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})$
169	168	breq1d	$⊢ h (z) = if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) \to (h (z) - h (z) + (\frac{y}{3}) \leq G (z) \leftrightarrow h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq G (z))$
170		id	$⊢ h (z) = 0 \to h (z) = 0$
171		simpr	$⊢ ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0) \to h (z) \neq 0$
172	171	necon2bi	$⊢ h (z) = 0 \to \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)$
173		iffalse	$⊢ \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0) \to if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = h (z)$
174	172 173	syl	$⊢ h (z) = 0 \to if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = h (z)$
175	174 170	eqtrd	$⊢ h (z) = 0 \to if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0$
176	170 175	oveq12d	$⊢ h (z) = 0 \to h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0 - 0$
177		0m0e0	$⊢ 0 - 0 = 0$
178	176 177	syl6eq	$⊢ h (z) = 0 \to h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0$
179		iffalse	$⊢ \neg h (z) = 0 \to if (h (z) = 0, 0, h (z) + y) = h (z) + y$
180	179	breq1d	$⊢ \neg h (z) = 0 \to (if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z) \leftrightarrow h (z) + y \leq F (z) + G (z))$
181	178 180	nsyl5	$⊢ \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0 \to (if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z) \leftrightarrow h (z) + y \leq F (z) + G (z))$
182	181	adantl	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to (if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z) \leftrightarrow h (z) + y \leq F (z) + G (z))$
183	98	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to h (z) \in ℂ$
184	60	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \in ℂ$
185	183 184 77	subsubd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to h (z) - ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) = h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3})$
186	185	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land h (z) + y \leq F (z) + G (z)) \to h (z) - ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) = h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3})$
187	60 59	resubcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) \in ℝ$
188		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
189	188	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to y \in ℝ$
190	187 189	readdcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) + y \in ℝ$
191	51 159	sseldi	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to G (z) \in ℝ$
192		1re	$⊢ 1 \in ℝ$
193	192 192	readdcli	$⊢ 1 + 1 \in ℝ$
194		resubcl	$⊢ (\frac{F (z)}{\frac{y}{3}} \in ℝ \land 1 + 1 \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) - (1 + 1) \in ℝ$
195	54 193 194	sylancl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) - (1 + 1) \in ℝ$
196	195 59	remulcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1)) (\frac{y}{3}) \in ℝ$
197		peano2re	$⊢ ⌊\frac{F (z)}{\frac{y}{3}}⌋ \in ℝ \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 \in ℝ$
198	64 197	syl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 \in ℝ$
199		resubcl	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 \in ℝ \land 1 + 1 \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1) \in ℝ$
200	198 193 199	sylancl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1) \in ℝ$
201	200 59	remulcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)) (\frac{y}{3}) \in ℝ$
202	58 188	resubcld	$⊢ y \in ℝ^{+} \to (\frac{y}{3}) - y \in ℝ$
203	202	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{y}{3}) - y \in ℝ$
204	193	a1i	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to 1 + 1 \in ℝ$
205		fllep1	$⊢ \frac{F (z)}{\frac{y}{3}} \in ℝ \to \frac{F (z)}{\frac{y}{3}} \leq ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1$
206	54 205	syl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to \frac{F (z)}{\frac{y}{3}} \leq ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1$
207	54 198 204 206	lesub1dd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) - (1 + 1) \leq ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)$
208	195 200 53	lemul1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1) \leq ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1) \leftrightarrow ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1)) (\frac{y}{3}) \leq (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)) (\frac{y}{3}))$
209	207 208	mpbid	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1)) (\frac{y}{3}) \leq (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)) (\frac{y}{3})$
210	196 201 203 209	lesub1dd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1)) (\frac{y}{3}) - ((\frac{y}{3}) - y) \leq (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)) (\frac{y}{3}) - ((\frac{y}{3}) - y)$
211	73 73	addcli	$⊢ 1 + 1 \in ℂ$
212	211	negcli	$⊢ - (1 + 1) \in ℂ$
213	212	a1i	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to - (1 + 1) \in ℂ$
214	72 213 77	adddird	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) + (- (1 + 1))) (\frac{y}{3}) = (\frac{F (z)}{\frac{y}{3}}) (\frac{y}{3}) + (- (1 + 1)) (\frac{y}{3})$
215		negsub	$⊢ (\frac{F (z)}{\frac{y}{3}} \in ℂ \land 1 + 1 \in ℂ) \to (\frac{F (z)}{\frac{y}{3}}) + (- (1 + 1)) = (\frac{F (z)}{\frac{y}{3}}) - (1 + 1)$
216	72 211 215	sylancl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) + (- (1 + 1)) = (\frac{F (z)}{\frac{y}{3}}) - (1 + 1)$
217	216	oveq1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) + (- (1 + 1))) (\frac{y}{3}) = ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1)) (\frac{y}{3})$
218		df-2	$⊢ 2 = 1 + 1$
219	218	negeqi	$⊢ - 2 = - (1 + 1)$
220	219	oveq1i	$⊢ -2 (\frac{y}{3}) = (- (1 + 1)) (\frac{y}{3})$
221		2cn	$⊢ 2 \in ℂ$
222	14	rpcnd	$⊢ y \in ℝ^{+} \to \frac{y}{3} \in ℂ$
223		mulneg1	$⊢ (2 \in ℂ \land \frac{y}{3} \in ℂ) \to -2 (\frac{y}{3}) = - 2 (\frac{y}{3})$
224	221 222 223	sylancr	$⊢ y \in ℝ^{+} \to -2 (\frac{y}{3}) = - 2 (\frac{y}{3})$
225	220 224	syl5eqr	$⊢ y \in ℝ^{+} \to (- (1 + 1)) (\frac{y}{3}) = - 2 (\frac{y}{3})$
226	225	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (- (1 + 1)) (\frac{y}{3}) = - 2 (\frac{y}{3})$
227	87 226	oveq12d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{F (z)}{\frac{y}{3}}) (\frac{y}{3}) + (- (1 + 1)) (\frac{y}{3}) = F (z) + (- 2 (\frac{y}{3}))$
228	214 217 227	3eqtr3d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1)) (\frac{y}{3}) = F (z) + (- 2 (\frac{y}{3}))$
229		rpcn	$⊢ y \in ℝ^{+} \to y \in ℂ$
230	229 222	negsubdi2d	$⊢ y \in ℝ^{+} \to - (y - (\frac{y}{3})) = (\frac{y}{3}) - y$
231		3cn	$⊢ 3 \in ℂ$
232		3ne0	$⊢ 3 \neq 0$
233		divcan2	$⊢ (y \in ℂ \land 3 \in ℂ \land 3 \neq 0) \to 3 (\frac{y}{3}) = y$
234	231 232 233	mp3an23	$⊢ y \in ℂ \to 3 (\frac{y}{3}) = y$
235	229 234	syl	$⊢ y \in ℝ^{+} \to 3 (\frac{y}{3}) = y$
236	222	mulid2d	$⊢ y \in ℝ^{+} \to 1 (\frac{y}{3}) = \frac{y}{3}$
237	235 236	oveq12d	$⊢ y \in ℝ^{+} \to 3 (\frac{y}{3}) - 1 (\frac{y}{3}) = y - (\frac{y}{3})$
238		3m1e2	$⊢ 3 - 1 = 2$
239	238	oveq1i	$⊢ (3 - 1) (\frac{y}{3}) = 2 (\frac{y}{3})$
240		subdir	$⊢ (3 \in ℂ \land 1 \in ℂ \land \frac{y}{3} \in ℂ) \to (3 - 1) (\frac{y}{3}) = 3 (\frac{y}{3}) - 1 (\frac{y}{3})$
241	231 73 222 240	mp3an12i	$⊢ y \in ℝ^{+} \to (3 - 1) (\frac{y}{3}) = 3 (\frac{y}{3}) - 1 (\frac{y}{3})$
242	239 241	syl5reqr	$⊢ y \in ℝ^{+} \to 3 (\frac{y}{3}) - 1 (\frac{y}{3}) = 2 (\frac{y}{3})$
243	237 242	eqtr3d	$⊢ y \in ℝ^{+} \to y - (\frac{y}{3}) = 2 (\frac{y}{3})$
244	243	negeqd	$⊢ y \in ℝ^{+} \to - (y - (\frac{y}{3})) = - 2 (\frac{y}{3})$
245	230 244	eqtr3d	$⊢ y \in ℝ^{+} \to (\frac{y}{3}) - y = - 2 (\frac{y}{3})$
246	245	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (\frac{y}{3}) - y = - 2 (\frac{y}{3})$
247	228 246	oveq12d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1)) (\frac{y}{3}) - ((\frac{y}{3}) - y) = F (z) + (- 2 (\frac{y}{3})) - (- 2 (\frac{y}{3}))$
248		rpcn	$⊢ \frac{y}{3} \in ℝ^{+} \to \frac{y}{3} \in ℂ$
249		mulcl	$⊢ (2 \in ℂ \land \frac{y}{3} \in ℂ) \to 2 (\frac{y}{3}) \in ℂ$
250	221 248 249	sylancr	$⊢ \frac{y}{3} \in ℝ^{+} \to 2 (\frac{y}{3}) \in ℂ$
251	14 250	syl	$⊢ y \in ℝ^{+} \to 2 (\frac{y}{3}) \in ℂ$
252	251	negcld	$⊢ y \in ℝ^{+} \to - 2 (\frac{y}{3}) \in ℂ$
253	252	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to - 2 (\frac{y}{3}) \in ℂ$
254	85 253	pncand	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to F (z) + (- 2 (\frac{y}{3})) - (- 2 (\frac{y}{3})) = F (z)$
255	247 254	eqtrd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((\frac{F (z)}{\frac{y}{3}}) - (1 + 1)) (\frac{y}{3}) - ((\frac{y}{3}) - y) = F (z)$
256	64	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ \in ℂ$
257		peano2cn	$⊢ ⌊\frac{F (z)}{\frac{y}{3}}⌋ \in ℂ \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 \in ℂ$
258		subsub4	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1) - 1 - 1 = ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)$
259	73 73 258	mp3an23	$⊢ ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 \in ℂ \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1) - 1 - 1 = ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)$
260	256 257 259	3syl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1) - 1 - 1 = ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)$
261		pncan	$⊢ (⌊\frac{F (z)}{\frac{y}{3}}⌋ \in ℂ \land 1 \in ℂ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - 1 = ⌊\frac{F (z)}{\frac{y}{3}}⌋$
262	256 73 261	sylancl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - 1 = ⌊\frac{F (z)}{\frac{y}{3}}⌋$
263	262	oveq1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1) - 1 - 1 = ⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1$
264	260 263	eqtr3d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1) = ⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1$
265	264	oveq1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)) (\frac{y}{3}) = (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3})$
266	265	oveq1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)) (\frac{y}{3}) - ((\frac{y}{3}) - y) = (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - ((\frac{y}{3}) - y)$
267	189	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to y \in ℂ$
268	184 77 267	subsubd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - ((\frac{y}{3}) - y) = (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) + y$
269	266 268	eqtrd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ + 1 - (1 + 1)) (\frac{y}{3}) - ((\frac{y}{3}) - y) = (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) + y$
270	210 255 269	3brtr3d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to F (z) \leq (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) + y$
271	52 190 191 270	leadd1dd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to F (z) + G (z) \leq ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y + G (z)$
272	191	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to G (z) \in ℂ$
273	187	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) \in ℂ$
274	229	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to y \in ℂ$
275	273 274	addcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) + y \in ℂ$
276	272 273 274	addassd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y = G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y$
277	272 275 276	comraddd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y = ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y + G (z)$
278	271 277	breqtrrd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to F (z) + G (z) \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y$
279	98 189	readdcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to h (z) + y \in ℝ$
280	52 191	readdcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to F (z) + G (z) \in ℝ$
281	191 187	readdcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to G (z) + (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) \in ℝ$
282	281 189	readdcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y \in ℝ$
283		letr	$⊢ (h (z) + y \in ℝ \land F (z) + G (z) \in ℝ \land G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y \in ℝ) \to ((h (z) + y \leq F (z) + G (z) \land F (z) + G (z) \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y) \to h (z) + y \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y)$
284	279 280 282 283	syl3anc	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to ((h (z) + y \leq F (z) + G (z) \land F (z) + G (z) \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y) \to h (z) + y \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y)$
285	278 284	mpan2d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (h (z) + y \leq F (z) + G (z) \to h (z) + y \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y)$
286	285	imp	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land h (z) + y \leq F (z) + G (z)) \to h (z) + y \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y$
287	98 187 191	lesubaddd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (h (z) - ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) \leq G (z) \leftrightarrow h (z) \leq G (z) + (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}))$
288	98 281 189	leadd1d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (h (z) \leq G (z) + (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3}) \leftrightarrow h (z) + y \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y)$
289	287 288	bitrd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (h (z) - ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) \leq G (z) \leftrightarrow h (z) + y \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y)$
290	289	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land h (z) + y \leq F (z) + G (z)) \to (h (z) - ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) \leq G (z) \leftrightarrow h (z) + y \leq G (z) + ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) + y)$
291	286 290	mpbird	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land h (z) + y \leq F (z) + G (z)) \to h (z) - ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) - (\frac{y}{3})) \leq G (z)$
292	186 291	eqbrtrrd	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land h (z) + y \leq F (z) + G (z)) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq G (z)$
293	292	ex	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (h (z) + y \leq F (z) + G (z) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq G (z))$
294	293	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to (h (z) + y \leq F (z) + G (z) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq G (z))$
295	182 294	sylbid	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to (if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq G (z))$
296	295	imp	$⊢ (((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq G (z)$
297	296	an32s	$⊢ (((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq G (z)$
298	297	adantr	$⊢ ((((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \land ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \to h (z) - (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) + (\frac{y}{3}) \leq G (z)$
299	173	oveq2d	$⊢ \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0) \to h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = h (z) - h (z)$
300	183	subidd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to h (z) - h (z) = 0$
301	300	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \to h (z) - h (z) = 0$
302	299 301	sylan9eqr	$⊢ (((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \land \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \to h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0$
303	302	pm2.24d	$⊢ (((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \land \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \to (\neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0 \to h (z) - h (z) + (\frac{y}{3}) \leq G (z))$
304	303	imp	$⊢ ((((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \land \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to h (z) - h (z) + (\frac{y}{3}) \leq G (z)$
305	304	an32s	$⊢ ((((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \land \neg ((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0)) \to h (z) - h (z) + (\frac{y}{3}) \leq G (z)$
306	166 169 298 305	ifbothda	$⊢ (((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \land \neg h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0) \to h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3}) \leq G (z)$
307	156 157 163 306	ifbothda	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \to if (h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) = 0, 0, h (z) - if (((⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (z) \land h (z) \neq 0), (⌊\frac{F (z)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (z)) + (\frac{y}{3})) \leq G (z)$
308	155 307	eqbrtrd	$⊢ ((((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \land if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z)) \to if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) \leq G (z)$
309	308	ex	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land z \in ℝ) \to (if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z) \to if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) \leq G (z))$
310	309	ralimdva	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (\forall z \in ℝ if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z) \to \forall z \in ℝ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) \leq G (z))$
311	122	a1i	$⊢ φ \to ℝ \in V$
312		ovex	$⊢ h (z) + y \in V$
313	124 312	ifex	$⊢ if (h (z) = 0, 0, h (z) + y) \in V$
314	313	a1i	$⊢ (φ \land z \in ℝ) \to if (h (z) = 0, 0, h (z) + y) \in V$
315	2	ffvelrnda	$⊢ (φ \land z \in ℝ) \to F (z) \in [0, +∞)$
316	51 315	sseldi	$⊢ (φ \land z \in ℝ) \to F (z) \in ℝ$
317	4	ffvelrnda	$⊢ (φ \land z \in ℝ) \to G (z) \in [0, +∞)$
318	51 317	sseldi	$⊢ (φ \land z \in ℝ) \to G (z) \in ℝ$
319	316 318	readdcld	$⊢ (φ \land z \in ℝ) \to F (z) + G (z) \in ℝ$
320		eqidd	$⊢ φ \to (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) = (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y))$
321	4	feqmptd	$⊢ φ \to G = (z \in ℝ ⟼ G (z))$
322	311 315 317 129 321	offval2	$⊢ φ \to F +_{f} G = (z \in ℝ ⟼ F (z) + G (z))$
323	311 314 319 320 322	ofrfval2	$⊢ φ \to ((z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \leftrightarrow \forall z \in ℝ if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z))$
324	323	ad2antrr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to ((z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \leftrightarrow \forall z \in ℝ if (h (z) = 0, 0, h (z) + y) \leq F (z) + G (z))$
325		ovex	$⊢ (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}) \in V$
326	124 325	ifex	$⊢ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) \in V$
327	326	a1i	$⊢ (φ \land z \in ℝ) \to if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) \in V$
328		eqidd	$⊢ φ \to (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}))) = (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})))$
329	311 327 317 328 321	ofrfval2	$⊢ φ \to ((z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}))) \leq_{f} G \leftrightarrow \forall z \in ℝ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) \leq G (z))$
330	329	ad2antrr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to ((z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}))) \leq_{f} G \leftrightarrow \forall z \in ℝ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})) \leq G (z))$
331	310 324 330	3imtr4d	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to ((z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \to (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}))) \leq_{f} G)$
332	331	impr	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}))) \leq_{f} G$
333		oveq2	$⊢ d = \frac{y}{3} \to (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d = (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})$
334	333	ifeq2d	$⊢ d = \frac{y}{3} \to if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d) = if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}))$
335	334	mpteq2dv	$⊢ d = \frac{y}{3} \to (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) = (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3})))$
336	335	breq1d	$⊢ d = \frac{y}{3} \to ((z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \leftrightarrow (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}))) \leq_{f} G)$
337	336	rspcev	$⊢ (\frac{y}{3} \in ℝ^{+} \land (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + (\frac{y}{3}))) \leq_{f} G) \to \exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G$
338	140 332 337	syl2anc	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to \exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G$
339	36	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to F (x) \in [0, +∞)$
340	51 339	sseldi	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to F (x) \in ℝ$
341	14	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to \frac{y}{3} \in ℝ^{+}$
342	340 341	rerpdivcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to \frac{F (x)}{\frac{y}{3}} \in ℝ$
343		reflcl	$⊢ \frac{F (x)}{\frac{y}{3}} \in ℝ \to ⌊\frac{F (x)}{\frac{y}{3}}⌋ \in ℝ$
344		peano2rem	$⊢ ⌊\frac{F (x)}{\frac{y}{3}}⌋ \in ℝ \to ⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1 \in ℝ$
345	342 343 344	3syl	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1 \in ℝ$
346	58	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to \frac{y}{3} \in ℝ$
347	345 346	remulcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \in ℝ$
348	97	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to h (x) \in ℝ$
349	347 348	ifcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) \in ℝ$
350	349	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) \in ℂ$
351	348	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to h (x) \in ℂ$
352	350 351	pncan3d	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) + h (x) - if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) = h (x)$
353	352	mpteq2dva	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) + h (x) - if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) = (x \in ℝ ⟼ h (x))$
354	348 349	resubcld	$⊢ (((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \land x \in ℝ) \to h (x) - if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) \in ℝ$
355		eqidd	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))$
356	96	feqmptd	$⊢ h \in dom \int^{1} \to h = (x \in ℝ ⟼ h (x))$
357	356	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to h = (x \in ℝ ⟼ h (x))$
358	123 348 349 357 355	offval2	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) = (x \in ℝ ⟼ h (x) - if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))$
359	123 349 354 355 358	offval2	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) +_{f} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)) + h (x) - if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))$
360	353 359 357	3eqtr4d	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) +_{f} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) = h$
361	360	fveq2d	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) +_{f} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) = \int^{1} (h)$
362	6 10	itg1add	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) +_{f} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) + \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))$
363	361 362	eqtr3d	$⊢ ((φ \land h \in dom \int^{1}) \land y \in ℝ^{+}) \to \int^{1} (h) = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) + \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))$
364	363	adantrr	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to \int^{1} (h) = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) + \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))$
365		fvex	$⊢ \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \in V$
366		fvex	$⊢ \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \in V$
367		iba	$⊢ t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \to (\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \leftrightarrow (\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))))$
368		iba	$⊢ u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \to (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \leftrightarrow (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))))$
369	367 368	bi2anan9	$⊢ (t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \to ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land \exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G) \leftrightarrow ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))))$
370	369	bicomd	$⊢ (t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \to (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))) \leftrightarrow (\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land \exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G))$
371		oveq12	$⊢ (t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \to t + u = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) + \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))$
372	371	eqeq2d	$⊢ (t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \to (\int^{1} (h) = t + u \leftrightarrow \int^{1} (h) = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) + \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))$
373	370 372	anbi12d	$⊢ (t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \to ((((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))) \land \int^{1} (h) = t + u) \leftrightarrow ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land \exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G) \land \int^{1} (h) = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) + \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))))$
374	365 366 373	spc2ev	$⊢ ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land \exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G) \land \int^{1} (h) = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) + \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \to \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))) \land \int^{1} (h) = t + u)$
375	139 338 364 374	syl21anc	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))) \land \int^{1} (h) = t + u)$
376		fveq1	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to f (z) = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z)$
377	376	eqeq1d	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (f (z) = 0 \leftrightarrow (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0)$
378	376	oveq1d	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to f (z) + c = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c$
379	377 378	ifbieq2d	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to if (f (z) = 0, 0, f (z) + c) = if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)$
380	379	mpteq2dv	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) = (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c))$
381	380	breq1d	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \leftrightarrow (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F)$
382	381	rexbidv	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \leftrightarrow \exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F)$
383		fveq2	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to \int^{1} (f) = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))$
384	383	eqeq2d	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (t = \int^{1} (f) \leftrightarrow t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))$
385	382 384	anbi12d	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \leftrightarrow (\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))))$
386	385	anbi1d	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \leftrightarrow ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))))$
387	386	anbi1d	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to ((((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u) \leftrightarrow (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u))$
388	387	2exbidv	$⊢ f = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (\exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u) \leftrightarrow \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u))$
389		fveq1	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to g (z) = (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z)$
390	389	eqeq1d	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (g (z) = 0 \leftrightarrow (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0)$
391	389	oveq1d	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to g (z) + d = (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d$
392	390 391	ifbieq2d	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to if (g (z) = 0, 0, g (z) + d) = if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)$
393	392	mpteq2dv	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) = (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d))$
394	393	breq1d	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to ((z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \leftrightarrow (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G)$
395	394	rexbidv	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \leftrightarrow \exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G)$
396		fveq2	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to \int^{1} (g) = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))$
397	396	eqeq2d	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (u = \int^{1} (g) \leftrightarrow u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))$
398	395 397	anbi12d	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to ((\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g)) \leftrightarrow (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))))$
399	398	anbi2d	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \leftrightarrow ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))))$
400	399	anbi1d	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to ((((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u) \leftrightarrow (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))) \land \int^{1} (h) = t + u))$
401	400	2exbidv	$⊢ g = h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \to (\exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u) \leftrightarrow \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))) \land \int^{1} (h) = t + u))$
402	388 401	rspc2ev	$⊢ ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \in dom \int^{1} \land h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) \in dom \int^{1} \land \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) = 0, 0, (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))) (z) + c)) \leq_{f} F \land t = \int^{1} ((x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x))))) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if ((h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) = 0, 0, (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))) (z) + d)) \leq_{f} G \land u = \int^{1} (h -_{f} (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{y}{3}}⌋ - 1) (\frac{y}{3}), h (x)))))) \land \int^{1} (h) = t + u)) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u)$
403	7 11 375 402	syl3anc	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u)$
404		eqeq1	$⊢ s = \int^{1} (h) \to (s = t + u \leftrightarrow \int^{1} (h) = t + u)$
405	404	anbi2d	$⊢ s = \int^{1} (h) \to ((((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u))$
406	405	2exbidv	$⊢ s = \int^{1} (h) \to (\exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u))$
407	406	2rexbidv	$⊢ s = \int^{1} (h) \to (\exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land \int^{1} (h) = t + u))$
408	403 407	syl5ibrcom	$⊢ ((φ \land h \in dom \int^{1}) \land (y \in ℝ^{+} \land (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G))) \to (s = \int^{1} (h) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u))$
409	408	rexlimdvaa	$⊢ (φ \land h \in dom \int^{1}) \to (\exists y \in ℝ^{+} (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \to (s = \int^{1} (h) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)))$
410	409	impd	$⊢ (φ \land h \in dom \int^{1}) \to ((\exists y \in ℝ^{+} (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \land s = \int^{1} (h)) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u))$
411	410	rexlimdva	$⊢ φ \to (\exists h \in dom \int^{1} (\exists y \in ℝ^{+} (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \land s = \int^{1} (h)) \to \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u))$
412		rexcom4	$⊢ \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists t \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
413	412	rexbii	$⊢ \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists f \in dom \int^{1} \exists t \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
414		rexcom4	$⊢ \exists f \in dom \int^{1} \exists t \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists t \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
415	413 414	bitri	$⊢ \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists t \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
416		rexcom4	$⊢ \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists u \exists g \in dom \int^{1} (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
417	416	rexbii	$⊢ \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists f \in dom \int^{1} \exists u \exists g \in dom \int^{1} (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
418		rexcom4	$⊢ \exists f \in dom \int^{1} \exists u \exists g \in dom \int^{1} (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists u \exists f \in dom \int^{1} \exists g \in dom \int^{1} (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
419	417 418	bitri	$⊢ \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists u \exists f \in dom \int^{1} \exists g \in dom \int^{1} (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
420	419	exbii	$⊢ \exists t \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists t \exists u \exists f \in dom \int^{1} \exists g \in dom \int^{1} (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
421		r19.41vv	$⊢ \exists f \in dom \int^{1} \exists g \in dom \int^{1} (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow (\exists f \in dom \int^{1} \exists g \in dom \int^{1} ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
422	421	2exbii	$⊢ \exists t \exists u \exists f \in dom \int^{1} \exists g \in dom \int^{1} (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists t \exists u (\exists f \in dom \int^{1} \exists g \in dom \int^{1} ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
423	415 420 422	3bitrri	$⊢ \exists t \exists u (\exists f \in dom \int^{1} \exists g \in dom \int^{1} ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u) \leftrightarrow \exists f \in dom \int^{1} \exists g \in dom \int^{1} \exists t \exists u (((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u)$
424	411 423	syl6ibr	$⊢ φ \to (\exists h \in dom \int^{1} (\exists y \in ℝ^{+} (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \land s = \int^{1} (h)) \to \exists t \exists u (\exists f \in dom \int^{1} \exists g \in dom \int^{1} ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g))) \land s = t + u))$

Metamath Proof Explorer

Theorem itg2addnclem3

Proof