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

Theorem iccgelb 11720
Description: An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.)
Assertion
Ref Expression
iccgelb  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  ( A [,] B
) )  ->  A  <_  C )

Proof of Theorem iccgelb
StepHypRef Expression
1 elicc1 11709 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( C  e.  ( A [,] B )  <->  ( C  e.  RR*  /\  A  <_  C  /\  C  <_  B
) ) )
21biimpa 491 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  C  e.  ( A [,] B ) )  ->  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )
32simp2d 1027 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  C  e.  ( A [,] B ) )  ->  A  <_  C
)
433impa 1210 1  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  ( A [,] B
) )  ->  A  <_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991    e. wcel 1898   class class class wbr 4416  (class class class)co 6315   RR*cxr 9700    <_ cle 9702   [,]cicc 11667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-iota 5565  df-fun 5603  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-xr 9705  df-icc 11671
This theorem is referenced by:  supicc  11809  ttgcontlem1  24964  xrge0infss  28389  xrge0infssOLD  28390  xrge0addgt0  28503  xrge0adddir  28504  esumcst  28933  esumpinfval  28943  oms0  29174  oms0OLD  29178  probmeasb  29312  broucube  32019  areaquad  36146  lefldiveq  37544  xadd0ge  37580  xrge0nemnfd  37593  eliccelioc  37660  iccintsng  37662  ge0nemnf2  37668  eliccnelico  37669  eliccelicod  37670  ge0xrre  37671  inficc  37674  iccdificc  37679  cncfiooiccre  37811  iblspltprt  37888  itgioocnicc  37892  itgspltprt  37894  itgiccshift  37895  fourierdlem1  38008  fourierdlem20  38027  fourierdlem24  38031  fourierdlem25  38032  fourierdlem27  38034  fourierdlem43  38052  fourierdlem44  38053  fourierdlem50  38058  fourierdlem51  38059  fourierdlem52  38060  fourierdlem64  38072  fourierdlem73  38081  fourierdlem76  38084  fourierdlem81  38089  fourierdlem92  38100  fourierdlem102  38110  fourierdlem103  38111  fourierdlem104  38112  fourierdlem114  38122  salgencntex  38240  fge0iccico  38250  gsumge0cl  38251  sge0sn  38259  sge0tsms  38260  sge0cl  38261  sge0ge0  38264  sge0fsum  38267  sge0pr  38274  sge0prle  38281  sge0p1  38294  sge0rernmpt  38302  omessre  38369  omeiunltfirp  38378  carageniuncllem2  38381  omege0  38392  ovnlerp  38422  ovn0lem  38425  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457
  Copyright terms: Public domain W3C validator