elicoelioo - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > elicoelioo		Structured version Visualization version GIF version

Theorem elicoelioo 31099

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

**Assertion**
Ref	Expression
elicoelioo	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵))))

**Proof of Theorem elicoelioo**
Step	Hyp	Ref	Expression
1		simpl1 1190	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → 𝐴 ∈ ℝ^*)
2		simpl2 1191	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → 𝐵 ∈ ℝ^*)
3		simprl 768	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → 𝐶 ∈ (𝐴[,)𝐵))
4		elico1 13122	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
5	4	biimpa 477	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝐶 ∈ (𝐴[,)𝐵)) → (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))
6	5	simp1d 1141	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 ∈ ℝ^)
7	1, 2, 3, 6	syl21anc 835	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → 𝐶 ∈ ℝ^*)
8	5	simp2d 1142	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶)
9	1, 2, 3, 8	syl21anc 835	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → 𝐴 ≤ 𝐶)
10	1, 2	jca 512	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
11		simprr 770	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → ¬ 𝐶 ∈ (𝐴(,)𝐵))
12	5	simp3d 1143	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 < 𝐵)
13	10, 3, 12	syl2anc 584	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → 𝐶 < 𝐵)
14		elioo1 13119	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
15	14	notbid 318	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (¬ 𝐶 ∈ (𝐴(,)𝐵) ↔ ¬ (𝐶 ∈ ℝ^ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
16	15	biimpa 477	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵)) → ¬ (𝐶 ∈ ℝ^ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
17		3anan32 1096	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ ((𝐶 ∈ ℝ^* ∧ 𝐶 < 𝐵) ∧ 𝐴 < 𝐶))
18	17	notbii 320	. . . . . . . . . . 11 ⊢ (¬ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ ¬ ((𝐶 ∈ ℝ^* ∧ 𝐶 < 𝐵) ∧ 𝐴 < 𝐶))
19		imnan 400	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ ℝ^* ∧ 𝐶 < 𝐵) → ¬ 𝐴 < 𝐶) ↔ ¬ ((𝐶 ∈ ℝ^* ∧ 𝐶 < 𝐵) ∧ 𝐴 < 𝐶))
20	18, 19	bitr4i 277	. . . . . . . . . 10 ⊢ (¬ (𝐶 ∈ ℝ^* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ ((𝐶 ∈ ℝ^* ∧ 𝐶 < 𝐵) → ¬ 𝐴 < 𝐶))
21	16, 20	sylib 217	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵)) → ((𝐶 ∈ ℝ^ ∧ 𝐶 < 𝐵) → ¬ 𝐴 < 𝐶))
22	21	imp 407	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵)) ∧ (𝐶 ∈ ℝ^ ∧ 𝐶 < 𝐵)) → ¬ 𝐴 < 𝐶)
23	10, 11, 7, 13, 22	syl22anc 836	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → ¬ 𝐴 < 𝐶)
24		xeqlelt 31097	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐴 = 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ ¬ 𝐴 < 𝐶)))
25	24	biimpar 478	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) ∧ (𝐴 ≤ 𝐶 ∧ ¬ 𝐴 < 𝐶)) → 𝐴 = 𝐶)
26	1, 7, 9, 23, 25	syl22anc 836	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵))) → 𝐴 = 𝐶)
27	26	ex 413	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ((𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐴 = 𝐶))
28		eqcom 2745	. . . . 5 ⊢ (𝐴 = 𝐶 ↔ 𝐶 = 𝐴)
29	27, 28	syl6ib 250	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ((𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 = 𝐴))
30		pm5.6 999	. . . 4 ⊢ (((𝐶 ∈ (𝐴[,)𝐵) ∧ ¬ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 = 𝐴) ↔ (𝐶 ∈ (𝐴[,)𝐵) → (𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐴)))
31	29, 30	sylib 217	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → (𝐶 ∈ (𝐴[,)𝐵) → (𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐴)))
32		orcom 867	. . 3 ⊢ ((𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐴) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵)))
33	31, 32	syl6ib 250	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → (𝐶 ∈ (𝐴[,)𝐵) → (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵))))
34		simpr 485	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐶 = 𝐴)
35		simpl1 1190	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐴 ∈ ℝ^*)
36	34, 35	eqeltrd 2839	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐶 ∈ ℝ^*)
37	35	xrleidd 12886	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐴 ≤ 𝐴)
38	37, 34	breqtrrd 5102	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐴 ≤ 𝐶)
39		simpl3 1192	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐴 < 𝐵)
40	34, 39	eqbrtrd 5096	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐶 < 𝐵)
41		simpl2 1191	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐵 ∈ ℝ^*)
42	35, 41, 4	syl2anc 584	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
43	36, 38, 40, 42	mpbir3and 1341	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 = 𝐴) → 𝐶 ∈ (𝐴[,)𝐵))
44		ioossico 13170	. . . . 5 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵)
45		simpr 485	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ (𝐴(,)𝐵))
46	44, 45	sselid 3919	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ (𝐴[,)𝐵))
47	43, 46	jaodan 955	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) ∧ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵))) → 𝐶 ∈ (𝐴[,)𝐵))
48	47	ex 413	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ((𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ (𝐴[,)𝐵)))
49	33, 48	impbid 211	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 class class class wbr 5074 (class class class)co 7275 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 (,)cioo 13079 [,)cico 13081

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-pre-lttri 10945 ax-pre-lttrn 10946

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-po 5503 df-so 5504 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-ov 7278 df-oprab 7279 df-mpo 7280 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-ioo 13083 df-ico 13085

This theorem is referenced by: xrge0mulc1cn 31891

W3C validator