eliccelico

Description: Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017)

		Ref	Expression
	Assertion	eliccelico	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (C \in [A, B] \leftrightarrow (C \in [A, B) \lor C = B))$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to A \in ℝ^{*}$
2		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to B \in ℝ^{*}$
3		simprl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to C \in [A, B]$
4		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in [A, B] \leftrightarrow (C \in ℝ^{*} \land A \leq C \land C \leq B))$
5	4	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B]) \to (C \in ℝ^{*} \land A \leq C \land C \leq B)$
6	5	simp1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B]) \to C \in ℝ^{*}$
7	1 2 3 6	syl21anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to C \in ℝ^{*}$
8	5	simp3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B]) \to C \leq B$
9	1 2 3 8	syl21anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to C \leq B$
10	1 2	jca	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to (A \in ℝ^{} \land B \in ℝ^{})$
11		simprr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to \neg C \in [A, B)$
12	5	simp2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B]) \to A \leq C$
13	10 3 12	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to A \leq C$
14		elico1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in [A, B) \leftrightarrow (C \in ℝ^{*} \land A \leq C \land C < B))$
15	14	notbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg C \in [A, B) \leftrightarrow \neg (C \in ℝ^{*} \land A \leq C \land C < B))$
16	15	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg C \in [A, B)) \to \neg (C \in ℝ^{*} \land A \leq C \land C < B)$
17		df-3an	$⊢ (C \in ℝ^{} \land A \leq C \land C < B) \leftrightarrow ((C \in ℝ^{} \land A \leq C) \land C < B)$
18	17	notbii	$⊢ \neg (C \in ℝ^{} \land A \leq C \land C < B) \leftrightarrow \neg ((C \in ℝ^{} \land A \leq C) \land C < B)$
19		imnan	$⊢ ((C \in ℝ^{} \land A \leq C) \to \neg C < B) \leftrightarrow \neg ((C \in ℝ^{} \land A \leq C) \land C < B)$
20	18 19	bitr4i	$⊢ \neg (C \in ℝ^{} \land A \leq C \land C < B) \leftrightarrow ((C \in ℝ^{} \land A \leq C) \to \neg C < B)$
21	16 20	sylib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg C \in [A, B)) \to ((C \in ℝ^{*} \land A \leq C) \to \neg C < B)$
22	21	imp	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg C \in [A, B)) \land (C \in ℝ^{*} \land A \leq C)) \to \neg C < B$
23	10 11 7 13 22	syl22anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to \neg C < B$
24		xeqlelt	$⊢ (C \in ℝ^{} \land B \in ℝ^{}) \to (C = B \leftrightarrow (C \leq B \land \neg C < B))$
25	24	biimpar	$⊢ ((C \in ℝ^{} \land B \in ℝ^{}) \land (C \leq B \land \neg C < B)) \to C = B$
26	7 2 9 23 25	syl22anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B] \land \neg C \in [A, B))) \to C = B$
27	26	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to ((C \in [A, B] \land \neg C \in [A, B)) \to C = B)$
28		pm5.6	$⊢ ((C \in [A, B] \land \neg C \in [A, B)) \to C = B) \leftrightarrow (C \in [A, B] \to (C \in [A, B) \lor C = B))$
29	27 28	sylib	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (C \in [A, B] \to (C \in [A, B) \lor C = B))$
30		icossicc	$⊢ [A, B) \subseteq [A, B]$
31		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C \in [A, B)) \to C \in [A, B)$
32	30 31	sselid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C \in [A, B)) \to C \in [A, B]$
33		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to C = B$
34		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to B \in ℝ^{*}$
35	33 34	eqeltrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to C \in ℝ^{*}$
36		simpl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to A \leq B$
37	36 33	breqtrrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to A \leq C$
38	34	xrleidd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to B \leq B$
39	33 38	eqbrtrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to C \leq B$
40		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to A \in ℝ^{*}$
41	40 34 4	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to (C \in [A, B] \leftrightarrow (C \in ℝ^{*} \land A \leq C \land C \leq B))$
42	35 37 39 41	mpbir3and	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land C = B) \to C \in [A, B]$
43	32 42	jaodan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land (C \in [A, B) \lor C = B)) \to C \in [A, B]$
44	43	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to ((C \in [A, B) \lor C = B) \to C \in [A, B])$
45	29 44	impbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (C \in [A, B] \leftrightarrow (C \in [A, B) \lor C = B))$

Metamath Proof Explorer

Theorem eliccelico

Proof