Theorem elicod 13419

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086   ∈ wcel 2107   class class class wbr 5123  (class class class)co 7413  ℝ^*cxr 11276   < clt 11277   ≤ cle 11278  [,)cico 13371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-iota 6494  df-fun 6543  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-xr 11281  df-ico 13375

This theorem is referenced by:  fprodge1  16013  metustexhalf  24513  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ply1degltdimlem  33608  ply1degltdim  33609  absfico  45180  icoiccdif  45494  icoopn  45495  eliccnelico  45499  eliccelicod  45500  ge0xrre  45501  uzinico  45530  fsumge0cl  45545  limsupresico  45672  limsuppnfdlem  45673  limsupmnflem  45692  liminfresico  45743  limsup10exlem  45744  liminflelimsupuz  45757  xlimmnfvlem2  45805  icocncflimc  45861  fourierdlem41  46120  fourierdlem46  46124  fourierdlem48  46126  fouriersw  46203  fge0iccico  46342  sge0tsms  46352  sge0repnf  46358  sge0pr  46366  sge0iunmptlemre  46387  sge0rpcpnf  46393  sge0rernmpt  46394  sge0ad2en  46403  sge0xaddlem2  46406  voliunsge0lem  46444  meassre  46449  meaiuninclem  46452  omessre  46482  omeiunltfirp  46491  hoiprodcl  46519  hoicvr  46520  ovnsubaddlem1  46542  hoiprodcl3  46552  hoidmvcl  46554  hoidmv1lelem3  46565  hoidmvlelem3  46569  hoidmvlelem5  46571  hspdifhsp  46588  hoiqssbllem1  46594  hoiqssbllem2  46595  hspmbllem2  46599  volicorege0  46609  ovolval5lem1  46624  iunhoiioolem  46647  preimaicomnf  46683  mod42tp1mod8  47547  eenglngeehlnmlem2  48617  itscnhlinecirc02p  48664