MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  icogelb Structured version   Visualization version   GIF version

Theorem icogelb 12437
Description: An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
icogelb ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,)𝐵)) → 𝐴𝐶)

Proof of Theorem icogelb
StepHypRef Expression
1 elico1 12430 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝐶𝐶 < 𝐵)))
2 simp2 1160 . . 3 ((𝐶 ∈ ℝ*𝐴𝐶𝐶 < 𝐵) → 𝐴𝐶)
31, 2syl6bi 244 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) → 𝐴𝐶))
433impia 1138 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,)𝐵)) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100  wcel 2155   class class class wbr 4837  (class class class)co 6868  *cxr 10352   < clt 10353  cle 10354  [,)cico 12389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pr 5090  ax-un 7173  ax-cnex 10271  ax-resscn 10272
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-sbc 3628  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-br 4838  df-opab 4900  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-iota 6058  df-fun 6097  df-fv 6103  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-xr 10357  df-ico 12393
This theorem is referenced by:  fprodge0  14938  fprodge1  14940  hgt750lemf  31050  xralrple2  40044  icoopn  40226  icogelbd  40259  fsumge0cl  40279  limcresioolb  40349  fourierdlem41  40838  fourierdlem43  40840  fourierdlem46  40842  fourierdlem48  40844  fouriersw  40921  sge0isum  41117  sge0ad2en  41121  sge0uzfsumgt  41134  sge0seq  41136  sge0reuz  41137  hoidmv1lelem2  41282  hoidmvlelem1  41285  hoidmvlelem2  41286  ovnhoilem1  41291  hspdifhsp  41306  hspmbllem2  41317  iinhoiicclem  41363
  Copyright terms: Public domain W3C validator