iocinif

Description: Relate intersection of two open-below, closed-above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017)

		Ref	Expression
	Assertion	iocinif	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A, C] \cap (B, C] = if (A < B, (B, C], (A, C])$

Proof

Step	Hyp	Ref	Expression
1		exmid	$⊢ (A < B \lor \neg A < B)$
2		xrltle	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to A \leq B)$
3	2	imp	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to A \leq B$
4	3	3adantl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A < B) \to A \leq B$
5		iocinioc2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (A, C] \cap (B, C] = (B, C]$
6	4 5	syldan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A < B) \to (A, C] \cap (B, C] = (B, C]$
7	6	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A < B \to (A, C] \cap (B, C] = (B, C])$
8	7	ancld	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A < B \to (A < B \land (A, C] \cap (B, C] = (B, C]))$
9		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land \neg A < B) \to B \in ℝ^{}$
10		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land \neg A < B) \to A \in ℝ^{}$
11		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land \neg A < B) \to \neg A < B$
12		xrlenlt	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to (B \leq A \leftrightarrow \neg A < B)$
13	12	biimpar	$⊢ ((B \in ℝ^{} \land A \in ℝ^{}) \land \neg A < B) \to B \leq A$
14	9 10 11 13	syl21anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land \neg A < B) \to B \leq A$
15		3ancoma	$⊢ (B \in ℝ^{} \land A \in ℝ^{} \land C \in ℝ^{}) \leftrightarrow (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{})$
16		incom	$⊢ (B, C] \cap (A, C] = (A, C] \cap (B, C]$
17		iocinioc2	$⊢ ((B \in ℝ^{} \land A \in ℝ^{} \land C \in ℝ^{*}) \land B \leq A) \to (B, C] \cap (A, C] = (A, C]$
18	16 17	syl5eqr	$⊢ ((B \in ℝ^{} \land A \in ℝ^{} \land C \in ℝ^{*}) \land B \leq A) \to (A, C] \cap (B, C] = (A, C]$
19	15 18	sylanbr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land B \leq A) \to (A, C] \cap (B, C] = (A, C]$
20	14 19	syldan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land \neg A < B) \to (A, C] \cap (B, C] = (A, C]$
21	20	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (\neg A < B \to (A, C] \cap (B, C] = (A, C])$
22	21	ancld	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (\neg A < B \to (\neg A < B \land (A, C] \cap (B, C] = (A, C]))$
23	8 22	orim12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \lor \neg A < B) \to ((A < B \land (A, C] \cap (B, C] = (B, C]) \lor (\neg A < B \land (A, C] \cap (B, C] = (A, C])))$
24	1 23	mpi	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \land (A, C] \cap (B, C] = (B, C]) \lor (\neg A < B \land (A, C] \cap (B, C] = (A, C]))$
25		eqif	$⊢ (A, C] \cap (B, C] = if (A < B, (B, C], (A, C]) \leftrightarrow ((A < B \land (A, C] \cap (B, C] = (B, C]) \lor (\neg A < B \land (A, C] \cap (B, C] = (A, C]))$
26	24 25	sylibr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A, C] \cap (B, C] = if (A < B, (B, C], (A, C])$

Metamath Proof Explorer

Theorem iocinif

Proof