iooelexlt

Description: An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020)

		Ref	Expression
	Assertion	iooelexlt	$⊢ X \in (A, B) \to \exists y \in (A, B) y < X$

Proof

Step	Hyp	Ref	Expression
1		eliooxr	$⊢ X \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{})$
2	1	simpld	$⊢ X \in (A, B) \to A \in ℝ^{*}$
3		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
4		19.3v	$⊢ \forall y (X \in (A, B) \land A \in ℝ) \leftrightarrow (X \in (A, B) \land A \in ℝ)$
5		ovex	$⊢ \frac{A + X}{2} \in V$
6		nfcv	$⊢ \underline{Ⅎ} y (\frac{A + X}{2})$
7		nfre1	$⊢ Ⅎ y \exists y \in (A, B) y < X$
8		elioore	$⊢ X \in (A, B) \to X \in ℝ$
9		readdcl	$⊢ (A \in ℝ \land X \in ℝ) \to A + X \in ℝ$
10	9	rehalfcld	$⊢ (A \in ℝ \land X \in ℝ) \to \frac{A + X}{2} \in ℝ$
11	8 10	sylan2	$⊢ (A \in ℝ \land X \in (A, B)) \to \frac{A + X}{2} \in ℝ$
12	11	ancoms	$⊢ (X \in (A, B) \land A \in ℝ) \to \frac{A + X}{2} \in ℝ$
13	12	rexrd	$⊢ (X \in (A, B) \land A \in ℝ) \to \frac{A + X}{2} \in ℝ^{*}$
14		eliooord	$⊢ X \in (A, B) \to (A < X \land X < B)$
15	14	simpld	$⊢ X \in (A, B) \to A < X$
16	15	adantr	$⊢ (X \in (A, B) \land A \in ℝ) \to A < X$
17		avglt1	$⊢ (A \in ℝ \land X \in ℝ) \to (A < X \leftrightarrow A < \frac{A + X}{2})$
18	8 17	sylan2	$⊢ (A \in ℝ \land X \in (A, B)) \to (A < X \leftrightarrow A < \frac{A + X}{2})$
19	18	ancoms	$⊢ (X \in (A, B) \land A \in ℝ) \to (A < X \leftrightarrow A < \frac{A + X}{2})$
20	16 19	mpbid	$⊢ (X \in (A, B) \land A \in ℝ) \to A < \frac{A + X}{2}$
21	8	rexrd	$⊢ X \in (A, B) \to X \in ℝ^{*}$
22	21	adantr	$⊢ (X \in (A, B) \land A \in ℝ) \to X \in ℝ^{*}$
23	1	simprd	$⊢ X \in (A, B) \to B \in ℝ^{*}$
24	23	adantr	$⊢ (X \in (A, B) \land A \in ℝ) \to B \in ℝ^{*}$
25		avglt2	$⊢ (A \in ℝ \land X \in ℝ) \to (A < X \leftrightarrow \frac{A + X}{2} < X)$
26	8 25	sylan2	$⊢ (A \in ℝ \land X \in (A, B)) \to (A < X \leftrightarrow \frac{A + X}{2} < X)$
27	26	ancoms	$⊢ (X \in (A, B) \land A \in ℝ) \to (A < X \leftrightarrow \frac{A + X}{2} < X)$
28	16 27	mpbid	$⊢ (X \in (A, B) \land A \in ℝ) \to \frac{A + X}{2} < X$
29	14	simprd	$⊢ X \in (A, B) \to X < B$
30	29	adantr	$⊢ (X \in (A, B) \land A \in ℝ) \to X < B$
31	13 22 24 28 30	xrlttrd	$⊢ (X \in (A, B) \land A \in ℝ) \to \frac{A + X}{2} < B$
32		elioo1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\frac{A + X}{2} \in (A, B) \leftrightarrow (\frac{A + X}{2} \in ℝ^{*} \land A < \frac{A + X}{2} \land \frac{A + X}{2} < B))$
33	1 32	syl	$⊢ X \in (A, B) \to (\frac{A + X}{2} \in (A, B) \leftrightarrow (\frac{A + X}{2} \in ℝ^{*} \land A < \frac{A + X}{2} \land \frac{A + X}{2} < B))$
34	33	adantr	$⊢ (X \in (A, B) \land A \in ℝ) \to (\frac{A + X}{2} \in (A, B) \leftrightarrow (\frac{A + X}{2} \in ℝ^{*} \land A < \frac{A + X}{2} \land \frac{A + X}{2} < B))$
35	13 20 31 34	mpbir3and	$⊢ (X \in (A, B) \land A \in ℝ) \to \frac{A + X}{2} \in (A, B)$
36	35 28	jca	$⊢ (X \in (A, B) \land A \in ℝ) \to (\frac{A + X}{2} \in (A, B) \land \frac{A + X}{2} < X)$
37		eleq1	$⊢ y = \frac{A + X}{2} \to (y \in (A, B) \leftrightarrow \frac{A + X}{2} \in (A, B))$
38		breq1	$⊢ y = \frac{A + X}{2} \to (y < X \leftrightarrow \frac{A + X}{2} < X)$
39	37 38	anbi12d	$⊢ y = \frac{A + X}{2} \to ((y \in (A, B) \land y < X) \leftrightarrow (\frac{A + X}{2} \in (A, B) \land \frac{A + X}{2} < X))$
40	36 39	syl5ibr	$⊢ y = \frac{A + X}{2} \to ((X \in (A, B) \land A \in ℝ) \to (y \in (A, B) \land y < X))$
41		rspe	$⊢ (y \in (A, B) \land y < X) \to \exists y \in (A, B) y < X$
42	40 41	syl6	$⊢ y = \frac{A + X}{2} \to ((X \in (A, B) \land A \in ℝ) \to \exists y \in (A, B) y < X)$
43	6 7 42	spcimgf	$⊢ \frac{A + X}{2} \in V \to (\forall y (X \in (A, B) \land A \in ℝ) \to \exists y \in (A, B) y < X)$
44	5 43	ax-mp	$⊢ \forall y (X \in (A, B) \land A \in ℝ) \to \exists y \in (A, B) y < X$
45	4 44	sylbir	$⊢ (X \in (A, B) \land A \in ℝ) \to \exists y \in (A, B) y < X$
46	45	expcom	$⊢ A \in ℝ \to (X \in (A, B) \to \exists y \in (A, B) y < X)$
47		simpl	$⊢ (X \in (A, B) \land A = +∞) \to X \in (A, B)$
48		oveq1	$⊢ A = +∞ \to (A, B) = (+∞, B)$
49	48	eleq2d	$⊢ A = +∞ \to (X \in (A, B) \leftrightarrow X \in (+∞, B))$
50	49	adantl	$⊢ (X \in (A, B) \land A = +∞) \to (X \in (A, B) \leftrightarrow X \in (+∞, B))$
51		pnfxr	$⊢ +∞ \in ℝ^{*}$
52		elioo2	$⊢ (+∞ \in ℝ^{} \land B \in ℝ^{}) \to (X \in (+∞, B) \leftrightarrow (X \in ℝ \land +∞ < X \land X < B))$
53	51 52	mpan	$⊢ B \in ℝ^{*} \to (X \in (+∞, B) \leftrightarrow (X \in ℝ \land +∞ < X \land X < B))$
54	53	biimpd	$⊢ B \in ℝ^{*} \to (X \in (+∞, B) \to (X \in ℝ \land +∞ < X \land X < B))$
55		elioore	$⊢ X \in (+∞, B) \to X \in ℝ$
56		rexr	$⊢ X \in ℝ \to X \in ℝ^{*}$
57		pnfnlt	$⊢ X \in ℝ^{*} \to \neg +∞ < X$
58	56 57	syl	$⊢ X \in ℝ \to \neg +∞ < X$
59	58	intn3an2d	$⊢ X \in ℝ \to \neg (X \in ℝ \land +∞ < X \land X < B)$
60	55 59	syl	$⊢ X \in (+∞, B) \to \neg (X \in ℝ \land +∞ < X \land X < B)$
61	60	a1i	$⊢ B \in ℝ^{*} \to (X \in (+∞, B) \to \neg (X \in ℝ \land +∞ < X \land X < B))$
62	54 61	pm2.65d	$⊢ B \in ℝ^{*} \to \neg X \in (+∞, B)$
63	23 62	syl	$⊢ X \in (A, B) \to \neg X \in (+∞, B)$
64	63	pm2.21d	$⊢ X \in (A, B) \to (X \in (+∞, B) \to \exists y \in (A, B) y < X)$
65	64	adantr	$⊢ (X \in (A, B) \land A = +∞) \to (X \in (+∞, B) \to \exists y \in (A, B) y < X)$
66	50 65	sylbid	$⊢ (X \in (A, B) \land A = +∞) \to (X \in (A, B) \to \exists y \in (A, B) y < X)$
67	47 66	mpd	$⊢ (X \in (A, B) \land A = +∞) \to \exists y \in (A, B) y < X$
68	67	expcom	$⊢ A = +∞ \to (X \in (A, B) \to \exists y \in (A, B) y < X)$
69		19.3v	$⊢ \forall y (X \in (A, B) \land A = −∞) \leftrightarrow (X \in (A, B) \land A = −∞)$
70		ovex	$⊢ X - 1 \in V$
71		nfcv	$⊢ \underline{Ⅎ} y (X - 1)$
72		peano2rem	$⊢ X \in ℝ \to X - 1 \in ℝ$
73	8 72	syl	$⊢ X \in (A, B) \to X - 1 \in ℝ$
74		mnflt	$⊢ X - 1 \in ℝ \to −∞ < X - 1$
75	73 74	syl	$⊢ X \in (A, B) \to −∞ < X - 1$
76	73	rexrd	$⊢ X \in (A, B) \to X - 1 \in ℝ^{*}$
77	8	ltm1d	$⊢ X \in (A, B) \to X - 1 < X$
78	76 21 23 77 29	xrlttrd	$⊢ X \in (A, B) \to X - 1 < B$
79		mnfxr	$⊢ −∞ \in ℝ^{*}$
80		elioo2	$⊢ (−∞ \in ℝ^{} \land B \in ℝ^{}) \to (X - 1 \in (−∞, B) \leftrightarrow (X - 1 \in ℝ \land −∞ < X - 1 \land X - 1 < B))$
81	79 80	mpan	$⊢ B \in ℝ^{*} \to (X - 1 \in (−∞, B) \leftrightarrow (X - 1 \in ℝ \land −∞ < X - 1 \land X - 1 < B))$
82	23 81	syl	$⊢ X \in (A, B) \to (X - 1 \in (−∞, B) \leftrightarrow (X - 1 \in ℝ \land −∞ < X - 1 \land X - 1 < B))$
83	73 75 78 82	mpbir3and	$⊢ X \in (A, B) \to X - 1 \in (−∞, B)$
84	83	adantr	$⊢ (X \in (A, B) \land A = −∞) \to X - 1 \in (−∞, B)$
85		oveq1	$⊢ A = −∞ \to (A, B) = (−∞, B)$
86	85	eleq2d	$⊢ A = −∞ \to (X - 1 \in (A, B) \leftrightarrow X - 1 \in (−∞, B))$
87	86	adantl	$⊢ (X \in (A, B) \land A = −∞) \to (X - 1 \in (A, B) \leftrightarrow X - 1 \in (−∞, B))$
88	84 87	mpbird	$⊢ (X \in (A, B) \land A = −∞) \to X - 1 \in (A, B)$
89	77	adantr	$⊢ (X \in (A, B) \land A = −∞) \to X - 1 < X$
90	88 89	jca	$⊢ (X \in (A, B) \land A = −∞) \to (X - 1 \in (A, B) \land X - 1 < X)$
91	90	adantr	$⊢ ((X \in (A, B) \land A = −∞) \land y = X - 1) \to (X - 1 \in (A, B) \land X - 1 < X)$
92		eleq1	$⊢ y = X - 1 \to (y \in (A, B) \leftrightarrow X - 1 \in (A, B))$
93		breq1	$⊢ y = X - 1 \to (y < X \leftrightarrow X - 1 < X)$
94	92 93	anbi12d	$⊢ y = X - 1 \to ((y \in (A, B) \land y < X) \leftrightarrow (X - 1 \in (A, B) \land X - 1 < X))$
95	94	adantl	$⊢ ((X \in (A, B) \land A = −∞) \land y = X - 1) \to ((y \in (A, B) \land y < X) \leftrightarrow (X - 1 \in (A, B) \land X - 1 < X))$
96	91 95	mpbird	$⊢ ((X \in (A, B) \land A = −∞) \land y = X - 1) \to (y \in (A, B) \land y < X)$
97	96 41	syl	$⊢ ((X \in (A, B) \land A = −∞) \land y = X - 1) \to \exists y \in (A, B) y < X$
98	97	expcom	$⊢ y = X - 1 \to ((X \in (A, B) \land A = −∞) \to \exists y \in (A, B) y < X)$
99	71 7 98	spcimgf	$⊢ X - 1 \in V \to (\forall y (X \in (A, B) \land A = −∞) \to \exists y \in (A, B) y < X)$
100	70 99	ax-mp	$⊢ \forall y (X \in (A, B) \land A = −∞) \to \exists y \in (A, B) y < X$
101	69 100	sylbir	$⊢ (X \in (A, B) \land A = −∞) \to \exists y \in (A, B) y < X$
102	101	expcom	$⊢ A = −∞ \to (X \in (A, B) \to \exists y \in (A, B) y < X)$
103	46 68 102	3jaoi	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \to (X \in (A, B) \to \exists y \in (A, B) y < X)$
104	3 103	sylbi	$⊢ A \in ℝ^{*} \to (X \in (A, B) \to \exists y \in (A, B) y < X)$
105	2 104	mpcom	$⊢ X \in (A, B) \to \exists y \in (A, B) y < X$

Metamath Proof Explorer

Theorem iooelexlt

Proof