itg2addnc

Description: Alternate proof of itg2add using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub , which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc , and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017) (Revised by Brendan Leahy, 13-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	itg2addnc	$⊢ φ \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G)$

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		simprr	$⊢ (f \in dom \int^{1} \land (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))) \to x = \int^{1} (f)$
7		itg1cl	$⊢ f \in dom \int^{1} \to \int^{1} (f) \in ℝ$
8	7	adantr	$⊢ (f \in dom \int^{1} \land (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))) \to \int^{1} (f) \in ℝ$
9	6 8	eqeltrd	$⊢ (f \in dom \int^{1} \land (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))) \to x \in ℝ$
10	9	rexlimiva	$⊢ \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f)) \to x \in ℝ$
11	10	abssi	$⊢ \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \subseteq ℝ$
12	11	a1i	$⊢ φ \to \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \subseteq ℝ$
13		i1f0	$⊢ ℝ \times \{0\} \in dom \int^{1}$
14		3nn	$⊢ 3 \in ℕ$
15		nnrp	$⊢ 3 \in ℕ \to 3 \in ℝ^{+}$
16		ne0i	$⊢ 3 \in ℝ^{+} \to ℝ^{+} \neq \emptyset$
17	14 15 16	mp2b	$⊢ ℝ^{+} \neq \emptyset$
18	2	ffvelrnda	$⊢ (φ \land z \in ℝ) \to F (z) \in [0, +∞)$
19		elrege0	$⊢ F (z) \in [0, +∞) \leftrightarrow (F (z) \in ℝ \land 0 \leq F (z))$
20	18 19	sylib	$⊢ (φ \land z \in ℝ) \to (F (z) \in ℝ \land 0 \leq F (z))$
21	20	simprd	$⊢ (φ \land z \in ℝ) \to 0 \leq F (z)$
22	21	ralrimiva	$⊢ φ \to \forall z \in ℝ 0 \leq F (z)$
23		reex	$⊢ ℝ \in V$
24	23	a1i	$⊢ φ \to ℝ \in V$
25		c0ex	$⊢ 0 \in V$
26	25	a1i	$⊢ (φ \land z \in ℝ) \to 0 \in V$
27		eqidd	$⊢ φ \to (z \in ℝ ⟼ 0) = (z \in ℝ ⟼ 0)$
28	2	feqmptd	$⊢ φ \to F = (z \in ℝ ⟼ F (z))$
29	24 26 18 27 28	ofrfval2	$⊢ φ \to ((z \in ℝ ⟼ 0) \leq_{f} F \leftrightarrow \forall z \in ℝ 0 \leq F (z))$
30	22 29	mpbird	$⊢ φ \to (z \in ℝ ⟼ 0) \leq_{f} F$
31	30	ralrimivw	$⊢ φ \to \forall c \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} F$
32		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall c \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} F) \to \exists c \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} F$
33	17 31 32	sylancr	$⊢ φ \to \exists c \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} F$
34		fveq2	$⊢ f = ℝ \times \{0\} \to \int^{1} (f) = \int^{1} (ℝ \times \{0\})$
35		itg10	$⊢ \int^{1} (ℝ \times \{0\}) = 0$
36	34 35	eqtr2di	$⊢ f = ℝ \times \{0\} \to 0 = \int^{1} (f)$
37	36	biantrud	$⊢ f = ℝ \times \{0\} \to (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \leftrightarrow (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land 0 = \int^{1} (f)))$
38		fveq1	$⊢ f = ℝ \times \{0\} \to f (z) = (ℝ \times \{0\}) (z)$
39	25	fvconst2	$⊢ z \in ℝ \to (ℝ \times \{0\}) (z) = 0$
40	38 39	sylan9eq	$⊢ (f = ℝ \times \{0\} \land z \in ℝ) \to f (z) = 0$
41	40	iftrued	$⊢ (f = ℝ \times \{0\} \land z \in ℝ) \to if (f (z) = 0, 0, f (z) + c) = 0$
42	41	mpteq2dva	$⊢ f = ℝ \times \{0\} \to (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) = (z \in ℝ ⟼ 0)$
43	42	breq1d	$⊢ f = ℝ \times \{0\} \to ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \leftrightarrow (z \in ℝ ⟼ 0) \leq_{f} F)$
44	43	rexbidv	$⊢ f = ℝ \times \{0\} \to (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \leftrightarrow \exists c \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} F)$
45	37 44	bitr3d	$⊢ f = ℝ \times \{0\} \to ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land 0 = \int^{1} (f)) \leftrightarrow \exists c \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} F)$
46	45	rspcev	$⊢ (ℝ \times \{0\} \in dom \int^{1} \land \exists c \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} F) \to \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land 0 = \int^{1} (f))$
47	13 33 46	sylancr	$⊢ φ \to \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land 0 = \int^{1} (f))$
48		eqeq1	$⊢ x = 0 \to (x = \int^{1} (f) \leftrightarrow 0 = \int^{1} (f))$
49	48	anbi2d	$⊢ x = 0 \to ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f)) \leftrightarrow (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land 0 = \int^{1} (f)))$
50	49	rexbidv	$⊢ x = 0 \to (\exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f)) \leftrightarrow \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land 0 = \int^{1} (f)))$
51	25 50	elab	$⊢ 0 \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \leftrightarrow \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land 0 = \int^{1} (f))$
52	47 51	sylibr	$⊢ φ \to 0 \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\}$
53	52	ne0d	$⊢ φ \to \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \neq \emptyset$
54		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
55		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F : ℝ ⟶ [0, +∞]$
56	54 55	mpan2	$⊢ F : ℝ ⟶ [0, +∞) \to F : ℝ ⟶ [0, +∞]$
57		eqid	$⊢ \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} = \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\}$
58	57	itg2addnclem	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <)$
59	2 56 58	3syl	$⊢ φ \to \int^{2} (F) = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <)$
60	59 3	eqeltrrd	$⊢ φ \to sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <) \in ℝ$
61		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
62	11 61	sstri	$⊢ \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \subseteq ℝ^{*}$
63		supxrub	$⊢ (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \subseteq ℝ^{} \land b \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\}) \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <)$
64	62 63	mpan	$⊢ b \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <)$
65	64	rgen	$⊢ \forall b \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <)$
66		brralrspcev	$⊢ (sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) \in ℝ \land \forall b \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <)) \to \exists a \in ℝ \forall b \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} b \leq a$
67	60 65 66	sylancl	$⊢ φ \to \exists a \in ℝ \forall b \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} b \leq a$
68		simprr	$⊢ (g \in dom \int^{1} \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))) \to x = \int^{1} (g)$
69		itg1cl	$⊢ g \in dom \int^{1} \to \int^{1} (g) \in ℝ$
70	69	adantr	$⊢ (g \in dom \int^{1} \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))) \to \int^{1} (g) \in ℝ$
71	68 70	eqeltrd	$⊢ (g \in dom \int^{1} \land (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))) \to x \in ℝ$
72	71	rexlimiva	$⊢ \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g)) \to x \in ℝ$
73	72	abssi	$⊢ \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \subseteq ℝ$
74	73	a1i	$⊢ φ \to \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \subseteq ℝ$
75	4	ffvelrnda	$⊢ (φ \land z \in ℝ) \to G (z) \in [0, +∞)$
76		elrege0	$⊢ G (z) \in [0, +∞) \leftrightarrow (G (z) \in ℝ \land 0 \leq G (z))$
77	75 76	sylib	$⊢ (φ \land z \in ℝ) \to (G (z) \in ℝ \land 0 \leq G (z))$
78	77	simprd	$⊢ (φ \land z \in ℝ) \to 0 \leq G (z)$
79	78	ralrimiva	$⊢ φ \to \forall z \in ℝ 0 \leq G (z)$
80	4	feqmptd	$⊢ φ \to G = (z \in ℝ ⟼ G (z))$
81	24 26 75 27 80	ofrfval2	$⊢ φ \to ((z \in ℝ ⟼ 0) \leq_{f} G \leftrightarrow \forall z \in ℝ 0 \leq G (z))$
82	79 81	mpbird	$⊢ φ \to (z \in ℝ ⟼ 0) \leq_{f} G$
83	82	ralrimivw	$⊢ φ \to \forall d \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} G$
84		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall d \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} G) \to \exists d \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} G$
85	17 83 84	sylancr	$⊢ φ \to \exists d \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} G$
86		fveq2	$⊢ g = ℝ \times \{0\} \to \int^{1} (g) = \int^{1} (ℝ \times \{0\})$
87	86 35	eqtr2di	$⊢ g = ℝ \times \{0\} \to 0 = \int^{1} (g)$
88	87	biantrud	$⊢ g = ℝ \times \{0\} \to (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \leftrightarrow (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land 0 = \int^{1} (g)))$
89		fveq1	$⊢ g = ℝ \times \{0\} \to g (z) = (ℝ \times \{0\}) (z)$
90	89 39	sylan9eq	$⊢ (g = ℝ \times \{0\} \land z \in ℝ) \to g (z) = 0$
91	90	iftrued	$⊢ (g = ℝ \times \{0\} \land z \in ℝ) \to if (g (z) = 0, 0, g (z) + d) = 0$
92	91	mpteq2dva	$⊢ g = ℝ \times \{0\} \to (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) = (z \in ℝ ⟼ 0)$
93	92	breq1d	$⊢ g = ℝ \times \{0\} \to ((z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \leftrightarrow (z \in ℝ ⟼ 0) \leq_{f} G)$
94	93	rexbidv	$⊢ g = ℝ \times \{0\} \to (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \leftrightarrow \exists d \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} G)$
95	88 94	bitr3d	$⊢ g = ℝ \times \{0\} \to ((\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land 0 = \int^{1} (g)) \leftrightarrow \exists d \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} G)$
96	95	rspcev	$⊢ (ℝ \times \{0\} \in dom \int^{1} \land \exists d \in ℝ^{+} (z \in ℝ ⟼ 0) \leq_{f} G) \to \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land 0 = \int^{1} (g))$
97	13 85 96	sylancr	$⊢ φ \to \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land 0 = \int^{1} (g))$
98		eqeq1	$⊢ x = 0 \to (x = \int^{1} (g) \leftrightarrow 0 = \int^{1} (g))$
99	98	anbi2d	$⊢ x = 0 \to ((\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g)) \leftrightarrow (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land 0 = \int^{1} (g)))$
100	99	rexbidv	$⊢ x = 0 \to (\exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g)) \leftrightarrow \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land 0 = \int^{1} (g)))$
101	25 100	elab	$⊢ 0 \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \leftrightarrow \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land 0 = \int^{1} (g))$
102	97 101	sylibr	$⊢ φ \to 0 \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}$
103	102	ne0d	$⊢ φ \to \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \neq \emptyset$
104		fss	$⊢ (G : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to G : ℝ ⟶ [0, +∞]$
105	54 104	mpan2	$⊢ G : ℝ ⟶ [0, +∞) \to G : ℝ ⟶ [0, +∞]$
106		eqid	$⊢ \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} = \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}$
107	106	itg2addnclem	$⊢ G : ℝ ⟶ [0, +∞] \to \int^{2} (G) = sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <)$
108	4 105 107	3syl	$⊢ φ \to \int^{2} (G) = sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <)$
109	108 5	eqeltrrd	$⊢ φ \to sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <) \in ℝ$
110	73 61	sstri	$⊢ \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \subseteq ℝ^{*}$
111		supxrub	$⊢ (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \subseteq ℝ^{} \land b \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \to b \leq sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <)$
112	110 111	mpan	$⊢ b \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \to b \leq sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <)$
113	112	rgen	$⊢ \forall b \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b \leq sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <)$
114		brralrspcev	$⊢ (sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <) \in ℝ \land \forall b \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b \leq sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <)) \to \exists a \in ℝ \forall b \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b \leq a$
115	109 113 114	sylancl	$⊢ φ \to \exists a \in ℝ \forall b \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b \leq a$
116		eqid	$⊢ \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} = \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\}$
117	12 53 67 74 103 115 116	supadd	$⊢ φ \to sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ <) = sup (\{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} ℝ <)$
118		supxrre	$⊢ (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \subseteq ℝ \land \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \neq \emptyset \land \exists a \in ℝ \forall b \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} b \leq a) \to sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <) = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ <)$
119	12 53 67 118	syl3anc	$⊢ φ \to sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <) = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ <)$
120	59 119	eqtrd	$⊢ φ \to \int^{2} (F) = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ <)$
121		supxrre	$⊢ (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \subseteq ℝ \land \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \neq \emptyset \land \exists a \in ℝ \forall b \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b \leq a) \to sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <) = sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ <)$
122	74 103 115 121	syl3anc	$⊢ φ \to sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <) = sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ <)$
123	108 122	eqtrd	$⊢ φ \to \int^{2} (G) = sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ <)$
124	120 123	oveq12d	$⊢ φ \to \int^{2} (F) + \int^{2} (G) = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ <)$
125		ge0addcl	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x + y \in [0, +∞)$
126	54 125	sseldi	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x + y \in [0, +∞]$
127	126	adantl	$⊢ (φ \land (x \in [0, +∞) \land y \in [0, +∞))) \to x + y \in [0, +∞]$
128		inidm	$⊢ ℝ \cap ℝ = ℝ$
129	127 2 4 24 24 128	off	$⊢ φ \to (F +_{f} G) : ℝ ⟶ [0, +∞]$
130		eqid	$⊢ \{s \| \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))\} = \{s \| \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))\}$
131	130	itg2addnclem	$⊢ (F +_{f} G) : ℝ ⟶ [0, +∞] \to \int^{2} (F +_{f} G) = sup (\{s \| \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))\} ℝ^{*} <)$
132	129 131	syl	$⊢ φ \to \int^{2} (F +_{f} G) = sup (\{s \| \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))\} ℝ^{*} <)$
133	1 2 3 4 5	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))$
134		simpl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f \in dom \int^{1}$
135		simpr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to g \in dom \int^{1}$
136	134 135	i1fadd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f +_{f} g \in dom \int^{1}$
137	136	ad3antlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land ((\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) \to f +_{f} g \in dom \int^{1}$
138		reeanv	$⊢ \exists c \in ℝ^{+} \exists d \in ℝ^{+} ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G) \leftrightarrow (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land \exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G)$
139	138	biimpri	$⊢ (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land \exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G) \to \exists c \in ℝ^{+} \exists d \in ℝ^{+} ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G)$
140	139	ad2ant2r	$⊢ ((\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))) \to \exists c \in ℝ^{+} \exists d \in ℝ^{+} ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G)$
141		ifcl	$⊢ (c \in ℝ^{+} \land d \in ℝ^{+}) \to if (c \leq d, c, d) \in ℝ^{+}$
142	141	ad2antlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G)) \to if (c \leq d, c, d) \in ℝ^{+}$
143		breq1	$⊢ 0 = if (f (z) = 0, 0, f (z) + c) \to (0 \leq F (z) \leftrightarrow if (f (z) = 0, 0, f (z) + c) \leq F (z))$
144	143	anbi1d	$⊢ 0 = if (f (z) = 0, 0, f (z) + c) \to ((0 \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \leftrightarrow (if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
145	144	imbi1d	$⊢ 0 = if (f (z) = 0, 0, f (z) + c) \to (((0 \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)) \leftrightarrow ((if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)))$
146		breq1	$⊢ f (z) + c = if (f (z) = 0, 0, f (z) + c) \to (f (z) + c \leq F (z) \leftrightarrow if (f (z) = 0, 0, f (z) + c) \leq F (z))$
147	146	anbi1d	$⊢ f (z) + c = if (f (z) = 0, 0, f (z) + c) \to ((f (z) + c \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \leftrightarrow (if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
148	147	imbi1d	$⊢ f (z) + c = if (f (z) = 0, 0, f (z) + c) \to (((f (z) + c \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)) \leftrightarrow ((if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)))$
149		breq1	$⊢ 0 = if (g (z) = 0, 0, g (z) + d) \to (0 \leq G (z) \leftrightarrow if (g (z) = 0, 0, g (z) + d) \leq G (z))$
150	149	anbi2d	$⊢ 0 = if (g (z) = 0, 0, g (z) + d) \to ((0 \leq F (z) \land 0 \leq G (z)) \leftrightarrow (0 \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
151	150	imbi1d	$⊢ 0 = if (g (z) = 0, 0, g (z) + d) \to (((0 \leq F (z) \land 0 \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)) \leftrightarrow ((0 \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)))$
152		breq1	$⊢ g (z) + d = if (g (z) = 0, 0, g (z) + d) \to (g (z) + d \leq G (z) \leftrightarrow if (g (z) = 0, 0, g (z) + d) \leq G (z))$
153	152	anbi2d	$⊢ g (z) + d = if (g (z) = 0, 0, g (z) + d) \to ((0 \leq F (z) \land g (z) + d \leq G (z)) \leftrightarrow (0 \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
154	153	imbi1d	$⊢ g (z) + d = if (g (z) = 0, 0, g (z) + d) \to (((0 \leq F (z) \land g (z) + d \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)) \leftrightarrow ((0 \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)))$
155		oveq12	$⊢ (f (z) = 0 \land g (z) = 0) \to f (z) + g (z) = 0 + 0$
156		00id	$⊢ 0 + 0 = 0$
157	155 156	eqtrdi	$⊢ (f (z) = 0 \land g (z) = 0) \to f (z) + g (z) = 0$
158	157	iftrued	$⊢ (f (z) = 0 \land g (z) = 0) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) = 0$
159	158	adantll	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) = 0) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) = 0$
160		simpll	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to φ$
161	19	simplbi	$⊢ F (z) \in [0, +∞) \to F (z) \in ℝ$
162	18 161	syl	$⊢ (φ \land z \in ℝ) \to F (z) \in ℝ$
163	76	simplbi	$⊢ G (z) \in [0, +∞) \to G (z) \in ℝ$
164	75 163	syl	$⊢ (φ \land z \in ℝ) \to G (z) \in ℝ$
165	162 164 21 78	addge0d	$⊢ (φ \land z \in ℝ) \to 0 \leq F (z) + G (z)$
166	160 165	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to 0 \leq F (z) + G (z)$
167	166	ad2antrr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) = 0) \to 0 \leq F (z) + G (z)$
168	159 167	eqbrtrd	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) = 0) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)$
169	168	a1d	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) = 0) \to ((0 \leq F (z) \land 0 \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
170	166	ad2antrr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) + d \leq G (z)) \to 0 \leq F (z) + G (z)$
171		oveq1	$⊢ f (z) = 0 \to f (z) + g (z) = 0 + g (z)$
172		simplrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to g \in dom \int^{1}$
173		i1ff	$⊢ g \in dom \int^{1} \to g : ℝ ⟶ ℝ$
174	173	ffvelrnda	$⊢ (g \in dom \int^{1} \land z \in ℝ) \to g (z) \in ℝ$
175	172 174	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to g (z) \in ℝ$
176	175	recnd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to g (z) \in ℂ$
177	176	addid2d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to 0 + g (z) = g (z)$
178	171 177	sylan9eqr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \to f (z) + g (z) = g (z)$
179	178	oveq1d	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \to f (z) + g (z) + if (c \leq d, c, d) = g (z) + if (c \leq d, c, d)$
180	179	adantr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) + d \leq G (z)) \to f (z) + g (z) + if (c \leq d, c, d) = g (z) + if (c \leq d, c, d)$
181	141	rpred	$⊢ (c \in ℝ^{+} \land d \in ℝ^{+}) \to if (c \leq d, c, d) \in ℝ$
182	181	ad2antlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to if (c \leq d, c, d) \in ℝ$
183	175 182	readdcld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to g (z) + if (c \leq d, c, d) \in ℝ$
184	183	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) + d \leq G (z)) \to g (z) + if (c \leq d, c, d) \in ℝ$
185	160 164	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to G (z) \in ℝ$
186	185	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) + d \leq G (z)) \to G (z) \in ℝ$
187	160 162	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to F (z) \in ℝ$
188	187 185	readdcld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to F (z) + G (z) \in ℝ$
189	188	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) + d \leq G (z)) \to F (z) + G (z) \in ℝ$
190		simplrr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to d \in ℝ^{+}$
191	190	rpred	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to d \in ℝ$
192		rpre	$⊢ c \in ℝ^{+} \to c \in ℝ$
193		rpre	$⊢ d \in ℝ^{+} \to d \in ℝ$
194		min2	$⊢ (c \in ℝ \land d \in ℝ) \to if (c \leq d, c, d) \leq d$
195	192 193 194	syl2an	$⊢ (c \in ℝ^{+} \land d \in ℝ^{+}) \to if (c \leq d, c, d) \leq d$
196	195	ad2antlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to if (c \leq d, c, d) \leq d$
197	182 191 175 196	leadd2dd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to g (z) + if (c \leq d, c, d) \leq g (z) + d$
198	175 191	readdcld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to g (z) + d \in ℝ$
199		letr	$⊢ (g (z) + if (c \leq d, c, d) \in ℝ \land g (z) + d \in ℝ \land G (z) \in ℝ) \to ((g (z) + if (c \leq d, c, d) \leq g (z) + d \land g (z) + d \leq G (z)) \to g (z) + if (c \leq d, c, d) \leq G (z))$
200	183 198 185 199	syl3anc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to ((g (z) + if (c \leq d, c, d) \leq g (z) + d \land g (z) + d \leq G (z)) \to g (z) + if (c \leq d, c, d) \leq G (z))$
201	197 200	mpand	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to (g (z) + d \leq G (z) \to g (z) + if (c \leq d, c, d) \leq G (z))$
202	201	imp	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) + d \leq G (z)) \to g (z) + if (c \leq d, c, d) \leq G (z)$
203	164 162	addge02d	$⊢ (φ \land z \in ℝ) \to (0 \leq F (z) \leftrightarrow G (z) \leq F (z) + G (z))$
204	21 203	mpbid	$⊢ (φ \land z \in ℝ) \to G (z) \leq F (z) + G (z)$
205	160 204	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to G (z) \leq F (z) + G (z)$
206	205	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) + d \leq G (z)) \to G (z) \leq F (z) + G (z)$
207	184 186 189 202 206	letrd	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) + d \leq G (z)) \to g (z) + if (c \leq d, c, d) \leq F (z) + G (z)$
208	207	adantlr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) + d \leq G (z)) \to g (z) + if (c \leq d, c, d) \leq F (z) + G (z)$
209	180 208	eqbrtrd	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) + d \leq G (z)) \to f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z)$
210		breq1	$⊢ 0 = if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \to (0 \leq F (z) + G (z) \leftrightarrow if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
211		breq1	$⊢ f (z) + g (z) + if (c \leq d, c, d) = if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \to (f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z) \leftrightarrow if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
212	210 211	ifboth	$⊢ (0 \leq F (z) + G (z) \land f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)$
213	170 209 212	syl2anc	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land g (z) + d \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)$
214	213	ex	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \to (g (z) + d \leq G (z) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
215	214	adantld	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \to ((0 \leq F (z) \land g (z) + d \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
216	215	adantr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \land \neg g (z) = 0) \to ((0 \leq F (z) \land g (z) + d \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
217	151 154 169 216	ifbothda	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) = 0) \to ((0 \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
218	149	anbi2d	$⊢ 0 = if (g (z) = 0, 0, g (z) + d) \to ((f (z) + c \leq F (z) \land 0 \leq G (z)) \leftrightarrow (f (z) + c \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
219	218	imbi1d	$⊢ 0 = if (g (z) = 0, 0, g (z) + d) \to (((f (z) + c \leq F (z) \land 0 \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)) \leftrightarrow ((f (z) + c \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)))$
220	152	anbi2d	$⊢ g (z) + d = if (g (z) = 0, 0, g (z) + d) \to ((f (z) + c \leq F (z) \land g (z) + d \leq G (z)) \leftrightarrow (f (z) + c \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
221	220	imbi1d	$⊢ g (z) + d = if (g (z) = 0, 0, g (z) + d) \to (((f (z) + c \leq F (z) \land g (z) + d \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)) \leftrightarrow ((f (z) + c \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)))$
222	166	ad2antrr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) = 0) \land f (z) + c \leq F (z)) \to 0 \leq F (z) + G (z)$
223		oveq2	$⊢ g (z) = 0 \to f (z) + g (z) = f (z) + 0$
224		simplrl	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to f \in dom \int^{1}$
225		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
226	225	ffvelrnda	$⊢ (f \in dom \int^{1} \land z \in ℝ) \to f (z) \in ℝ$
227	224 226	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) \in ℝ$
228	227	recnd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) \in ℂ$
229	228	addid1d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) + 0 = f (z)$
230	223 229	sylan9eqr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) = 0) \to f (z) + g (z) = f (z)$
231	230	oveq1d	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) = 0) \to f (z) + g (z) + if (c \leq d, c, d) = f (z) + if (c \leq d, c, d)$
232	231	adantr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) = 0) \land f (z) + c \leq F (z)) \to f (z) + g (z) + if (c \leq d, c, d) = f (z) + if (c \leq d, c, d)$
233	227 182	readdcld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) + if (c \leq d, c, d) \in ℝ$
234	233	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) + c \leq F (z)) \to f (z) + if (c \leq d, c, d) \in ℝ$
235	187	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) + c \leq F (z)) \to F (z) \in ℝ$
236	188	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) + c \leq F (z)) \to F (z) + G (z) \in ℝ$
237		simplrl	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to c \in ℝ^{+}$
238	237	rpred	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to c \in ℝ$
239		min1	$⊢ (c \in ℝ \land d \in ℝ) \to if (c \leq d, c, d) \leq c$
240	192 193 239	syl2an	$⊢ (c \in ℝ^{+} \land d \in ℝ^{+}) \to if (c \leq d, c, d) \leq c$
241	240	ad2antlr	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to if (c \leq d, c, d) \leq c$
242	182 238 227 241	leadd2dd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) + if (c \leq d, c, d) \leq f (z) + c$
243	227 238	readdcld	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) + c \in ℝ$
244		letr	$⊢ (f (z) + if (c \leq d, c, d) \in ℝ \land f (z) + c \in ℝ \land F (z) \in ℝ) \to ((f (z) + if (c \leq d, c, d) \leq f (z) + c \land f (z) + c \leq F (z)) \to f (z) + if (c \leq d, c, d) \leq F (z))$
245	233 243 187 244	syl3anc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to ((f (z) + if (c \leq d, c, d) \leq f (z) + c \land f (z) + c \leq F (z)) \to f (z) + if (c \leq d, c, d) \leq F (z))$
246	242 245	mpand	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to (f (z) + c \leq F (z) \to f (z) + if (c \leq d, c, d) \leq F (z))$
247	246	imp	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) + c \leq F (z)) \to f (z) + if (c \leq d, c, d) \leq F (z)$
248	162 164	addge01d	$⊢ (φ \land z \in ℝ) \to (0 \leq G (z) \leftrightarrow F (z) \leq F (z) + G (z))$
249	78 248	mpbid	$⊢ (φ \land z \in ℝ) \to F (z) \leq F (z) + G (z)$
250	160 249	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to F (z) \leq F (z) + G (z)$
251	250	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) + c \leq F (z)) \to F (z) \leq F (z) + G (z)$
252	234 235 236 247 251	letrd	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land f (z) + c \leq F (z)) \to f (z) + if (c \leq d, c, d) \leq F (z) + G (z)$
253	252	adantlr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) = 0) \land f (z) + c \leq F (z)) \to f (z) + if (c \leq d, c, d) \leq F (z) + G (z)$
254	232 253	eqbrtrd	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) = 0) \land f (z) + c \leq F (z)) \to f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z)$
255	222 254 212	syl2anc	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) = 0) \land f (z) + c \leq F (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)$
256	255	ex	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land g (z) = 0) \to (f (z) + c \leq F (z) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
257	256	adantlr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land \neg f (z) = 0) \land g (z) = 0) \to (f (z) + c \leq F (z) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
258	257	adantrd	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land \neg f (z) = 0) \land g (z) = 0) \to ((f (z) + c \leq F (z) \land 0 \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
259	166	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land (f (z) + c \leq F (z) \land g (z) + d \leq G (z))) \to 0 \leq F (z) + G (z)$
260	182	recnd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to if (c \leq d, c, d) \in ℂ$
261	228 176 260	addassd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) + g (z) + if (c \leq d, c, d) = f (z) + g (z) + if (c \leq d, c, d)$
262	261	adantr	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land (f (z) + c \leq F (z) \land g (z) + d \leq G (z))) \to f (z) + g (z) + if (c \leq d, c, d) = f (z) + g (z) + if (c \leq d, c, d)$
263	227 237	ltaddrpd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) < f (z) + c$
264	227 243 263	ltled	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) \leq f (z) + c$
265		letr	$⊢ (f (z) \in ℝ \land f (z) + c \in ℝ \land F (z) \in ℝ) \to ((f (z) \leq f (z) + c \land f (z) + c \leq F (z)) \to f (z) \leq F (z))$
266	227 243 187 265	syl3anc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to ((f (z) \leq f (z) + c \land f (z) + c \leq F (z)) \to f (z) \leq F (z))$
267	264 266	mpand	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to (f (z) + c \leq F (z) \to f (z) \leq F (z))$
268		le2add	$⊢ ((f (z) \in ℝ \land g (z) + if (c \leq d, c, d) \in ℝ) \land (F (z) \in ℝ \land G (z) \in ℝ)) \to ((f (z) \leq F (z) \land g (z) + if (c \leq d, c, d) \leq G (z)) \to f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z))$
269	227 183 187 185 268	syl22anc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to ((f (z) \leq F (z) \land g (z) + if (c \leq d, c, d) \leq G (z)) \to f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z))$
270	267 201 269	syl2and	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to ((f (z) + c \leq F (z) \land g (z) + d \leq G (z)) \to f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z))$
271	270	imp	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land (f (z) + c \leq F (z) \land g (z) + d \leq G (z))) \to f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z)$
272	262 271	eqbrtrd	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land (f (z) + c \leq F (z) \land g (z) + d \leq G (z))) \to f (z) + g (z) + if (c \leq d, c, d) \leq F (z) + G (z)$
273	259 272 212	syl2anc	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land (f (z) + c \leq F (z) \land g (z) + d \leq G (z))) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z)$
274	273	ex	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to ((f (z) + c \leq F (z) \land g (z) + d \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
275	274	ad2antrr	$⊢ (((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land \neg f (z) = 0) \land \neg g (z) = 0) \to ((f (z) + c \leq F (z) \land g (z) + d \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
276	219 221 258 275	ifbothda	$⊢ ((((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \land \neg f (z) = 0) \to ((f (z) + c \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
277	145 148 217 276	ifbothda	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to ((if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
278	277	ralimdva	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to (\forall z \in ℝ (if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \to \forall z \in ℝ if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
279		ovex	$⊢ f (z) + c \in V$
280	25 279	ifex	$⊢ if (f (z) = 0, 0, f (z) + c) \in V$
281	280	a1i	$⊢ (φ \land z \in ℝ) \to if (f (z) = 0, 0, f (z) + c) \in V$
282		eqidd	$⊢ φ \to (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) = (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c))$
283	24 281 18 282 28	ofrfval2	$⊢ φ \to ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \leftrightarrow \forall z \in ℝ if (f (z) = 0, 0, f (z) + c) \leq F (z))$
284		ovex	$⊢ g (z) + d \in V$
285	25 284	ifex	$⊢ if (g (z) = 0, 0, g (z) + d) \in V$
286	285	a1i	$⊢ (φ \land z \in ℝ) \to if (g (z) = 0, 0, g (z) + d) \in V$
287		eqidd	$⊢ φ \to (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) = (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d))$
288	24 286 75 287 80	ofrfval2	$⊢ φ \to ((z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \leftrightarrow \forall z \in ℝ if (g (z) = 0, 0, g (z) + d) \leq G (z))$
289	283 288	anbi12d	$⊢ φ \to (((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G) \leftrightarrow (\forall z \in ℝ if (f (z) = 0, 0, f (z) + c) \leq F (z) \land \forall z \in ℝ if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
290		r19.26	$⊢ \forall z \in ℝ (if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)) \leftrightarrow (\forall z \in ℝ if (f (z) = 0, 0, f (z) + c) \leq F (z) \land \forall z \in ℝ if (g (z) = 0, 0, g (z) + d) \leq G (z))$
291	289 290	bitr4di	$⊢ φ \to (((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G) \leftrightarrow \forall z \in ℝ (if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
292	291	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to (((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G) \leftrightarrow \forall z \in ℝ (if (f (z) = 0, 0, f (z) + c) \leq F (z) \land if (g (z) = 0, 0, g (z) + d) \leq G (z)))$
293	23	a1i	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to ℝ \in V$
294		ovex	$⊢ f (z) + g (z) + if (c \leq d, c, d) \in V$
295	25 294	ifex	$⊢ if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \in V$
296	295	a1i	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \in V$
297		ovexd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to F (z) + G (z) \in V$
298	225	ffnd	$⊢ f \in dom \int^{1} \to f Fn ℝ$
299	298	adantr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f Fn ℝ$
300	299	ad2antlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to f Fn ℝ$
301	173	ffnd	$⊢ g \in dom \int^{1} \to g Fn ℝ$
302	301	adantl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to g Fn ℝ$
303	302	ad2antlr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to g Fn ℝ$
304		eqidd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to f (z) = f (z)$
305		eqidd	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to g (z) = g (z)$
306	300 303 293 293 128 304 305	ofval	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to (f +_{f} g) (z) = f (z) + g (z)$
307	306	eqeq1d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to ((f +_{f} g) (z) = 0 \leftrightarrow f (z) + g (z) = 0)$
308	306	oveq1d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to (f +_{f} g) (z) + if (c \leq d, c, d) = f (z) + g (z) + if (c \leq d, c, d)$
309	307 308	ifbieq2d	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land z \in ℝ) \to if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d)) = if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d))$
310	309	mpteq2dva	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d))) = (z \in ℝ ⟼ if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)))$
311	2	ffnd	$⊢ φ \to F Fn ℝ$
312	4	ffnd	$⊢ φ \to G Fn ℝ$
313		eqidd	$⊢ (φ \land z \in ℝ) \to F (z) = F (z)$
314		eqidd	$⊢ (φ \land z \in ℝ) \to G (z) = G (z)$
315	311 312 24 24 128 313 314	offval	$⊢ φ \to F +_{f} G = (z \in ℝ ⟼ F (z) + G (z))$
316	315	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to F +_{f} G = (z \in ℝ ⟼ F (z) + G (z))$
317	293 296 297 310 316	ofrfval2	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to ((z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d))) \leq_{f} (F +_{f} G) \leftrightarrow \forall z \in ℝ if (f (z) + g (z) = 0, 0, f (z) + g (z) + if (c \leq d, c, d)) \leq F (z) + G (z))$
318	278 292 317	3imtr4d	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to (((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G) \to (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d))) \leq_{f} (F +_{f} G))$
319	318	imp	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G)) \to (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d))) \leq_{f} (F +_{f} G)$
320		oveq2	$⊢ y = if (c \leq d, c, d) \to (f +_{f} g) (z) + y = (f +_{f} g) (z) + if (c \leq d, c, d)$
321	320	ifeq2d	$⊢ y = if (c \leq d, c, d) \to if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y) = if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d))$
322	321	mpteq2dv	$⊢ y = if (c \leq d, c, d) \to (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) = (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d)))$
323	322	breq1d	$⊢ y = if (c \leq d, c, d) \to ((z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G) \leftrightarrow (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d))) \leq_{f} (F +_{f} G))$
324	323	rspcev	$⊢ (if (c \leq d, c, d) \in ℝ^{+} \land (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + if (c \leq d, c, d))) \leq_{f} (F +_{f} G)) \to \exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G)$
325	142 319 324	syl2anc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G)) \to \exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G)$
326	325	ex	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to (((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G) \to \exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G))$
327	326	rexlimdvva	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to (\exists c \in ℝ^{+} \exists d \in ℝ^{+} ((z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G) \to \exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G))$
328	140 327	syl5	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \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))) \to \exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G))$
329	328	a1dd	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \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))) \to (s = t + u \to \exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G)))$
330	329	imp31	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land ((\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) \to \exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G)$
331		oveq12	$⊢ (t = \int^{1} (f) \land u = \int^{1} (g)) \to t + u = \int^{1} (f) + \int^{1} (g)$
332	331	ad2ant2l	$⊢ ((\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))) \to t + u = \int^{1} (f) + \int^{1} (g)$
333	134 135	itg1add	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \int^{1} (f +_{f} g) = \int^{1} (f) + \int^{1} (g)$
334	333	eqcomd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to \int^{1} (f) + \int^{1} (g) = \int^{1} (f +_{f} g)$
335	334	adantl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to \int^{1} (f) + \int^{1} (g) = \int^{1} (f +_{f} g)$
336	332 335	sylan9eqr	$⊢ ((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land ((\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)))) \to t + u = \int^{1} (f +_{f} g)$
337		eqtr	$⊢ (s = t + u \land t + u = \int^{1} (f +_{f} g)) \to s = \int^{1} (f +_{f} g)$
338	337	ancoms	$⊢ (t + u = \int^{1} (f +_{f} g) \land s = t + u) \to s = \int^{1} (f +_{f} g)$
339	336 338	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land ((\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) \to s = \int^{1} (f +_{f} g)$
340		fveq1	$⊢ h = f +_{f} g \to h (z) = (f +_{f} g) (z)$
341	340	eqeq1d	$⊢ h = f +_{f} g \to (h (z) = 0 \leftrightarrow (f +_{f} g) (z) = 0)$
342	340	oveq1d	$⊢ h = f +_{f} g \to h (z) + y = (f +_{f} g) (z) + y$
343	341 342	ifbieq2d	$⊢ h = f +_{f} g \to if (h (z) = 0, 0, h (z) + y) = if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)$
344	343	mpteq2dv	$⊢ h = f +_{f} g \to (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) = (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y))$
345	344	breq1d	$⊢ h = f +_{f} g \to ((z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \leftrightarrow (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G))$
346	345	rexbidv	$⊢ h = f +_{f} g \to (\exists y \in ℝ^{+} (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \leftrightarrow \exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G))$
347		fveq2	$⊢ h = f +_{f} g \to \int^{1} (h) = \int^{1} (f +_{f} g)$
348	347	eqeq2d	$⊢ h = f +_{f} g \to (s = \int^{1} (h) \leftrightarrow s = \int^{1} (f +_{f} g))$
349	346 348	anbi12d	$⊢ h = f +_{f} g \to ((\exists y \in ℝ^{+} (z \in ℝ ⟼ if (h (z) = 0, 0, h (z) + y)) \leq_{f} (F +_{f} G) \land s = \int^{1} (h)) \leftrightarrow (\exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G) \land s = \int^{1} (f +_{f} g)))$
350	349	rspcev	$⊢ (f +_{f} g \in dom \int^{1} \land (\exists y \in ℝ^{+} (z \in ℝ ⟼ if ((f +_{f} g) (z) = 0, 0, (f +_{f} g) (z) + y)) \leq_{f} (F +_{f} G) \land s = \int^{1} (f +_{f} g))) \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))$
351	137 330 339 350	syl12anc	$⊢ (((φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \land ((\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) \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))$
352	351	exp31	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \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))) \to (s = t + u \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))))$
353	352	rexlimdvva	$⊢ φ \to (\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))) \to (s = t + u \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))))$
354	353	impd	$⊢ φ \to ((\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) \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)))$
355	354	exlimdvv	$⊢ φ \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) \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)))$
356	133 355	impbid	$⊢ φ \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)) \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))$
357		eqeq1	$⊢ x = t \to (x = \int^{1} (f) \leftrightarrow t = \int^{1} (f))$
358	357	anbi2d	$⊢ x = t \to ((\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f)) \leftrightarrow (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)))$
359	358	rexbidv	$⊢ x = t \to (\exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f)) \leftrightarrow \exists f \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)))$
360	359	rexab	$⊢ \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u \leftrightarrow \exists t (\exists f \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 u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u)$
361		eqeq1	$⊢ x = u \to (x = \int^{1} (g) \leftrightarrow u = \int^{1} (g))$
362	361	anbi2d	$⊢ x = u \to ((\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g)) \leftrightarrow (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g)))$
363	362	rexbidv	$⊢ x = u \to (\exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g)) \leftrightarrow \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g)))$
364	363	rexab	$⊢ \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u \leftrightarrow \exists u (\exists g \in dom \int^{1} (\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)$
365	364	anbi2i	$⊢ (\exists f \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 u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u) \leftrightarrow (\exists f \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 u (\exists g \in dom \int^{1} (\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))$
366		19.42v	$⊢ \exists u (\exists f \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 g \in dom \int^{1} (\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 c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land \exists u (\exists g \in dom \int^{1} (\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))$
367		reeanv	$⊢ \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))) \leftrightarrow (\exists f \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 g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land u = \int^{1} (g)))$
368	367	anbi1i	$⊢ (\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 c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land \exists g \in dom \int^{1} (\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)$
369		anass	$⊢ ((\exists f \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 g \in dom \int^{1} (\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 c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land t = \int^{1} (f)) \land (\exists g \in dom \int^{1} (\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))$
370	368 369	bitr2i	$⊢ (\exists f \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 g \in dom \int^{1} (\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)$
371	370	exbii	$⊢ \exists u (\exists f \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 g \in dom \int^{1} (\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)$
372	365 366 371	3bitr2i	$⊢ (\exists f \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 u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} 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)$
373	372	exbii	$⊢ \exists t (\exists f \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 u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} 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)$
374	360 373	bitri	$⊢ \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} 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)$
375	356 374	bitr4di	$⊢ φ \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)) \leftrightarrow \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u)$
376	375	abbidv	$⊢ φ \to \{s \| \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))\} = \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\}$
377	376	supeq1d	$⊢ φ \to sup (\{s \| \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))\} ℝ^{} <) = sup (\{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} ℝ^{} <)$
378		simpr	$⊢ ((t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \land s = t + u) \to s = t + u$
379	11	sseli	$⊢ t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \to t \in ℝ$
380	379	ad2antrr	$⊢ ((t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \land s = t + u) \to t \in ℝ$
381	73	sseli	$⊢ u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \to u \in ℝ$
382	381	ad2antlr	$⊢ ((t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \land s = t + u) \to u \in ℝ$
383	380 382	readdcld	$⊢ ((t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \land s = t + u) \to t + u \in ℝ$
384	378 383	eqeltrd	$⊢ ((t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \land s = t + u) \to s \in ℝ$
385	384	ex	$⊢ (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \to (s = t + u \to s \in ℝ)$
386	385	rexlimivv	$⊢ \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u \to s \in ℝ$
387	386	abssi	$⊢ \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} \subseteq ℝ$
388	387	a1i	$⊢ φ \to \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} \subseteq ℝ$
389	156	eqcomi	$⊢ 0 = 0 + 0$
390		rspceov	$⊢ (0 \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land 0 \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \land 0 = 0 + 0) \to \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} 0 = t + u$
391	389 390	mp3an3	$⊢ (0 \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land 0 \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \to \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} 0 = t + u$
392	52 102 391	syl2anc	$⊢ φ \to \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} 0 = t + u$
393		eqeq1	$⊢ s = 0 \to (s = t + u \leftrightarrow 0 = t + u)$
394	393	2rexbidv	$⊢ s = 0 \to (\exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u \leftrightarrow \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} 0 = t + u)$
395	25 394	spcev	$⊢ \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} 0 = t + u \to \exists s \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u$
396	392 395	syl	$⊢ φ \to \exists s \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u$
397		abn0	$⊢ \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} \neq \emptyset \leftrightarrow \exists s \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u$
398	396 397	sylibr	$⊢ φ \to \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} \neq \emptyset$
399	60 109	readdcld	$⊢ φ \to sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <) \in ℝ$
400		simpr	$⊢ ((φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \land b = t + u) \to b = t + u$
401	379	ad2antrl	$⊢ (φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \to t \in ℝ$
402	381	ad2antll	$⊢ (φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \to u \in ℝ$
403	60	adantr	$⊢ (φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \to sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <) \in ℝ$
404	109	adantr	$⊢ (φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \to sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <) \in ℝ$
405		supxrub	$⊢ (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \subseteq ℝ^{} \land t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\}) \to t \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <)$
406	62 405	mpan	$⊢ t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \to t \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <)$
407	406	ad2antrl	$⊢ (φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \to t \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{*} <)$
408		supxrub	$⊢ (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \subseteq ℝ^{} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\}) \to u \leq sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <)$
409	110 408	mpan	$⊢ u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} \to u \leq sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <)$
410	409	ad2antll	$⊢ (φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \to u \leq sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{*} <)$
411	401 402 403 404 407 410	le2addd	$⊢ (φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \to t + u \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <)$
412	411	adantr	$⊢ ((φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \land b = t + u) \to t + u \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <)$
413	400 412	eqbrtrd	$⊢ ((φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \land b = t + u) \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <)$
414	413	ex	$⊢ (φ \land (t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \land u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\})) \to (b = t + u \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <))$
415	414	rexlimdvva	$⊢ φ \to (\exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b = t + u \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <))$
416	415	alrimiv	$⊢ φ \to \forall b (\exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b = t + u \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <))$
417		breq2	$⊢ a = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <) \to (b \leq a \leftrightarrow b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <))$
418	417	ralbidv	$⊢ a = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <) \to (\forall b \in \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} b \leq a \leftrightarrow \forall b \in \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <))$
419		eqeq1	$⊢ s = b \to (s = t + u \leftrightarrow b = t + u)$
420	419	2rexbidv	$⊢ s = b \to (\exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u \leftrightarrow \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b = t + u)$
421	420	ralab	$⊢ \forall b \in \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <) \leftrightarrow \forall b (\exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b = t + u \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <))$
422	418 421	bitrdi	$⊢ a = sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <) \to (\forall b \in \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} b \leq a \leftrightarrow \forall b (\exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b = t + u \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <)))$
423	422	rspcev	$⊢ (sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <) \in ℝ \land \forall b (\exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} b = t + u \to b \leq sup (\{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} ℝ^{} <) + sup (\{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} ℝ^{} <))) \to \exists a \in ℝ \forall b \in \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} b \leq a$
424	399 416 423	syl2anc	$⊢ φ \to \exists a \in ℝ \forall b \in \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} b \leq a$
425		supxrre	$⊢ (\{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} \subseteq ℝ \land \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} \neq \emptyset \land \exists a \in ℝ \forall b \in \{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} b \leq a) \to sup (\{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} ℝ^{*} <) = sup (\{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} ℝ <)$
426	388 398 424 425	syl3anc	$⊢ φ \to sup (\{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} ℝ^{*} <) = sup (\{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} ℝ <)$
427	132 377 426	3eqtrd	$⊢ φ \to \int^{2} (F +_{f} G) = sup (\{s \| \exists t \in \{x \| \exists f \in dom \int^{1} (\exists c \in ℝ^{+} (z \in ℝ ⟼ if (f (z) = 0, 0, f (z) + c)) \leq_{f} F \land x = \int^{1} (f))\} \exists u \in \{x \| \exists g \in dom \int^{1} (\exists d \in ℝ^{+} (z \in ℝ ⟼ if (g (z) = 0, 0, g (z) + d)) \leq_{f} G \land x = \int^{1} (g))\} s = t + u\} ℝ <)$
428	117 124 427	3eqtr4rd	$⊢ φ \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G)$

Metamath Proof Explorer

Theorem itg2addnc

Proof