Theorem elicod 13553

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103   ∈ wcel 2147   class class class wbr 5106  (class class class)co 7443  ℝ^*cxr 11369   < clt 11370   ≤ cle 11371  [,)cico 13505

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-xr 11374  df-ico 13509

This theorem is used by:  fprodge1  16191  metustexhalf  24905  ply1degltel  34196  ply1degleel  34197  ply1degltlss  34198  ply1degltdimlem  34324  ply1degltdim  34325  absfico  46436  icoiccdif  46741  icoopn  46742  eliccnelico  46746  eliccelicod  46747  ge0xrre  46748  uzinico  46776  fsumge0cl  46790  limsupresico  46915  limsuppnfdlem  46916  limsupmnflem  46935  liminfresico  46986  limsup10exlem  46987  liminflelimsupuz  47000  xlimmnfvlem2  47048  icocncflimc  47104  fourierdlem41  47363  fourierdlem46  47367  fourierdlem48  47369  fouriersw  47446  fge0iccico  47585  sge0tsms  47595  sge0repnf  47601  sge0pr  47609  sge0iunmptlemre  47630  sge0rpcpnf  47636  sge0rernmpt  47637  sge0ad2en  47646  sge0xaddlem2  47649  voliunsge0lem  47687  meassre  47692  meaiuninclem  47695  omessre  47725  omeiunltfirp  47734  hoiprodcl  47762  hoicvr  47763  ovnsubaddlem1  47785  hoiprodcl3  47795  hoidmvcl  47797  hoidmv1lelem3  47808  hoidmvlelem3  47812  hoidmvlelem5  47814  hspdifhsp  47831  hoiqssbllem1  47837  hoiqssbllem2  47838  hspmbllem2  47842  volicorege0  47852  ovolval5lem1  47867  iunhoiioolem  47890  preimaicomnf  47926  mod42tp1mod8  48892  eenglngeehlnmlem2  50056  itscnhlinecirc02p  50102