supmullem1

	Ref	Expression
Hypotheses	supmul.1	$⊢ C = \{z \| \exists v \in A \exists b \in B z = v b\}$
	supmul.2	$⊢ φ \leftrightarrow ((\forall x \in A 0 \leq x \land \forall x \in B 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x))$
Assertion	supmullem1	$⊢ φ \to \forall w \in C w \leq sup (A ℝ <) sup (B ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		supmul.1	$⊢ C = \{z \| \exists v \in A \exists b \in B z = v b\}$
2		supmul.2	$⊢ φ \leftrightarrow ((\forall x \in A 0 \leq x \land \forall x \in B 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x))$
3		vex	$⊢ w \in V$
4		oveq1	$⊢ v = a \to v b = a b$
5	4	eqeq2d	$⊢ v = a \to (z = v b \leftrightarrow z = a b)$
6	5	rexbidv	$⊢ v = a \to (\exists b \in B z = v b \leftrightarrow \exists b \in B z = a b)$
7	6	cbvrexvw	$⊢ \exists v \in A \exists b \in B z = v b \leftrightarrow \exists a \in A \exists b \in B z = a b$
8		eqeq1	$⊢ z = w \to (z = a b \leftrightarrow w = a b)$
9	8	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)$
10	7 9	bitrid	$⊢ 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)$
11	3 10 1	elab2	$⊢ w \in C \leftrightarrow \exists a \in A \exists b \in B w = a b$
12	2	simp2bi	$⊢ φ \to (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)$
13	12	simp1d	$⊢ φ \to A \subseteq ℝ$
14	13	sselda	$⊢ (φ \land a \in A) \to a \in ℝ$
15	14	adantrr	$⊢ (φ \land (a \in A \land b \in B)) \to a \in ℝ$
16		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
17	12 16	syl	$⊢ φ \to sup (A ℝ <) \in ℝ$
18	17	adantr	$⊢ (φ \land (a \in A \land b \in B)) \to sup (A ℝ <) \in ℝ$
19	2	simp3bi	$⊢ φ \to (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)$
20	19	simp1d	$⊢ φ \to B \subseteq ℝ$
21	20	sselda	$⊢ (φ \land b \in B) \to b \in ℝ$
22	21	adantrl	$⊢ (φ \land (a \in A \land b \in B)) \to b \in ℝ$
23		suprcl	$⊢ (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x) \to sup (B ℝ <) \in ℝ$
24	19 23	syl	$⊢ φ \to sup (B ℝ <) \in ℝ$
25	24	adantr	$⊢ (φ \land (a \in A \land b \in B)) \to sup (B ℝ <) \in ℝ$
26		simp1l	$⊢ ((\forall x \in A 0 \leq x \land \forall x \in B 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)) \to \forall x \in A 0 \leq x$
27	2 26	sylbi	$⊢ φ \to \forall x \in A 0 \leq x$
28		breq2	$⊢ x = a \to (0 \leq x \leftrightarrow 0 \leq a)$
29	28	rspccv	$⊢ \forall x \in A 0 \leq x \to (a \in A \to 0 \leq a)$
30	27 29	syl	$⊢ φ \to (a \in A \to 0 \leq a)$
31	30	imp	$⊢ (φ \land a \in A) \to 0 \leq a$
32	31	adantrr	$⊢ (φ \land (a \in A \land b \in B)) \to 0 \leq a$
33		simp1r	$⊢ ((\forall x \in A 0 \leq x \land \forall x \in B 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)) \to \forall x \in B 0 \leq x$
34	2 33	sylbi	$⊢ φ \to \forall x \in B 0 \leq x$
35		breq2	$⊢ x = b \to (0 \leq x \leftrightarrow 0 \leq b)$
36	35	rspccv	$⊢ \forall x \in B 0 \leq x \to (b \in B \to 0 \leq b)$
37	34 36	syl	$⊢ φ \to (b \in B \to 0 \leq b)$
38	37	imp	$⊢ (φ \land b \in B) \to 0 \leq b$
39	38	adantrl	$⊢ (φ \land (a \in A \land b \in B)) \to 0 \leq b$
40		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 ℝ <)$
41	12 40	sylan	$⊢ (φ \land a \in A) \to a \leq sup (A ℝ <)$
42	41	adantrr	$⊢ (φ \land (a \in A \land b \in B)) \to a \leq sup (A ℝ <)$
43		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 ℝ <)$
44	19 43	sylan	$⊢ (φ \land b \in B) \to b \leq sup (B ℝ <)$
45	44	adantrl	$⊢ (φ \land (a \in A \land b \in B)) \to b \leq sup (B ℝ <)$
46	15 18 22 25 32 39 42 45	lemul12ad	$⊢ (φ \land (a \in A \land b \in B)) \to a b \leq sup (A ℝ <) sup (B ℝ <)$
47	46	ex	$⊢ φ \to ((a \in A \land b \in B) \to a b \leq sup (A ℝ <) sup (B ℝ <))$
48		breq1	$⊢ w = a b \to (w \leq sup (A ℝ <) sup (B ℝ <) \leftrightarrow a b \leq sup (A ℝ <) sup (B ℝ <))$
49	48	biimprcd	$⊢ a b \leq sup (A ℝ <) sup (B ℝ <) \to (w = a b \to w \leq sup (A ℝ <) sup (B ℝ <))$
50	47 49	syl6	$⊢ φ \to ((a \in A \land b \in B) \to (w = a b \to w \leq sup (A ℝ <) sup (B ℝ <)))$
51	50	rexlimdvv	$⊢ φ \to (\exists a \in A \exists b \in B w = a b \to w \leq sup (A ℝ <) sup (B ℝ <))$
52	11 51	biimtrid	$⊢ φ \to (w \in C \to w \leq sup (A ℝ <) sup (B ℝ <))$
53	52	ralrimiv	$⊢ φ \to \forall w \in C w \leq sup (A ℝ <) sup (B ℝ <)$

Metamath Proof Explorer

Theorem supmullem1

Proof