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

Theorem iccgelb 13326
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 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,]𝐵)) → 𝐴𝐶)

Proof of Theorem iccgelb
StepHypRef Expression
1 elicc1 13314 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵)))
21biimpa 478 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵))
32simp2d 1144 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴𝐶)
433impa 1111 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,]𝐵)) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088  wcel 2107   class class class wbr 5106  (class class class)co 7358  *cxr 11193  cle 11195  [,]cicc 13273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-iota 6449  df-fun 6499  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-xr 11198  df-icc 13277
This theorem is referenced by:  xrge0neqmnf  13375  supicc  13424  ttgcontlem1  27875  xrge0infss  31712  xrge0addgt0  31931  xrge0adddir  31932  esumcst  32719  esumpinfval  32729  oms0  32954  probmeasb  33087  broucube  36158  areaquad  41593  lefldiveq  43613  xadd0ge  43641  xrge0nemnfd  43653  eliccelioc  43845  iccintsng  43847  eliccnelico  43853  eliccelicod  43854  ge0xrre  43855  inficc  43858  iccdificc  43863  iccgelbd  43867  cncfiooiccre  44222  iblspltprt  44300  itgioocnicc  44304  itgspltprt  44306  itgiccshift  44307  fourierdlem1  44435  fourierdlem20  44454  fourierdlem24  44458  fourierdlem25  44459  fourierdlem27  44461  fourierdlem43  44477  fourierdlem44  44478  fourierdlem50  44483  fourierdlem51  44484  fourierdlem52  44485  fourierdlem64  44497  fourierdlem73  44506  fourierdlem76  44509  fourierdlem81  44514  fourierdlem92  44525  fourierdlem102  44535  fourierdlem103  44536  fourierdlem104  44537  fourierdlem114  44547  rrxsnicc  44627  salgencntex  44670  fge0iccico  44697  gsumge0cl  44698  sge0sn  44706  sge0tsms  44707  sge0cl  44708  sge0ge0  44711  sge0fsum  44714  sge0pr  44721  sge0prle  44728  sge0p1  44741  sge0rernmpt  44749  meage0  44802  omessre  44837  omeiunltfirp  44846  carageniuncllem2  44849  omege0  44860  ovnlerp  44889  ovn0lem  44892  hoidmvlelem1  44922  hoidmvlelem2  44923  hoidmvlelem3  44924
  Copyright terms: Public domain W3C validator