Theorem elicod 13396

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1097   ∈ wcel 2141   class class class wbr 5099  (class class class)co 7392  ℝ^*cxr 11212   < clt 11213   ≤ cle 11214  [,)cico 13348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389  ax-un 7714  ax-cnex 11126  ax-resscn 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-iota 6473  df-fun 6519  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-xr 11217  df-ico 13352

This theorem is referenced by:  fprodge1  16008  metustexhalf  24596  ply1degltel  33751  ply1degleel  33752  ply1degltlss  33753  ply1degltdimlem  33880  ply1degltdim  33881  absfico  45758  icoiccdif  46064  icoopn  46065  eliccnelico  46069  eliccelicod  46070  ge0xrre  46071  uzinico  46099  fsumge0cl  46113  limsupresico  46238  limsuppnfdlem  46239  limsupmnflem  46258  liminfresico  46309  limsup10exlem  46310  liminflelimsupuz  46323  xlimmnfvlem2  46371  icocncflimc  46427  fourierdlem41  46686  fourierdlem46  46690  fourierdlem48  46692  fouriersw  46769  fge0iccico  46908  sge0tsms  46918  sge0repnf  46924  sge0pr  46932  sge0iunmptlemre  46953  sge0rpcpnf  46959  sge0rernmpt  46960  sge0ad2en  46969  sge0xaddlem2  46972  voliunsge0lem  47010  meassre  47015  meaiuninclem  47018  omessre  47048  omeiunltfirp  47057  hoiprodcl  47085  hoicvr  47086  ovnsubaddlem1  47108  hoiprodcl3  47118  hoidmvcl  47120  hoidmv1lelem3  47131  hoidmvlelem3  47135  hoidmvlelem5  47137  hspdifhsp  47154  hoiqssbllem1  47160  hoiqssbllem2  47161  hspmbllem2  47165  volicorege0  47175  ovolval5lem1  47190  iunhoiioolem  47213  preimaicomnf  47249  mod42tp1mod8  48175  eenglngeehlnmlem2  49324  itscnhlinecirc02p  49371