Theorem elicod 13423

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103   ∈ wcel 2143   class class class wbr 5110  (class class class)co 7412  ℝ^*cxr 11243   < clt 11244   ≤ cle 11245  [,)cico 13375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-xr 11248  df-ico 13379

This theorem is referenced by:  fprodge1  16051  metustexhalf  24694  ply1degltel  33862  ply1degleel  33863  ply1degltlss  33864  ply1degltdimlem  33990  ply1degltdim  33991  absfico  45914  icoiccdif  46220  icoopn  46221  eliccnelico  46225  eliccelicod  46226  ge0xrre  46227  uzinico  46255  fsumge0cl  46269  limsupresico  46394  limsuppnfdlem  46395  limsupmnflem  46414  liminfresico  46465  limsup10exlem  46466  liminflelimsupuz  46479  xlimmnfvlem2  46527  icocncflimc  46583  fourierdlem41  46842  fourierdlem46  46846  fourierdlem48  46848  fouriersw  46925  fge0iccico  47064  sge0tsms  47074  sge0repnf  47080  sge0pr  47088  sge0iunmptlemre  47109  sge0rpcpnf  47115  sge0rernmpt  47116  sge0ad2en  47125  sge0xaddlem2  47128  voliunsge0lem  47166  meassre  47171  meaiuninclem  47174  omessre  47204  omeiunltfirp  47213  hoiprodcl  47241  hoicvr  47242  ovnsubaddlem1  47264  hoiprodcl3  47274  hoidmvcl  47276  hoidmv1lelem3  47287  hoidmvlelem3  47291  hoidmvlelem5  47293  hspdifhsp  47310  hoiqssbllem1  47316  hoiqssbllem2  47317  hspmbllem2  47321  volicorege0  47331  ovolval5lem1  47346  iunhoiioolem  47369  preimaicomnf  47405  mod42tp1mod8  48331  eenglngeehlnmlem2  49495  itscnhlinecirc02p  49542