Theorem elicod 13138

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1086   ∈ wcel 2107   class class class wbr 5075  (class class class)co 7284  ℝ^*cxr 11017   < clt 11018   ≤ cle 11019  [,)cico 13090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-xr 11022  df-ico 13094

This theorem is referenced by:  fprodge1  15714  metustexhalf  23721  absfico  42765  icoiccdif  43069  icoopn  43070  eliccnelico  43074  eliccelicod  43075  ge0xrre  43076  uzinico  43105  fsumge0cl  43121  limsupresico  43248  limsuppnfdlem  43249  limsupmnflem  43268  liminfresico  43319  limsup10exlem  43320  liminflelimsupuz  43333  xlimmnfvlem2  43381  icocncflimc  43437  fourierdlem41  43696  fourierdlem46  43700  fourierdlem48  43702  fouriersw  43779  fge0iccico  43915  sge0tsms  43925  sge0repnf  43931  sge0pr  43939  sge0iunmptlemre  43960  sge0rpcpnf  43966  sge0rernmpt  43967  sge0ad2en  43976  sge0xaddlem2  43979  voliunsge0lem  44017  meassre  44022  meaiuninclem  44025  omessre  44055  omeiunltfirp  44064  hoiprodcl  44092  hoicvr  44093  ovnsubaddlem1  44115  hoiprodcl3  44125  hoidmvcl  44127  hoidmv1lelem3  44138  hoidmvlelem3  44142  hoidmvlelem5  44144  hspdifhsp  44161  hoiqssbllem1  44167  hoiqssbllem2  44168  hspmbllem2  44172  volicorege0  44182  ovolval5lem1  44197  iunhoiioolem  44220  preimaicomnf  44256  mod42tp1mod8  45065  eenglngeehlnmlem2  46095  itscnhlinecirc02p  46142