supadd

Description: The supremum function distributes over addition in a sense similar to that in supmul . (Contributed by Brendan Leahy, 26-Sep-2017)

	Ref	Expression
Hypotheses	supadd.a1	$⊢ φ \to A \subseteq ℝ$
	supadd.a2	$⊢ φ \to A \neq \emptyset$
	supadd.a3	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
	supadd.b1	$⊢ φ \to B \subseteq ℝ$
	supadd.b2	$⊢ φ \to B \neq \emptyset$
	supadd.b3	$⊢ φ \to \exists x \in ℝ \forall y \in B y \leq x$
	supadd.c	$⊢ C = \{z \| \exists v \in A \exists b \in B z = v + b\}$
Assertion	supadd	$⊢ φ \to sup (A ℝ <) + sup (B ℝ <) = sup (C ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		supadd.a1	$⊢ φ \to A \subseteq ℝ$
2		supadd.a2	$⊢ φ \to A \neq \emptyset$
3		supadd.a3	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
4		supadd.b1	$⊢ φ \to B \subseteq ℝ$
5		supadd.b2	$⊢ φ \to B \neq \emptyset$
6		supadd.b3	$⊢ φ \to \exists x \in ℝ \forall y \in B y \leq x$
7		supadd.c	$⊢ C = \{z \| \exists v \in A \exists b \in B z = v + b\}$
8	4 5 6	suprcld	$⊢ φ \to sup (B ℝ <) \in ℝ$
9		eqid	$⊢ \{z \| \exists a \in A z = a + sup (B ℝ <)\} = \{z \| \exists a \in A z = a + sup (B ℝ <)\}$
10	1 2 3 8 9	supaddc	$⊢ φ \to sup (A ℝ <) + sup (B ℝ <) = sup (\{z \| \exists a \in A z = a + sup (B ℝ <)\} ℝ <)$
11	1	sselda	$⊢ (φ \land a \in A) \to a \in ℝ$
12	11	recnd	$⊢ (φ \land a \in A) \to a \in ℂ$
13	8	adantr	$⊢ (φ \land a \in A) \to sup (B ℝ <) \in ℝ$
14	13	recnd	$⊢ (φ \land a \in A) \to sup (B ℝ <) \in ℂ$
15	12 14	addcomd	$⊢ (φ \land a \in A) \to a + sup (B ℝ <) = sup (B ℝ <) + a$
16	15	eqeq2d	$⊢ (φ \land a \in A) \to (z = a + sup (B ℝ <) \leftrightarrow z = sup (B ℝ <) + a)$
17	16	rexbidva	$⊢ φ \to (\exists a \in A z = a + sup (B ℝ <) \leftrightarrow \exists a \in A z = sup (B ℝ <) + a)$
18	17	abbidv	$⊢ φ \to \{z \| \exists a \in A z = a + sup (B ℝ <)\} = \{z \| \exists a \in A z = sup (B ℝ <) + a\}$
19	18	supeq1d	$⊢ φ \to sup (\{z \| \exists a \in A z = a + sup (B ℝ <)\} ℝ <) = sup (\{z \| \exists a \in A z = sup (B ℝ <) + a\} ℝ <)$
20	10 19	eqtrd	$⊢ φ \to sup (A ℝ <) + sup (B ℝ <) = sup (\{z \| \exists a \in A z = sup (B ℝ <) + a\} ℝ <)$
21		vex	$⊢ w \in V$
22		eqeq1	$⊢ z = w \to (z = sup (B ℝ <) + a \leftrightarrow w = sup (B ℝ <) + a)$
23	22	rexbidv	$⊢ z = w \to (\exists a \in A z = sup (B ℝ <) + a \leftrightarrow \exists a \in A w = sup (B ℝ <) + a)$
24	21 23	elab	$⊢ w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} \leftrightarrow \exists a \in A w = sup (B ℝ <) + a$
25	4	adantr	$⊢ (φ \land a \in A) \to B \subseteq ℝ$
26	5	adantr	$⊢ (φ \land a \in A) \to B \neq \emptyset$
27	6	adantr	$⊢ (φ \land a \in A) \to \exists x \in ℝ \forall y \in B y \leq x$
28		eqid	$⊢ \{z \| \exists b \in B z = b + a\} = \{z \| \exists b \in B z = b + a\}$
29	25 26 27 11 28	supaddc	$⊢ (φ \land a \in A) \to sup (B ℝ <) + a = sup (\{z \| \exists b \in B z = b + a\} ℝ <)$
30	4	sselda	$⊢ (φ \land b \in B) \to b \in ℝ$
31	30	adantlr	$⊢ ((φ \land a \in A) \land b \in B) \to b \in ℝ$
32	31	recnd	$⊢ ((φ \land a \in A) \land b \in B) \to b \in ℂ$
33	11	adantr	$⊢ ((φ \land a \in A) \land b \in B) \to a \in ℝ$
34	33	recnd	$⊢ ((φ \land a \in A) \land b \in B) \to a \in ℂ$
35	32 34	addcomd	$⊢ ((φ \land a \in A) \land b \in B) \to b + a = a + b$
36	35	eqeq2d	$⊢ ((φ \land a \in A) \land b \in B) \to (z = b + a \leftrightarrow z = a + b)$
37	36	rexbidva	$⊢ (φ \land a \in A) \to (\exists b \in B z = b + a \leftrightarrow \exists b \in B z = a + b)$
38	37	abbidv	$⊢ (φ \land a \in A) \to \{z \| \exists b \in B z = b + a\} = \{z \| \exists b \in B z = a + b\}$
39	38	supeq1d	$⊢ (φ \land a \in A) \to sup (\{z \| \exists b \in B z = b + a\} ℝ <) = sup (\{z \| \exists b \in B z = a + b\} ℝ <)$
40	29 39	eqtrd	$⊢ (φ \land a \in A) \to sup (B ℝ <) + a = sup (\{z \| \exists b \in B z = a + b\} ℝ <)$
41		eqeq1	$⊢ z = w \to (z = a + b \leftrightarrow w = a + b)$
42	41	rexbidv	$⊢ z = w \to (\exists b \in B z = a + b \leftrightarrow \exists b \in B w = a + b)$
43	21 42	elab	$⊢ w \in \{z \| \exists b \in B z = a + b\} \leftrightarrow \exists b \in B w = a + b$
44		rspe	$⊢ (a \in A \land \exists b \in B w = a + b) \to \exists a \in A \exists b \in B w = a + b$
45		oveq1	$⊢ v = a \to v + b = a + b$
46	45	eqeq2d	$⊢ v = a \to (z = v + b \leftrightarrow z = a + b)$
47	46	rexbidv	$⊢ v = a \to (\exists b \in B z = v + b \leftrightarrow \exists b \in B z = a + b)$
48	47	cbvrexvw	$⊢ \exists v \in A \exists b \in B z = v + b \leftrightarrow \exists a \in A \exists b \in B z = a + b$
49	41	2rexbidv	$⊢ z = w \to (\exists a \in A \exists b \in B z = a + b \leftrightarrow \exists a \in A \exists b \in B w = a + b)$
50	48 49	syl5bb	$⊢ z = w \to (\exists v \in A \exists b \in B z = v + b \leftrightarrow \exists a \in A \exists b \in B w = a + b)$
51	21 50 7	elab2	$⊢ w \in C \leftrightarrow \exists a \in A \exists b \in B w = a + b$
52	44 51	sylibr	$⊢ (a \in A \land \exists b \in B w = a + b) \to w \in C$
53	52	ex	$⊢ a \in A \to (\exists b \in B w = a + b \to w \in C)$
54	1	sseld	$⊢ φ \to (a \in A \to a \in ℝ)$
55	4	sseld	$⊢ φ \to (b \in B \to b \in ℝ)$
56	54 55	anim12d	$⊢ φ \to ((a \in A \land b \in B) \to (a \in ℝ \land b \in ℝ))$
57		readdcl	$⊢ (a \in ℝ \land b \in ℝ) \to a + b \in ℝ$
58	56 57	syl6	$⊢ φ \to ((a \in A \land b \in B) \to a + b \in ℝ)$
59		eleq1a	$⊢ a + b \in ℝ \to (w = a + b \to w \in ℝ)$
60	58 59	syl6	$⊢ φ \to ((a \in A \land b \in B) \to (w = a + b \to w \in ℝ))$
61	60	rexlimdvv	$⊢ φ \to (\exists a \in A \exists b \in B w = a + b \to w \in ℝ)$
62	51 61	syl5bi	$⊢ φ \to (w \in C \to w \in ℝ)$
63	62	ssrdv	$⊢ φ \to C \subseteq ℝ$
64		ovex	$⊢ a + b \in V$
65	64	isseti	$⊢ \exists w w = a + b$
66	65	rgenw	$⊢ \forall b \in B \exists w w = a + b$
67		r19.2z	$⊢ (B \neq \emptyset \land \forall b \in B \exists w w = a + b) \to \exists b \in B \exists w w = a + b$
68	5 66 67	sylancl	$⊢ φ \to \exists b \in B \exists w w = a + b$
69		rexcom4	$⊢ \exists b \in B \exists w w = a + b \leftrightarrow \exists w \exists b \in B w = a + b$
70	68 69	sylib	$⊢ φ \to \exists w \exists b \in B w = a + b$
71	70	ralrimivw	$⊢ φ \to \forall a \in A \exists w \exists b \in B w = a + b$
72		r19.2z	$⊢ (A \neq \emptyset \land \forall a \in A \exists w \exists b \in B w = a + b) \to \exists a \in A \exists w \exists b \in B w = a + b$
73	2 71 72	syl2anc	$⊢ φ \to \exists a \in A \exists w \exists b \in B w = a + b$
74		rexcom4	$⊢ \exists a \in A \exists w \exists b \in B w = a + b \leftrightarrow \exists w \exists a \in A \exists b \in B w = a + b$
75	73 74	sylib	$⊢ φ \to \exists w \exists a \in A \exists b \in B w = a + b$
76		n0	$⊢ C \neq \emptyset \leftrightarrow \exists w w \in C$
77	51	exbii	$⊢ \exists w w \in C \leftrightarrow \exists w \exists a \in A \exists b \in B w = a + b$
78	76 77	bitri	$⊢ C \neq \emptyset \leftrightarrow \exists w \exists a \in A \exists b \in B w = a + b$
79	75 78	sylibr	$⊢ φ \to C \neq \emptyset$
80	1 2 3	suprcld	$⊢ φ \to sup (A ℝ <) \in ℝ$
81	80 8	readdcld	$⊢ φ \to sup (A ℝ <) + sup (B ℝ <) \in ℝ$
82	11	adantrr	$⊢ (φ \land (a \in A \land b \in B)) \to a \in ℝ$
83	30	adantrl	$⊢ (φ \land (a \in A \land b \in B)) \to b \in ℝ$
84	80	adantr	$⊢ (φ \land (a \in A \land b \in B)) \to sup (A ℝ <) \in ℝ$
85	8	adantr	$⊢ (φ \land (a \in A \land b \in B)) \to sup (B ℝ <) \in ℝ$
86	1 2 3	3jca	$⊢ φ \to (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)$
87		suprub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land a \in A) \to a \leq sup (A ℝ <)$
88	86 87	sylan	$⊢ (φ \land a \in A) \to a \leq sup (A ℝ <)$
89	88	adantrr	$⊢ (φ \land (a \in A \land b \in B)) \to a \leq sup (A ℝ <)$
90	4 5 6	3jca	$⊢ φ \to (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)$
91		suprub	$⊢ ((B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x) \land b \in B) \to b \leq sup (B ℝ <)$
92	90 91	sylan	$⊢ (φ \land b \in B) \to b \leq sup (B ℝ <)$
93	92	adantrl	$⊢ (φ \land (a \in A \land b \in B)) \to b \leq sup (B ℝ <)$
94	82 83 84 85 89 93	le2addd	$⊢ (φ \land (a \in A \land b \in B)) \to a + b \leq sup (A ℝ <) + sup (B ℝ <)$
95	94	ex	$⊢ φ \to ((a \in A \land b \in B) \to a + b \leq sup (A ℝ <) + sup (B ℝ <))$
96		breq1	$⊢ w = a + b \to (w \leq sup (A ℝ <) + sup (B ℝ <) \leftrightarrow a + b \leq sup (A ℝ <) + sup (B ℝ <))$
97	96	biimprcd	$⊢ a + b \leq sup (A ℝ <) + sup (B ℝ <) \to (w = a + b \to w \leq sup (A ℝ <) + sup (B ℝ <))$
98	95 97	syl6	$⊢ φ \to ((a \in A \land b \in B) \to (w = a + b \to w \leq sup (A ℝ <) + sup (B ℝ <)))$
99	98	rexlimdvv	$⊢ φ \to (\exists a \in A \exists b \in B w = a + b \to w \leq sup (A ℝ <) + sup (B ℝ <))$
100	51 99	syl5bi	$⊢ φ \to (w \in C \to w \leq sup (A ℝ <) + sup (B ℝ <))$
101	100	ralrimiv	$⊢ φ \to \forall w \in C w \leq sup (A ℝ <) + sup (B ℝ <)$
102		brralrspcev	$⊢ (sup (A ℝ <) + sup (B ℝ <) \in ℝ \land \forall w \in C w \leq sup (A ℝ <) + sup (B ℝ <)) \to \exists x \in ℝ \forall w \in C w \leq x$
103	81 101 102	syl2anc	$⊢ φ \to \exists x \in ℝ \forall w \in C w \leq x$
104		suprub	$⊢ ((C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \land w \in C) \to w \leq sup (C ℝ <)$
105	104	ex	$⊢ (C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \to (w \in C \to w \leq sup (C ℝ <))$
106	63 79 103 105	syl3anc	$⊢ φ \to (w \in C \to w \leq sup (C ℝ <))$
107	53 106	sylan9r	$⊢ (φ \land a \in A) \to (\exists b \in B w = a + b \to w \leq sup (C ℝ <))$
108	43 107	syl5bi	$⊢ (φ \land a \in A) \to (w \in \{z \| \exists b \in B z = a + b\} \to w \leq sup (C ℝ <))$
109	108	ralrimiv	$⊢ (φ \land a \in A) \to \forall w \in \{z \| \exists b \in B z = a + b\} w \leq sup (C ℝ <)$
110	33 31	readdcld	$⊢ ((φ \land a \in A) \land b \in B) \to a + b \in ℝ$
111		eleq1a	$⊢ a + b \in ℝ \to (z = a + b \to z \in ℝ)$
112	110 111	syl	$⊢ ((φ \land a \in A) \land b \in B) \to (z = a + b \to z \in ℝ)$
113	112	rexlimdva	$⊢ (φ \land a \in A) \to (\exists b \in B z = a + b \to z \in ℝ)$
114	113	abssdv	$⊢ (φ \land a \in A) \to \{z \| \exists b \in B z = a + b\} \subseteq ℝ$
115	64	isseti	$⊢ \exists z z = a + b$
116	115	rgenw	$⊢ \forall b \in B \exists z z = a + b$
117		r19.2z	$⊢ (B \neq \emptyset \land \forall b \in B \exists z z = a + b) \to \exists b \in B \exists z z = a + b$
118	5 116 117	sylancl	$⊢ φ \to \exists b \in B \exists z z = a + b$
119		rexcom4	$⊢ \exists b \in B \exists z z = a + b \leftrightarrow \exists z \exists b \in B z = a + b$
120	118 119	sylib	$⊢ φ \to \exists z \exists b \in B z = a + b$
121		abn0	$⊢ \{z \| \exists b \in B z = a + b\} \neq \emptyset \leftrightarrow \exists z \exists b \in B z = a + b$
122	120 121	sylibr	$⊢ φ \to \{z \| \exists b \in B z = a + b\} \neq \emptyset$
123	122	adantr	$⊢ (φ \land a \in A) \to \{z \| \exists b \in B z = a + b\} \neq \emptyset$
124	63 79 103	suprcld	$⊢ φ \to sup (C ℝ <) \in ℝ$
125	124	adantr	$⊢ (φ \land a \in A) \to sup (C ℝ <) \in ℝ$
126		brralrspcev	$⊢ (sup (C ℝ <) \in ℝ \land \forall w \in \{z \| \exists b \in B z = a + b\} w \leq sup (C ℝ <)) \to \exists x \in ℝ \forall w \in \{z \| \exists b \in B z = a + b\} w \leq x$
127	125 109 126	syl2anc	$⊢ (φ \land a \in A) \to \exists x \in ℝ \forall w \in \{z \| \exists b \in B z = a + b\} w \leq x$
128		suprleub	$⊢ ((\{z \| \exists b \in B z = a + b\} \subseteq ℝ \land \{z \| \exists b \in B z = a + b\} \neq \emptyset \land \exists x \in ℝ \forall w \in \{z \| \exists b \in B z = a + b\} w \leq x) \land sup (C ℝ <) \in ℝ) \to (sup (\{z \| \exists b \in B z = a + b\} ℝ <) \leq sup (C ℝ <) \leftrightarrow \forall w \in \{z \| \exists b \in B z = a + b\} w \leq sup (C ℝ <))$
129	114 123 127 125 128	syl31anc	$⊢ (φ \land a \in A) \to (sup (\{z \| \exists b \in B z = a + b\} ℝ <) \leq sup (C ℝ <) \leftrightarrow \forall w \in \{z \| \exists b \in B z = a + b\} w \leq sup (C ℝ <))$
130	109 129	mpbird	$⊢ (φ \land a \in A) \to sup (\{z \| \exists b \in B z = a + b\} ℝ <) \leq sup (C ℝ <)$
131	40 130	eqbrtrd	$⊢ (φ \land a \in A) \to sup (B ℝ <) + a \leq sup (C ℝ <)$
132		breq1	$⊢ w = sup (B ℝ <) + a \to (w \leq sup (C ℝ <) \leftrightarrow sup (B ℝ <) + a \leq sup (C ℝ <))$
133	131 132	syl5ibrcom	$⊢ (φ \land a \in A) \to (w = sup (B ℝ <) + a \to w \leq sup (C ℝ <))$
134	133	rexlimdva	$⊢ φ \to (\exists a \in A w = sup (B ℝ <) + a \to w \leq sup (C ℝ <))$
135	24 134	syl5bi	$⊢ φ \to (w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} \to w \leq sup (C ℝ <))$
136	135	ralrimiv	$⊢ φ \to \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} w \leq sup (C ℝ <)$
137	13 11	readdcld	$⊢ (φ \land a \in A) \to sup (B ℝ <) + a \in ℝ$
138		eleq1a	$⊢ sup (B ℝ <) + a \in ℝ \to (z = sup (B ℝ <) + a \to z \in ℝ)$
139	137 138	syl	$⊢ (φ \land a \in A) \to (z = sup (B ℝ <) + a \to z \in ℝ)$
140	139	rexlimdva	$⊢ φ \to (\exists a \in A z = sup (B ℝ <) + a \to z \in ℝ)$
141	140	abssdv	$⊢ φ \to \{z \| \exists a \in A z = sup (B ℝ <) + a\} \subseteq ℝ$
142		ovex	$⊢ sup (B ℝ <) + a \in V$
143	142	isseti	$⊢ \exists z z = sup (B ℝ <) + a$
144	143	rgenw	$⊢ \forall a \in A \exists z z = sup (B ℝ <) + a$
145		r19.2z	$⊢ (A \neq \emptyset \land \forall a \in A \exists z z = sup (B ℝ <) + a) \to \exists a \in A \exists z z = sup (B ℝ <) + a$
146	2 144 145	sylancl	$⊢ φ \to \exists a \in A \exists z z = sup (B ℝ <) + a$
147		rexcom4	$⊢ \exists a \in A \exists z z = sup (B ℝ <) + a \leftrightarrow \exists z \exists a \in A z = sup (B ℝ <) + a$
148	146 147	sylib	$⊢ φ \to \exists z \exists a \in A z = sup (B ℝ <) + a$
149		abn0	$⊢ \{z \| \exists a \in A z = sup (B ℝ <) + a\} \neq \emptyset \leftrightarrow \exists z \exists a \in A z = sup (B ℝ <) + a$
150	148 149	sylibr	$⊢ φ \to \{z \| \exists a \in A z = sup (B ℝ <) + a\} \neq \emptyset$
151		brralrspcev	$⊢ (sup (C ℝ <) \in ℝ \land \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} w \leq sup (C ℝ <)) \to \exists x \in ℝ \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} w \leq x$
152	124 136 151	syl2anc	$⊢ φ \to \exists x \in ℝ \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} w \leq x$
153		suprleub	$⊢ ((\{z \| \exists a \in A z = sup (B ℝ <) + a\} \subseteq ℝ \land \{z \| \exists a \in A z = sup (B ℝ <) + a\} \neq \emptyset \land \exists x \in ℝ \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} w \leq x) \land sup (C ℝ <) \in ℝ) \to (sup (\{z \| \exists a \in A z = sup (B ℝ <) + a\} ℝ <) \leq sup (C ℝ <) \leftrightarrow \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} w \leq sup (C ℝ <))$
154	141 150 152 124 153	syl31anc	$⊢ φ \to (sup (\{z \| \exists a \in A z = sup (B ℝ <) + a\} ℝ <) \leq sup (C ℝ <) \leftrightarrow \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) + a\} w \leq sup (C ℝ <))$
155	136 154	mpbird	$⊢ φ \to sup (\{z \| \exists a \in A z = sup (B ℝ <) + a\} ℝ <) \leq sup (C ℝ <)$
156	20 155	eqbrtrd	$⊢ φ \to sup (A ℝ <) + sup (B ℝ <) \leq sup (C ℝ <)$
157		suprleub	$⊢ ((C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \land sup (A ℝ <) + sup (B ℝ <) \in ℝ) \to (sup (C ℝ <) \leq sup (A ℝ <) + sup (B ℝ <) \leftrightarrow \forall w \in C w \leq sup (A ℝ <) + sup (B ℝ <))$
158	63 79 103 81 157	syl31anc	$⊢ φ \to (sup (C ℝ <) \leq sup (A ℝ <) + sup (B ℝ <) \leftrightarrow \forall w \in C w \leq sup (A ℝ <) + sup (B ℝ <))$
159	101 158	mpbird	$⊢ φ \to sup (C ℝ <) \leq sup (A ℝ <) + sup (B ℝ <)$
160	81 124	letri3d	$⊢ φ \to (sup (A ℝ <) + sup (B ℝ <) = sup (C ℝ <) \leftrightarrow (sup (A ℝ <) + sup (B ℝ <) \leq sup (C ℝ <) \land sup (C ℝ <) \leq sup (A ℝ <) + sup (B ℝ <)))$
161	156 159 160	mpbir2and	$⊢ φ \to sup (A ℝ <) + sup (B ℝ <) = sup (C ℝ <)$

Metamath Proof Explorer

Theorem supadd

Proof