ioorcl2

Description: An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015)

		Ref	Expression
	Assertion	ioorcl2	$⊢ ((A, B) \neq \emptyset \land {vol}^{*} ((A, B)) \in ℝ) \to (A \in ℝ \land B \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ (A, B) \neq \emptyset \leftrightarrow \exists z z \in (A, B)$
2		elioore	$⊢ z \in (A, B) \to z \in ℝ$
3	2	adantr	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to z \in ℝ$
4		peano2re	$⊢ {vol}^{} ((A, B)) \in ℝ \to {vol}^{} ((A, B)) + 1 \in ℝ$
5	4	adantl	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((A, B)) + 1 \in ℝ$
6	3 5	resubcld	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z - ({vol}^{} ((A, B)) + 1) \in ℝ$
7	6	rexrd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z - ({vol}^{} ((A, B)) + 1) \in ℝ^{*}$
8		eliooxr	$⊢ z \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{})$
9	8	adantr	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (A \in ℝ^{} \land B \in ℝ^{*})$
10	9	simpld	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to A \in ℝ^{}$
11	3	rexrd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z \in ℝ^{}$
12		ltp1	$⊢ {vol}^{} ((A, B)) \in ℝ \to {vol}^{} ((A, B)) < {vol}^{*} ((A, B)) + 1$
13	12	adantl	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((A, B)) < {vol}^{*} ((A, B)) + 1$
14		0red	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to 0 \in ℝ$
15		simpr	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((A, B)) \in ℝ$
16		ioossre	$⊢ (A, B) \subseteq ℝ$
17		ovolge0	$⊢ (A, B) \subseteq ℝ \to 0 \leq {vol}^{*} ((A, B))$
18	16 17	mp1i	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to 0 \leq {vol}^{} ((A, B))$
19		lep1	$⊢ {vol}^{} ((A, B)) \in ℝ \to {vol}^{} ((A, B)) \leq {vol}^{*} ((A, B)) + 1$
20	19	adantl	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((A, B)) \leq {vol}^{*} ((A, B)) + 1$
21	14 15 5 18 20	letrd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to 0 \leq {vol}^{} ((A, B)) + 1$
22	3 5	subge02d	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (0 \leq {vol}^{} ((A, B)) + 1 \leftrightarrow z - ({vol}^{*} ((A, B)) + 1) \leq z)$
23	21 22	mpbid	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z - ({vol}^{} ((A, B)) + 1) \leq z$
24		ovolioo	$⊢ (z - ({vol}^{} ((A, B)) + 1) \in ℝ \land z \in ℝ \land z - ({vol}^{} ((A, B)) + 1) \leq z) \to {vol}^{} ((z - ({vol}^{} ((A, B)) + 1), z)) = z - (z - ({vol}^{*} ((A, B)) + 1))$
25	6 3 23 24	syl3anc	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((z - ({vol}^{} ((A, B)) + 1), z)) = z - (z - ({vol}^{} ((A, B)) + 1))$
26	3	recnd	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to z \in ℂ$
27	5	recnd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((A, B)) + 1 \in ℂ$
28	26 27	nncand	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z - (z - ({vol}^{} ((A, B)) + 1)) = {vol}^{*} ((A, B)) + 1$
29	25 28	eqtrd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((z - ({vol}^{} ((A, B)) + 1), z)) = {vol}^{} ((A, B)) + 1$
30	29	adantr	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land A \leq z - ({vol}^{} ((A, B)) + 1)) \to {vol}^{} ((z - ({vol}^{} ((A, B)) + 1), z)) = {vol}^{*} ((A, B)) + 1$
31		iooss1	$⊢ (A \in ℝ^{} \land A \leq z - ({vol}^{} ((A, B)) + 1)) \to (z - ({vol}^{*} ((A, B)) + 1), z) \subseteq (A, z)$
32	10 31	sylan	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land A \leq z - ({vol}^{} ((A, B)) + 1)) \to (z - ({vol}^{*} ((A, B)) + 1), z) \subseteq (A, z)$
33	9	simprd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to B \in ℝ^{}$
34		eliooord	$⊢ z \in (A, B) \to (A < z \land z < B)$
35	34	adantr	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to (A < z \land z < B)$
36	35	simprd	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to z < B$
37	11 33 36	xrltled	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to z \leq B$
38		iooss2	$⊢ (B \in ℝ^{*} \land z \leq B) \to (A, z) \subseteq (A, B)$
39	33 37 38	syl2anc	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to (A, z) \subseteq (A, B)$
40	39	adantr	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land A \leq z - ({vol}^{} ((A, B)) + 1)) \to (A, z) \subseteq (A, B)$
41	32 40	sstrd	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land A \leq z - ({vol}^{} ((A, B)) + 1)) \to (z - ({vol}^{*} ((A, B)) + 1), z) \subseteq (A, B)$
42		ovolss	$⊢ ((z - ({vol}^{} ((A, B)) + 1), z) \subseteq (A, B) \land (A, B) \subseteq ℝ) \to {vol}^{} ((z - ({vol}^{} ((A, B)) + 1), z)) \leq {vol}^{} ((A, B))$
43	41 16 42	sylancl	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land A \leq z - ({vol}^{} ((A, B)) + 1)) \to {vol}^{} ((z - ({vol}^{} ((A, B)) + 1), z)) \leq {vol}^{*} ((A, B))$
44	30 43	eqbrtrrd	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land A \leq z - ({vol}^{} ((A, B)) + 1)) \to {vol}^{} ((A, B)) + 1 \leq {vol}^{} ((A, B))$
45	44	ex	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (A \leq z - ({vol}^{} ((A, B)) + 1) \to {vol}^{} ((A, B)) + 1 \leq {vol}^{} ((A, B)))$
46	10 7	xrlenltd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (A \leq z - ({vol}^{} ((A, B)) + 1) \leftrightarrow \neg z - ({vol}^{*} ((A, B)) + 1) < A)$
47	5 15	lenltd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to ({vol}^{} ((A, B)) + 1 \leq {vol}^{} ((A, B)) \leftrightarrow \neg {vol}^{} ((A, B)) < {vol}^{*} ((A, B)) + 1)$
48	45 46 47	3imtr3d	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (\neg z - ({vol}^{} ((A, B)) + 1) < A \to \neg {vol}^{} ((A, B)) < {vol}^{} ((A, B)) + 1)$
49	13 48	mt4d	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z - ({vol}^{} ((A, B)) + 1) < A$
50	35	simpld	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to A < z$
51		xrre2	$⊢ ((z - ({vol}^{} ((A, B)) + 1) \in ℝ^{} \land A \in ℝ^{} \land z \in ℝ^{}) \land (z - ({vol}^{*} ((A, B)) + 1) < A \land A < z)) \to A \in ℝ$
52	7 10 11 49 50 51	syl32anc	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to A \in ℝ$
53	3 5	readdcld	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z + {vol}^{} ((A, B)) + 1 \in ℝ$
54	53	rexrd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z + {vol}^{} ((A, B)) + 1 \in ℝ^{*}$
55	3 5	addge01d	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (0 \leq {vol}^{} ((A, B)) + 1 \leftrightarrow z \leq z + {vol}^{*} ((A, B)) + 1)$
56	21 55	mpbid	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z \leq z + {vol}^{} ((A, B)) + 1$
57		ovolioo	$⊢ (z \in ℝ \land z + {vol}^{} ((A, B)) + 1 \in ℝ \land z \leq z + {vol}^{} ((A, B)) + 1) \to {vol}^{} ((z, z + {vol}^{} ((A, B)) + 1)) = z + ({vol}^{*} ((A, B)) + 1) - z$
58	3 53 56 57	syl3anc	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((z, z + {vol}^{} ((A, B)) + 1)) = z + ({vol}^{} ((A, B)) + 1) - z$
59	26 27	pncan2d	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to z + ({vol}^{} ((A, B)) + 1) - z = {vol}^{*} ((A, B)) + 1$
60	58 59	eqtrd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to {vol}^{} ((z, z + {vol}^{} ((A, B)) + 1)) = {vol}^{} ((A, B)) + 1$
61	60	adantr	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land z + {vol}^{} ((A, B)) + 1 \leq B) \to {vol}^{} ((z, z + {vol}^{} ((A, B)) + 1)) = {vol}^{*} ((A, B)) + 1$
62		iooss2	$⊢ (B \in ℝ^{} \land z + {vol}^{} ((A, B)) + 1 \leq B) \to (z, z + {vol}^{*} ((A, B)) + 1) \subseteq (z, B)$
63	33 62	sylan	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land z + {vol}^{} ((A, B)) + 1 \leq B) \to (z, z + {vol}^{*} ((A, B)) + 1) \subseteq (z, B)$
64	10 11 50	xrltled	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to A \leq z$
65		iooss1	$⊢ (A \in ℝ^{*} \land A \leq z) \to (z, B) \subseteq (A, B)$
66	10 64 65	syl2anc	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to (z, B) \subseteq (A, B)$
67	66	adantr	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land z + {vol}^{} ((A, B)) + 1 \leq B) \to (z, B) \subseteq (A, B)$
68	63 67	sstrd	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land z + {vol}^{} ((A, B)) + 1 \leq B) \to (z, z + {vol}^{*} ((A, B)) + 1) \subseteq (A, B)$
69		ovolss	$⊢ ((z, z + {vol}^{} ((A, B)) + 1) \subseteq (A, B) \land (A, B) \subseteq ℝ) \to {vol}^{} ((z, z + {vol}^{} ((A, B)) + 1)) \leq {vol}^{} ((A, B))$
70	68 16 69	sylancl	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land z + {vol}^{} ((A, B)) + 1 \leq B) \to {vol}^{} ((z, z + {vol}^{} ((A, B)) + 1)) \leq {vol}^{*} ((A, B))$
71	61 70	eqbrtrrd	$⊢ ((z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \land z + {vol}^{} ((A, B)) + 1 \leq B) \to {vol}^{} ((A, B)) + 1 \leq {vol}^{} ((A, B))$
72	71	ex	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (z + {vol}^{} ((A, B)) + 1 \leq B \to {vol}^{} ((A, B)) + 1 \leq {vol}^{} ((A, B)))$
73	54 33	xrlenltd	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (z + {vol}^{} ((A, B)) + 1 \leq B \leftrightarrow \neg B < z + {vol}^{*} ((A, B)) + 1)$
74	72 73 47	3imtr3d	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to (\neg B < z + {vol}^{} ((A, B)) + 1 \to \neg {vol}^{} ((A, B)) < {vol}^{} ((A, B)) + 1)$
75	13 74	mt4d	$⊢ (z \in (A, B) \land {vol}^{} ((A, B)) \in ℝ) \to B < z + {vol}^{} ((A, B)) + 1$
76		xrre2	$⊢ ((z \in ℝ^{} \land B \in ℝ^{} \land z + {vol}^{} ((A, B)) + 1 \in ℝ^{}) \land (z < B \land B < z + {vol}^{*} ((A, B)) + 1)) \to B \in ℝ$
77	11 33 54 36 75 76	syl32anc	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to B \in ℝ$
78	52 77	jca	$⊢ (z \in (A, B) \land {vol}^{*} ((A, B)) \in ℝ) \to (A \in ℝ \land B \in ℝ)$
79	78	ex	$⊢ z \in (A, B) \to ({vol}^{*} ((A, B)) \in ℝ \to (A \in ℝ \land B \in ℝ))$
80	79	exlimiv	$⊢ \exists z z \in (A, B) \to ({vol}^{*} ((A, B)) \in ℝ \to (A \in ℝ \land B \in ℝ))$
81	1 80	sylbi	$⊢ (A, B) \neq \emptyset \to ({vol}^{*} ((A, B)) \in ℝ \to (A \in ℝ \land B \in ℝ))$
82	81	imp	$⊢ ((A, B) \neq \emptyset \land {vol}^{*} ((A, B)) \in ℝ) \to (A \in ℝ \land B \in ℝ)$

Metamath Proof Explorer

Theorem ioorcl2

Proof