suprzcl

Description: The supremum of a bounded-above set of integers is a member of the set. (Contributed by Paul Chapman, 21-Mar-2011) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	suprzcl	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in A$

Proof

Step	Hyp	Ref	Expression
1		zssre	$⊢ ℤ \subseteq ℝ$
2		sstr	$⊢ (A \subseteq ℤ \land ℤ \subseteq ℝ) \to A \subseteq ℝ$
3	1 2	mpan2	$⊢ A \subseteq ℤ \to A \subseteq ℝ$
4		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
5	3 4	syl3an1	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
6	5	ltm1d	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) - 1 < sup (A ℝ <)$
7		peano2rem	$⊢ sup (A ℝ <) \in ℝ \to sup (A ℝ <) - 1 \in ℝ$
8	4 7	syl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) - 1 \in ℝ$
9		suprlub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land sup (A ℝ <) - 1 \in ℝ) \to (sup (A ℝ <) - 1 < sup (A ℝ <) \leftrightarrow \exists z \in A sup (A ℝ <) - 1 < z)$
10	8 9	mpdan	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (sup (A ℝ <) - 1 < sup (A ℝ <) \leftrightarrow \exists z \in A sup (A ℝ <) - 1 < z)$
11	3 10	syl3an1	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (sup (A ℝ <) - 1 < sup (A ℝ <) \leftrightarrow \exists z \in A sup (A ℝ <) - 1 < z)$
12	6 11	mpbid	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to \exists z \in A sup (A ℝ <) - 1 < z$
13		simpl1	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to A \subseteq ℤ$
14	13	sselda	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to w \in ℤ$
15	1 14	sseldi	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to w \in ℝ$
16	5	adantr	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to sup (A ℝ <) \in ℝ$
17	16	adantr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to sup (A ℝ <) \in ℝ$
18		simprl	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to z \in A$
19	13 18	sseldd	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to z \in ℤ$
20		zre	$⊢ z \in ℤ \to z \in ℝ$
21	19 20	syl	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to z \in ℝ$
22		peano2re	$⊢ z \in ℝ \to z + 1 \in ℝ$
23	21 22	syl	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to z + 1 \in ℝ$
24	23	adantr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to z + 1 \in ℝ$
25		suprub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land w \in A) \to w \leq sup (A ℝ <)$
26	3 25	syl3anl1	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land w \in A) \to w \leq sup (A ℝ <)$
27	26	adantlr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to w \leq sup (A ℝ <)$
28		simprr	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to sup (A ℝ <) - 1 < z$
29		1red	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to 1 \in ℝ$
30	16 29 21	ltsubaddd	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to (sup (A ℝ <) - 1 < z \leftrightarrow sup (A ℝ <) < z + 1)$
31	28 30	mpbid	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to sup (A ℝ <) < z + 1$
32	31	adantr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to sup (A ℝ <) < z + 1$
33	15 17 24 27 32	lelttrd	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to w < z + 1$
34	19	adantr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to z \in ℤ$
35		zleltp1	$⊢ (w \in ℤ \land z \in ℤ) \to (w \leq z \leftrightarrow w < z + 1)$
36	14 34 35	syl2anc	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to (w \leq z \leftrightarrow w < z + 1)$
37	33 36	mpbird	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \land w \in A) \to w \leq z$
38	37	ralrimiva	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to \forall w \in A w \leq z$
39		suprleub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in ℝ) \to (sup (A ℝ <) \leq z \leftrightarrow \forall w \in A w \leq z)$
40	3 39	syl3anl1	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in ℝ) \to (sup (A ℝ <) \leq z \leftrightarrow \forall w \in A w \leq z)$
41	21 40	syldan	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to (sup (A ℝ <) \leq z \leftrightarrow \forall w \in A w \leq z)$
42	38 41	mpbird	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to sup (A ℝ <) \leq z$
43		suprub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to z \leq sup (A ℝ <)$
44	3 43	syl3anl1	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to z \leq sup (A ℝ <)$
45	44	adantrr	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to z \leq sup (A ℝ <)$
46	16 21	letri3d	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to (sup (A ℝ <) = z \leftrightarrow (sup (A ℝ <) \leq z \land z \leq sup (A ℝ <)))$
47	42 45 46	mpbir2and	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to sup (A ℝ <) = z$
48	47 18	eqeltrd	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (z \in A \land sup (A ℝ <) - 1 < z)) \to sup (A ℝ <) \in A$
49	12 48	rexlimddv	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in A$

Metamath Proof Explorer

Theorem suprzcl

Proof