Theorem elicod 13452

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 13445	. . 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 2145   class class class wbr 5107  (class class class)co 7417  ℝ^*cxr 11270   < clt 11271   ≤ cle 11272  [,)cico 13404

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-xr 11275  df-ico 13408

This theorem is used by:  fprodge1  16088  metustexhalf  24788  ply1degltel  34012  ply1degleel  34013  ply1degltlss  34014  ply1degltdimlem  34140  ply1degltdim  34141  absfico  46056  icoiccdif  46362  icoopn  46363  eliccnelico  46367  eliccelicod  46368  ge0xrre  46369  uzinico  46397  fsumge0cl  46411  limsupresico  46536  limsuppnfdlem  46537  limsupmnflem  46556  liminfresico  46607  limsup10exlem  46608  liminflelimsupuz  46621  xlimmnfvlem2  46669  icocncflimc  46725  fourierdlem41  46984  fourierdlem46  46988  fourierdlem48  46990  fouriersw  47067  fge0iccico  47206  sge0tsms  47216  sge0repnf  47222  sge0pr  47230  sge0iunmptlemre  47251  sge0rpcpnf  47257  sge0rernmpt  47258  sge0ad2en  47267  sge0xaddlem2  47270  voliunsge0lem  47308  meassre  47313  meaiuninclem  47316  omessre  47346  omeiunltfirp  47355  hoiprodcl  47383  hoicvr  47384  ovnsubaddlem1  47406  hoiprodcl3  47416  hoidmvcl  47418  hoidmv1lelem3  47429  hoidmvlelem3  47433  hoidmvlelem5  47435  hspdifhsp  47452  hoiqssbllem1  47458  hoiqssbllem2  47459  hspmbllem2  47463  volicorege0  47473  ovolval5lem1  47488  iunhoiioolem  47511  preimaicomnf  47547  mod42tp1mod8  48513  eenglngeehlnmlem2  49676  itscnhlinecirc02p  49723