Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  icoltub Structured version   Visualization version   GIF version

Theorem icoltub 41936
Description: An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
icoltub ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 < 𝐵)

Proof of Theorem icoltub
StepHypRef Expression
1 elico1 12760 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝐶𝐶 < 𝐵)))
2 simp3 1134 . . 3 ((𝐶 ∈ ℝ*𝐴𝐶𝐶 < 𝐵) → 𝐶 < 𝐵)
31, 2syl6bi 255 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) → 𝐶 < 𝐵))
433impia 1113 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 < 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083  wcel 2114   class class class wbr 5042  (class class class)co 7133  *cxr 10652   < clt 10653  cle 10654  [,)cico 12719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pr 5306  ax-un 7439  ax-cnex 10571  ax-resscn 10572
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-iota 6290  df-fun 6333  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-xr 10657  df-ico 12723
This theorem is referenced by:  icoopn  41953  icoub  41954  icoltubd  41973  ltmod  42071  limcresioolb  42076  fourierdlem41  42581  fourierdlem43  42583  fourierdlem46  42585  fourierdlem48  42587  fouriersw  42664  hoidmv1lelem2  43022  hoidmvlelem2  43026  hspdifhsp  43046  hspmbllem2  43057  iinhoiicclem  43103  preimaicomnf  43138
  Copyright terms: Public domain W3C validator