elico2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elico2		Structured version Visualization version GIF version

Theorem elico2 13305

Description: Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)

**Assertion**
Ref	Expression
elico2	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))

**Proof of Theorem elico2**
Step	Hyp	Ref	Expression
1		rexr 11153	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
2		elico1 13283	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
3	1, 2	sylan 580	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
4		mnfxr 11164	. . . . . . . 8 ⊢ -∞ ∈ ℝ^*
5	4	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ ∈ ℝ^*)
6	1	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐴 ∈ ℝ^*)
7		simpr1 1195	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 ∈ ℝ^*)
8		mnflt 13017	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
9	8	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ < 𝐴)
10		simpr2 1196	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐴 ≤ 𝐶)
11	5, 6, 7, 9, 10	xrltletrd 13055	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ < 𝐶)
12		simplr 768	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐵 ∈ ℝ^*)
13		pnfxr 11161	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
14	13	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → +∞ ∈ ℝ^*)
15		simpr3 1197	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 < 𝐵)
16		pnfge 13024	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ≤ +∞)
17	16	ad2antlr 727	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐵 ≤ +∞)
18	7, 12, 14, 15, 17	xrltletrd 13055	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 < +∞)
19		xrrebnd 13062	. . . . . . 7 ⊢ (𝐶 ∈ ℝ^* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
20	7, 19	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
21	11, 18, 20	mpbir2and 713	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 ∈ ℝ)
22	21, 10, 15	3jca 1128	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))
23	22	ex 412	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) → ((𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
24		rexr 11153	. . . 4 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
25	24	3anim1i 1152	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) → (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))
26	23, 25	impbid1 225	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) → ((𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
27	3, 26	bitrd 279	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∈ wcel 2111 class class class wbr 5086 (class class class)co 7341 ℝcr 11000 +∞cpnf 11138 -∞cmnf 11139 ℝ^*cxr 11140 < clt 11141 ≤ cle 11142 [,)cico 13242

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-cnex 11057 ax-resscn 11058 ax-pre-lttri 11075 ax-pre-lttrn 11076

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5506 df-po 5519 df-so 5520 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-ov 7344 df-oprab 7345 df-mpo 7346 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-ico 13246

This theorem is referenced by: icossre 13323 elicopnf 13340 icoshft 13368 modelico 13780 muladdmodid 13812 icodiamlt 15340 fprodge0 15895 fprodge1 15897 rge0srg 21370 metustexhalf 24466 cnbl0 24683 icoopnst 24858 iocopnst 24859 icopnfcnv 24862 icopnfhmeo 24863 iccpnfcnv 24864 psercnlem2 26356 psercnlem1 26357 psercn 26358 abelth 26373 cosq34lt1 26458 tanord1 26468 tanord 26469 efopnlem1 26587 logtayl 26591 rlimcnp 26897 rlimcnp2 26898 dchrvmasumlem2 27431 dchrvmasumiflem1 27434 pntlemb 27530 pnt 27547 ubico 32750 xrge0slmod 33305 voliune 34234 volfiniune 34235 dya2icoseg 34282 sibfinima 34344 relowlpssretop 37398 tan2h 37652 itg2addnclem2 37712 binomcxplemdvbinom 44386 binomcxplemcvg 44387 binomcxplemnotnn0 44389 limciccioolb 45661 fourierdlem32 46177 fourierdlem43 46188 fourierdlem63 46207 fourierdlem79 46223 fouriersw 46269 expnegico01 48550 dignnld 48635 eenglngeehlnmlem1 48769 i0oii 48951 sepfsepc 48959

W3C validator