Theorem elicod 13316

Description: Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
elicod.a	⊢ (𝜑 → 𝐴 ∈ ℝ*)
elicod.b	⊢ (𝜑 → 𝐵 ∈ ℝ*)
elicod.3	⊢ (𝜑 → 𝐶 ∈ ℝ*)
elicod.4	⊢ (𝜑 → 𝐴 ≤ 𝐶)
elicod.5	⊢ (𝜑 → 𝐶 < 𝐵)

Assertion

Ref	Expression
elicod	⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))

Proof of Theorem elicod

Step	Hyp	Ref	Expression
1		elicod.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℝ*)
2		elicod.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
3		elicod.5	. 2 ⊢ (𝜑 → 𝐶 < 𝐵)
4		elicod.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
5		elicod.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
6		elico1 13309	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
7	4, 5, 6	syl2anc 584	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
8	1, 2, 3, 7	mpbir3and 1343	1 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086   ∈ wcel 2109   class class class wbr 5095  (class class class)co 7353  ℝ^*cxr 11167   < clt 11168   ≤ cle 11169  [,)cico 13268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-xr 11172  df-ico 13272

This theorem is referenced by:  fprodge1  15920  metustexhalf  24460  ply1degltel  33536  ply1degleel  33537  ply1degltlss  33538  ply1degltdimlem  33594  ply1degltdim  33595  absfico  45196  icoiccdif  45506  icoopn  45507  eliccnelico  45511  eliccelicod  45512  ge0xrre  45513  uzinico  45541  fsumge0cl  45555  limsupresico  45682  limsuppnfdlem  45683  limsupmnflem  45702  liminfresico  45753  limsup10exlem  45754  liminflelimsupuz  45767  xlimmnfvlem2  45815  icocncflimc  45871  fourierdlem41  46130  fourierdlem46  46134  fourierdlem48  46136  fouriersw  46213  fge0iccico  46352  sge0tsms  46362  sge0repnf  46368  sge0pr  46376  sge0iunmptlemre  46397  sge0rpcpnf  46403  sge0rernmpt  46404  sge0ad2en  46413  sge0xaddlem2  46416  voliunsge0lem  46454  meassre  46459  meaiuninclem  46462  omessre  46492  omeiunltfirp  46501  hoiprodcl  46529  hoicvr  46530  ovnsubaddlem1  46552  hoiprodcl3  46562  hoidmvcl  46564  hoidmv1lelem3  46575  hoidmvlelem3  46579  hoidmvlelem5  46581  hspdifhsp  46598  hoiqssbllem1  46604  hoiqssbllem2  46605  hspmbllem2  46609  volicorege0  46619  ovolval5lem1  46634  iunhoiioolem  46657  preimaicomnf  46693  mod42tp1mod8  47587  eenglngeehlnmlem2  48724  itscnhlinecirc02p  48771