Theorem elicod 13457

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087   ∈ wcel 2108   class class class wbr 5166  (class class class)co 7448  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325  [,)cico 13409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-xr 11328  df-ico 13413

This theorem is referenced by:  fprodge1  16043  metustexhalf  24590  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  ply1degltdimlem  33635  ply1degltdim  33636  absfico  45125  icoiccdif  45442  icoopn  45443  eliccnelico  45447  eliccelicod  45448  ge0xrre  45449  uzinico  45478  fsumge0cl  45494  limsupresico  45621  limsuppnfdlem  45622  limsupmnflem  45641  liminfresico  45692  limsup10exlem  45693  liminflelimsupuz  45706  xlimmnfvlem2  45754  icocncflimc  45810  fourierdlem41  46069  fourierdlem46  46073  fourierdlem48  46075  fouriersw  46152  fge0iccico  46291  sge0tsms  46301  sge0repnf  46307  sge0pr  46315  sge0iunmptlemre  46336  sge0rpcpnf  46342  sge0rernmpt  46343  sge0ad2en  46352  sge0xaddlem2  46355  voliunsge0lem  46393  meassre  46398  meaiuninclem  46401  omessre  46431  omeiunltfirp  46440  hoiprodcl  46468  hoicvr  46469  ovnsubaddlem1  46491  hoiprodcl3  46501  hoidmvcl  46503  hoidmv1lelem3  46514  hoidmvlelem3  46518  hoidmvlelem5  46520  hspdifhsp  46537  hoiqssbllem1  46543  hoiqssbllem2  46544  hspmbllem2  46548  volicorege0  46558  ovolval5lem1  46573  iunhoiioolem  46596  preimaicomnf  46632  mod42tp1mod8  47476  eenglngeehlnmlem2  48472  itscnhlinecirc02p  48519