Theorem elicod 13339

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 13332	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
7	4, 5, 6	syl2anc 585	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
8	1, 2, 3, 7	mpbir3and 1344	1 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5086  (class class class)co 7360  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171  [,)cico 13291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-xr 11174  df-ico 13295

This theorem is referenced by:  fprodge1  15951  metustexhalf  24531  ply1degltel  33669  ply1degleel  33670  ply1degltlss  33671  ply1degltdimlem  33782  ply1degltdim  33783  absfico  45665  icoiccdif  45972  icoopn  45973  eliccnelico  45977  eliccelicod  45978  ge0xrre  45979  uzinico  46007  fsumge0cl  46021  limsupresico  46146  limsuppnfdlem  46147  limsupmnflem  46166  liminfresico  46217  limsup10exlem  46218  liminflelimsupuz  46231  xlimmnfvlem2  46279  icocncflimc  46335  fourierdlem41  46594  fourierdlem46  46598  fourierdlem48  46600  fouriersw  46677  fge0iccico  46816  sge0tsms  46826  sge0repnf  46832  sge0pr  46840  sge0iunmptlemre  46861  sge0rpcpnf  46867  sge0rernmpt  46868  sge0ad2en  46877  sge0xaddlem2  46880  voliunsge0lem  46918  meassre  46923  meaiuninclem  46926  omessre  46956  omeiunltfirp  46965  hoiprodcl  46993  hoicvr  46994  ovnsubaddlem1  47016  hoiprodcl3  47026  hoidmvcl  47028  hoidmv1lelem3  47039  hoidmvlelem3  47043  hoidmvlelem5  47045  hspdifhsp  47062  hoiqssbllem1  47068  hoiqssbllem2  47069  hspmbllem2  47073  volicorege0  47083  ovolval5lem1  47098  iunhoiioolem  47121  preimaicomnf  47157  mod42tp1mod8  48077  eenglngeehlnmlem2  49226  itscnhlinecirc02p  49273