Theorem elicod 13363

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 13356	. . 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 5110  (class class class)co 7390  ℝ^*cxr 11214   < clt 11215   ≤ cle 11216  [,)cico 13315

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-xr 11219  df-ico 13319

This theorem is referenced by:  fprodge1  15968  metustexhalf  24451  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  ply1degltdimlem  33625  ply1degltdim  33626  absfico  45219  icoiccdif  45529  icoopn  45530  eliccnelico  45534  eliccelicod  45535  ge0xrre  45536  uzinico  45564  fsumge0cl  45578  limsupresico  45705  limsuppnfdlem  45706  limsupmnflem  45725  liminfresico  45776  limsup10exlem  45777  liminflelimsupuz  45790  xlimmnfvlem2  45838  icocncflimc  45894  fourierdlem41  46153  fourierdlem46  46157  fourierdlem48  46159  fouriersw  46236  fge0iccico  46375  sge0tsms  46385  sge0repnf  46391  sge0pr  46399  sge0iunmptlemre  46420  sge0rpcpnf  46426  sge0rernmpt  46427  sge0ad2en  46436  sge0xaddlem2  46439  voliunsge0lem  46477  meassre  46482  meaiuninclem  46485  omessre  46515  omeiunltfirp  46524  hoiprodcl  46552  hoicvr  46553  ovnsubaddlem1  46575  hoiprodcl3  46585  hoidmvcl  46587  hoidmv1lelem3  46598  hoidmvlelem3  46602  hoidmvlelem5  46604  hspdifhsp  46621  hoiqssbllem1  46627  hoiqssbllem2  46628  hspmbllem2  46632  volicorege0  46642  ovolval5lem1  46657  iunhoiioolem  46680  preimaicomnf  46716  mod42tp1mod8  47607  eenglngeehlnmlem2  48731  itscnhlinecirc02p  48778