suplesup

Description: If any element of A can be approximated from below by members of B , then the supremum of A is less than or equal to the supremum of B . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	suplesup.a	$⊢ φ \to A \subseteq ℝ$
	suplesup.b	$⊢ φ \to B \subseteq ℝ^{*}$
	suplesup.c	$⊢ φ \to \forall x \in A \forall y \in ℝ^{+} \exists z \in B x - y < z$
Assertion	suplesup	$⊢ φ \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		suplesup.a	$⊢ φ \to A \subseteq ℝ$
2		suplesup.b	$⊢ φ \to B \subseteq ℝ^{*}$
3		suplesup.c	$⊢ φ \to \forall x \in A \forall y \in ℝ^{+} \exists z \in B x - y < z$
4		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
5	1 4	sstrdi	$⊢ φ \to A \subseteq ℝ^{*}$
6		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
7	5 6	syl	$⊢ φ \to sup (A ℝ^{} <) \in ℝ^{}$
8	7	adantr	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) \in ℝ^{*}$
9		eqidd	$⊢ (φ \land sup (A ℝ^{*} <) = +∞) \to +∞ = +∞$
10		simpr	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) = +∞$
11		peano2re	$⊢ w \in ℝ \to w + 1 \in ℝ$
12	11	adantl	$⊢ ((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \to w + 1 \in ℝ$
13	5	adantr	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to A \subseteq ℝ^{}$
14		supxrunb2	$⊢ A \subseteq ℝ^{} \to (\forall r \in ℝ \exists x \in A r < x \leftrightarrow sup (A ℝ^{} <) = +∞)$
15	13 14	syl	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to (\forall r \in ℝ \exists x \in A r < x \leftrightarrow sup (A ℝ^{} <) = +∞)$
16	10 15	mpbird	$⊢ (φ \land sup (A ℝ^{*} <) = +∞) \to \forall r \in ℝ \exists x \in A r < x$
17	16	adantr	$⊢ ((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \to \forall r \in ℝ \exists x \in A r < x$
18		breq1	$⊢ r = w + 1 \to (r < x \leftrightarrow w + 1 < x)$
19	18	rexbidv	$⊢ r = w + 1 \to (\exists x \in A r < x \leftrightarrow \exists x \in A w + 1 < x)$
20	19	rspcva	$⊢ (w + 1 \in ℝ \land \forall r \in ℝ \exists x \in A r < x) \to \exists x \in A w + 1 < x$
21	12 17 20	syl2anc	$⊢ ((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \to \exists x \in A w + 1 < x$
22		1rp	$⊢ 1 \in ℝ^{+}$
23	22	a1i	$⊢ (φ \land x \in A) \to 1 \in ℝ^{+}$
24	3	r19.21bi	$⊢ (φ \land x \in A) \to \forall y \in ℝ^{+} \exists z \in B x - y < z$
25		oveq2	$⊢ y = 1 \to x - y = x - 1$
26	25	breq1d	$⊢ y = 1 \to (x - y < z \leftrightarrow x - 1 < z)$
27	26	rexbidv	$⊢ y = 1 \to (\exists z \in B x - y < z \leftrightarrow \exists z \in B x - 1 < z)$
28	27	rspcva	$⊢ (1 \in ℝ^{+} \land \forall y \in ℝ^{+} \exists z \in B x - y < z) \to \exists z \in B x - 1 < z$
29	23 24 28	syl2anc	$⊢ (φ \land x \in A) \to \exists z \in B x - 1 < z$
30	29	adantlr	$⊢ ((φ \land w \in ℝ) \land x \in A) \to \exists z \in B x - 1 < z$
31	30	3adant3	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to \exists z \in B x - 1 < z$
32		nfv	$⊢ Ⅎ z ((φ \land w \in ℝ) \land x \in A \land w + 1 < x)$
33		simp11r	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B \land x - 1 < z) \to w \in ℝ$
34	4 33	sseldi	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B \land x - 1 < z) \to w \in ℝ^{*}$
35	1	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
36		1red	$⊢ (φ \land x \in A) \to 1 \in ℝ$
37	35 36	resubcld	$⊢ (φ \land x \in A) \to x - 1 \in ℝ$
38	37	adantlr	$⊢ ((φ \land w \in ℝ) \land x \in A) \to x - 1 \in ℝ$
39	38	3adant3	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to x - 1 \in ℝ$
40	39	3ad2ant1	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B \land x - 1 < z) \to x - 1 \in ℝ$
41	4 40	sseldi	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B \land x - 1 < z) \to x - 1 \in ℝ^{*}$
42	2	sselda	$⊢ (φ \land z \in B) \to z \in ℝ^{*}$
43	42	adantlr	$⊢ ((φ \land w \in ℝ) \land z \in B) \to z \in ℝ^{*}$
44	43	3ad2antl1	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B) \to z \in ℝ^{*}$
45	44	3adant3	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B \land x - 1 < z) \to z \in ℝ^{*}$
46		simp3	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to w + 1 < x$
47		simp1r	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to w \in ℝ$
48		1red	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to 1 \in ℝ$
49	35	adantlr	$⊢ ((φ \land w \in ℝ) \land x \in A) \to x \in ℝ$
50	49	3adant3	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to x \in ℝ$
51	47 48 50	ltaddsubd	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to (w + 1 < x \leftrightarrow w < x - 1)$
52	46 51	mpbid	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to w < x - 1$
53	52	3ad2ant1	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B \land x - 1 < z) \to w < x - 1$
54		simp3	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B \land x - 1 < z) \to x - 1 < z$
55	34 41 45 53 54	xrlttrd	$⊢ (((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \land z \in B \land x - 1 < z) \to w < z$
56	55	3exp	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to (z \in B \to (x - 1 < z \to w < z))$
57	32 56	reximdai	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to (\exists z \in B x - 1 < z \to \exists z \in B w < z)$
58	31 57	mpd	$⊢ ((φ \land w \in ℝ) \land x \in A \land w + 1 < x) \to \exists z \in B w < z$
59	58	3exp	$⊢ (φ \land w \in ℝ) \to (x \in A \to (w + 1 < x \to \exists z \in B w < z))$
60	59	adantlr	$⊢ ((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \to (x \in A \to (w + 1 < x \to \exists z \in B w < z))$
61	60	rexlimdv	$⊢ ((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \to (\exists x \in A w + 1 < x \to \exists z \in B w < z)$
62	21 61	mpd	$⊢ ((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \to \exists z \in B w < z$
63	4	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
64	63	sselda	$⊢ (φ \land w \in ℝ) \to w \in ℝ^{*}$
65	64	ad2antrr	$⊢ (((φ \land w \in ℝ) \land z \in B) \land w < z) \to w \in ℝ^{*}$
66	43	adantr	$⊢ (((φ \land w \in ℝ) \land z \in B) \land w < z) \to z \in ℝ^{*}$
67		simpr	$⊢ (((φ \land w \in ℝ) \land z \in B) \land w < z) \to w < z$
68	65 66 67	xrltled	$⊢ (((φ \land w \in ℝ) \land z \in B) \land w < z) \to w \leq z$
69	68	ex	$⊢ ((φ \land w \in ℝ) \land z \in B) \to (w < z \to w \leq z)$
70	69	adantllr	$⊢ (((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \land z \in B) \to (w < z \to w \leq z)$
71	70	reximdva	$⊢ ((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \to (\exists z \in B w < z \to \exists z \in B w \leq z)$
72	62 71	mpd	$⊢ ((φ \land sup (A ℝ^{*} <) = +∞) \land w \in ℝ) \to \exists z \in B w \leq z$
73	72	ralrimiva	$⊢ (φ \land sup (A ℝ^{*} <) = +∞) \to \forall w \in ℝ \exists z \in B w \leq z$
74		supxrunb1	$⊢ B \subseteq ℝ^{} \to (\forall w \in ℝ \exists z \in B w \leq z \leftrightarrow sup (B ℝ^{} <) = +∞)$
75	2 74	syl	$⊢ φ \to (\forall w \in ℝ \exists z \in B w \leq z \leftrightarrow sup (B ℝ^{*} <) = +∞)$
76	75	adantr	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to (\forall w \in ℝ \exists z \in B w \leq z \leftrightarrow sup (B ℝ^{} <) = +∞)$
77	73 76	mpbid	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to sup (B ℝ^{} <) = +∞$
78	9 10 77	3eqtr4d	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) = sup (B ℝ^{*} <)$
79	8 78	xreqled	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
80		supeq1	$⊢ A = \emptyset \to sup (A ℝ^{} <) = sup (\emptyset ℝ^{} <)$
81		xrsup0	$⊢ sup (\emptyset ℝ^{*} <) = −∞$
82	81	a1i	$⊢ A = \emptyset \to sup (\emptyset ℝ^{*} <) = −∞$
83	80 82	eqtrd	$⊢ A = \emptyset \to sup (A ℝ^{*} <) = −∞$
84	83	adantl	$⊢ (φ \land A = \emptyset) \to sup (A ℝ^{*} <) = −∞$
85		supxrcl	$⊢ B \subseteq ℝ^{} \to sup (B ℝ^{} <) \in ℝ^{*}$
86	2 85	syl	$⊢ φ \to sup (B ℝ^{} <) \in ℝ^{}$
87		mnfle	$⊢ sup (B ℝ^{} <) \in ℝ^{} \to −∞ \leq sup (B ℝ^{*} <)$
88	86 87	syl	$⊢ φ \to −∞ \leq sup (B ℝ^{*} <)$
89	88	adantr	$⊢ (φ \land A = \emptyset) \to −∞ \leq sup (B ℝ^{*} <)$
90	84 89	eqbrtrd	$⊢ (φ \land A = \emptyset) \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$
91	90	adantlr	$⊢ ((φ \land \neg sup (A ℝ^{} <) = +∞) \land A = \emptyset) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
92		simpll	$⊢ ((φ \land \neg sup (A ℝ^{*} <) = +∞) \land \neg A = \emptyset) \to φ$
93	1	adantr	$⊢ (φ \land \neg A = \emptyset) \to A \subseteq ℝ$
94		neqne	$⊢ \neg A = \emptyset \to A \neq \emptyset$
95	94	adantl	$⊢ (φ \land \neg A = \emptyset) \to A \neq \emptyset$
96		supxrgtmnf	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to −∞ < sup (A ℝ^{*} <)$
97	93 95 96	syl2anc	$⊢ (φ \land \neg A = \emptyset) \to −∞ < sup (A ℝ^{*} <)$
98	97	adantlr	$⊢ ((φ \land \neg sup (A ℝ^{} <) = +∞) \land \neg A = \emptyset) \to −∞ < sup (A ℝ^{} <)$
99		simpr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to \neg sup (A ℝ^{} <) = +∞$
100		simpl	$⊢ (φ \land \neg sup (A ℝ^{*} <) = +∞) \to φ$
101		nltpnft	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
102	100 7 101	3syl	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{*} <) < +∞)$
103	99 102	mtbid	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to \neg \neg sup (A ℝ^{} <) < +∞$
104		notnotr	$⊢ \neg \neg sup (A ℝ^{} <) < +∞ \to sup (A ℝ^{} <) < +∞$
105	103 104	syl	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) < +∞$
106	105	adantr	$⊢ ((φ \land \neg sup (A ℝ^{} <) = +∞) \land \neg A = \emptyset) \to sup (A ℝ^{} <) < +∞$
107	98 106	jca	$⊢ ((φ \land \neg sup (A ℝ^{} <) = +∞) \land \neg A = \emptyset) \to (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞)$
108	92 7	syl	$⊢ ((φ \land \neg sup (A ℝ^{} <) = +∞) \land \neg A = \emptyset) \to sup (A ℝ^{} <) \in ℝ^{*}$
109		xrrebnd	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞))$
110	108 109	syl	$⊢ ((φ \land \neg sup (A ℝ^{} <) = +∞) \land \neg A = \emptyset) \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{} <) < +∞))$
111	107 110	mpbird	$⊢ ((φ \land \neg sup (A ℝ^{} <) = +∞) \land \neg A = \emptyset) \to sup (A ℝ^{} <) \in ℝ$
112		nfv	$⊢ Ⅎ w (φ \land sup (A ℝ^{*} <) \in ℝ)$
113	2	adantr	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to B \subseteq ℝ^{}$
114		simpr	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to sup (A ℝ^{} <) \in ℝ$
115	114	adantr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to sup (A ℝ^{} <) \in ℝ$
116		simpr	$⊢ ((φ \land sup (A ℝ^{*} <) \in ℝ) \land w \in ℝ^{+}) \to w \in ℝ^{+}$
117	116	rphalfcld	$⊢ ((φ \land sup (A ℝ^{*} <) \in ℝ) \land w \in ℝ^{+}) \to \frac{w}{2} \in ℝ^{+}$
118	115 117	ltsubrpd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to sup (A ℝ^{} <) - (\frac{w}{2}) < sup (A ℝ^{*} <)$
119	5	ad2antrr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to A \subseteq ℝ^{}$
120		rpre	$⊢ w \in ℝ^{+} \to w \in ℝ$
121		2re	$⊢ 2 \in ℝ$
122	121	a1i	$⊢ w \in ℝ^{+} \to 2 \in ℝ$
123		2ne0	$⊢ 2 \neq 0$
124	123	a1i	$⊢ w \in ℝ^{+} \to 2 \neq 0$
125	120 122 124	redivcld	$⊢ w \in ℝ^{+} \to \frac{w}{2} \in ℝ$
126	125	adantl	$⊢ ((φ \land sup (A ℝ^{*} <) \in ℝ) \land w \in ℝ^{+}) \to \frac{w}{2} \in ℝ$
127	115 126	resubcld	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to sup (A ℝ^{} <) - (\frac{w}{2}) \in ℝ$
128	4 127	sseldi	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to sup (A ℝ^{} <) - (\frac{w}{2}) \in ℝ^{*}$
129		supxrlub	$⊢ (A \subseteq ℝ^{} \land sup (A ℝ^{} <) - (\frac{w}{2}) \in ℝ^{}) \to (sup (A ℝ^{} <) - (\frac{w}{2}) < sup (A ℝ^{} <) \leftrightarrow \exists x \in A sup (A ℝ^{} <) - (\frac{w}{2}) < x)$
130	119 128 129	syl2anc	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to (sup (A ℝ^{} <) - (\frac{w}{2}) < sup (A ℝ^{} <) \leftrightarrow \exists x \in A sup (A ℝ^{} <) - (\frac{w}{2}) < x)$
131	118 130	mpbid	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to \exists x \in A sup (A ℝ^{} <) - (\frac{w}{2}) < x$
132		rphalfcl	$⊢ w \in ℝ^{+} \to \frac{w}{2} \in ℝ^{+}$
133	132	3ad2ant2	$⊢ (φ \land w \in ℝ^{+} \land x \in A) \to \frac{w}{2} \in ℝ^{+}$
134	24	3adant2	$⊢ (φ \land w \in ℝ^{+} \land x \in A) \to \forall y \in ℝ^{+} \exists z \in B x - y < z$
135		oveq2	$⊢ y = \frac{w}{2} \to x - y = x - (\frac{w}{2})$
136	135	breq1d	$⊢ y = \frac{w}{2} \to (x - y < z \leftrightarrow x - (\frac{w}{2}) < z)$
137	136	rexbidv	$⊢ y = \frac{w}{2} \to (\exists z \in B x - y < z \leftrightarrow \exists z \in B x - (\frac{w}{2}) < z)$
138	137	rspcva	$⊢ (\frac{w}{2} \in ℝ^{+} \land \forall y \in ℝ^{+} \exists z \in B x - y < z) \to \exists z \in B x - (\frac{w}{2}) < z$
139	133 134 138	syl2anc	$⊢ (φ \land w \in ℝ^{+} \land x \in A) \to \exists z \in B x - (\frac{w}{2}) < z$
140	139	ad5ant134	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \to \exists z \in B x - (\frac{w}{2}) < z$
141		recn	$⊢ sup (A ℝ^{} <) \in ℝ \to sup (A ℝ^{} <) \in ℂ$
142	141	adantr	$⊢ (sup (A ℝ^{} <) \in ℝ \land w \in ℝ^{+}) \to sup (A ℝ^{} <) \in ℂ$
143	120	recnd	$⊢ w \in ℝ^{+} \to w \in ℂ$
144	143	adantl	$⊢ (sup (A ℝ^{*} <) \in ℝ \land w \in ℝ^{+}) \to w \in ℂ$
145	144	halfcld	$⊢ (sup (A ℝ^{*} <) \in ℝ \land w \in ℝ^{+}) \to \frac{w}{2} \in ℂ$
146	142 145 145	subsub4d	$⊢ (sup (A ℝ^{} <) \in ℝ \land w \in ℝ^{+}) \to sup (A ℝ^{} <) - (\frac{w}{2}) - (\frac{w}{2}) = sup (A ℝ^{*} <) - ((\frac{w}{2}) + (\frac{w}{2}))$
147	143	2halvesd	$⊢ w \in ℝ^{+} \to (\frac{w}{2}) + (\frac{w}{2}) = w$
148	147	oveq2d	$⊢ w \in ℝ^{+} \to sup (A ℝ^{} <) - ((\frac{w}{2}) + (\frac{w}{2})) = sup (A ℝ^{} <) - w$
149	148	adantl	$⊢ (sup (A ℝ^{} <) \in ℝ \land w \in ℝ^{+}) \to sup (A ℝ^{} <) - ((\frac{w}{2}) + (\frac{w}{2})) = sup (A ℝ^{*} <) - w$
150	146 149	eqtr2d	$⊢ (sup (A ℝ^{} <) \in ℝ \land w \in ℝ^{+}) \to sup (A ℝ^{} <) - w = sup (A ℝ^{*} <) - (\frac{w}{2}) - (\frac{w}{2})$
151	150	adantll	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to sup (A ℝ^{} <) - w = sup (A ℝ^{*} <) - (\frac{w}{2}) - (\frac{w}{2})$
152	151	adantr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \to sup (A ℝ^{} <) - w = sup (A ℝ^{*} <) - (\frac{w}{2}) - (\frac{w}{2})$
153	152	ad3antrrr	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{} <) - w = sup (A ℝ^{} <) - (\frac{w}{2}) - (\frac{w}{2})$
154	127 126	resubcld	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to sup (A ℝ^{} <) - (\frac{w}{2}) - (\frac{w}{2}) \in ℝ$
155	154	adantr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \to sup (A ℝ^{} <) - (\frac{w}{2}) - (\frac{w}{2}) \in ℝ$
156	155	ad3antrrr	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{*} <) - (\frac{w}{2}) - (\frac{w}{2}) \in ℝ$
157	4 156	sseldi	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{} <) - (\frac{w}{2}) - (\frac{w}{2}) \in ℝ^{}$
158	120 49	sylanl2	$⊢ ((φ \land w \in ℝ^{+}) \land x \in A) \to x \in ℝ$
159	125	ad2antlr	$⊢ ((φ \land w \in ℝ^{+}) \land x \in A) \to \frac{w}{2} \in ℝ$
160	158 159	resubcld	$⊢ ((φ \land w \in ℝ^{+}) \land x \in A) \to x - (\frac{w}{2}) \in ℝ$
161	160	adantllr	$⊢ (((φ \land sup (A ℝ^{*} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \to x - (\frac{w}{2}) \in ℝ$
162	161	ad3antrrr	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to x - (\frac{w}{2}) \in ℝ$
163	4 162	sseldi	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to x - (\frac{w}{2}) \in ℝ^{*}$
164		simp-6l	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to φ$
165		simplr	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to z \in B$
166	164 165 42	syl2anc	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to z \in ℝ^{*}$
167		simp-6r	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{*} <) \in ℝ$
168	120	ad5antlr	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to w \in ℝ$
169	168	rehalfcld	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to \frac{w}{2} \in ℝ$
170	167 169	resubcld	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{*} <) - (\frac{w}{2}) \in ℝ$
171		simp-4r	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to x \in A$
172	164 171 35	syl2anc	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to x \in ℝ$
173		simpllr	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{*} <) - (\frac{w}{2}) < x$
174	170 172 169 173	ltsub1dd	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{*} <) - (\frac{w}{2}) - (\frac{w}{2}) < x - (\frac{w}{2})$
175		simpr	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to x - (\frac{w}{2}) < z$
176	157 163 166 174 175	xrlttrd	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{*} <) - (\frac{w}{2}) - (\frac{w}{2}) < z$
177	153 176	eqbrtrd	$⊢ ((((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \land x - (\frac{w}{2}) < z) \to sup (A ℝ^{*} <) - w < z$
178	177	ex	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \land z \in B) \to (x - (\frac{w}{2}) < z \to sup (A ℝ^{*} <) - w < z)$
179	178	reximdva	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \to (\exists z \in B x - (\frac{w}{2}) < z \to \exists z \in B sup (A ℝ^{*} <) - w < z)$
180	140 179	mpd	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \land x \in A) \land sup (A ℝ^{} <) - (\frac{w}{2}) < x) \to \exists z \in B sup (A ℝ^{*} <) - w < z$
181	180	rexlimdva2	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to (\exists x \in A sup (A ℝ^{} <) - (\frac{w}{2}) < x \to \exists z \in B sup (A ℝ^{*} <) - w < z)$
182	131 181	mpd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land w \in ℝ^{+}) \to \exists z \in B sup (A ℝ^{} <) - w < z$
183	112 113 114 182	supxrgere	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
184	92 111 183	syl2anc	$⊢ ((φ \land \neg sup (A ℝ^{} <) = +∞) \land \neg A = \emptyset) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
185	91 184	pm2.61dan	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
186	79 185	pm2.61dan	$⊢ φ \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$

Metamath Proof Explorer

Theorem suplesup

Proof