Theorem elicod 13440

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 13433	. . 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 2146   class class class wbr 5114  (class class class)co 7423  ℝ^*cxr 11260   < clt 11261   ≤ cle 11262  [,)cico 13392

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-xr 11265  df-ico 13396

This theorem is used by:  fprodge1  16075  metustexhalf  24750  ply1degltel  33915  ply1degleel  33916  ply1degltlss  33917  ply1degltdimlem  34043  ply1degltdim  34044  absfico  45975  icoiccdif  46281  icoopn  46282  eliccnelico  46286  eliccelicod  46287  ge0xrre  46288  uzinico  46316  fsumge0cl  46330  limsupresico  46455  limsuppnfdlem  46456  limsupmnflem  46475  liminfresico  46526  limsup10exlem  46527  liminflelimsupuz  46540  xlimmnfvlem2  46588  icocncflimc  46644  fourierdlem41  46903  fourierdlem46  46907  fourierdlem48  46909  fouriersw  46986  fge0iccico  47125  sge0tsms  47135  sge0repnf  47141  sge0pr  47149  sge0iunmptlemre  47170  sge0rpcpnf  47176  sge0rernmpt  47177  sge0ad2en  47186  sge0xaddlem2  47189  voliunsge0lem  47227  meassre  47232  meaiuninclem  47235  omessre  47265  omeiunltfirp  47274  hoiprodcl  47302  hoicvr  47303  ovnsubaddlem1  47325  hoiprodcl3  47335  hoidmvcl  47337  hoidmv1lelem3  47348  hoidmvlelem3  47352  hoidmvlelem5  47354  hspdifhsp  47371  hoiqssbllem1  47377  hoiqssbllem2  47378  hspmbllem2  47382  volicorege0  47392  ovolval5lem1  47407  iunhoiioolem  47430  preimaicomnf  47466  mod42tp1mod8  48395  eenglngeehlnmlem2  49559  itscnhlinecirc02p  49606