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

Theorem iccgelb 12779
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 12768 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵)))
21biimpa 480 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵))
32simp2d 1140 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴𝐶)
433impa 1107 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,]𝐵)) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084  wcel 2115   class class class wbr 5047  (class class class)co 7138  *cxr 10659  cle 10661  [,]cicc 12727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pr 5311  ax-un 7444  ax-cnex 10578  ax-resscn 10579
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-iota 6295  df-fun 6338  df-fv 6344  df-ov 7141  df-oprab 7142  df-mpo 7143  df-xr 10664  df-icc 12731
This theorem is referenced by:  xrge0neqmnf  12828  supicc  12877  ttgcontlem1  26668  xrge0infss  30481  xrge0addgt0  30696  xrge0adddir  30697  esumcst  31340  esumpinfval  31350  oms0  31573  probmeasb  31706  broucube  34991  areaquad  39998  lefldiveq  41766  xadd0ge  41794  xrge0nemnfd  41806  eliccelioc  42000  iccintsng  42002  eliccnelico  42008  eliccelicod  42009  ge0xrre  42010  inficc  42013  iccdificc  42018  iccgelbd  42022  cncfiooiccre  42379  iblspltprt  42457  itgioocnicc  42461  itgspltprt  42463  itgiccshift  42464  fourierdlem1  42592  fourierdlem20  42611  fourierdlem24  42615  fourierdlem25  42616  fourierdlem27  42618  fourierdlem43  42634  fourierdlem44  42635  fourierdlem50  42640  fourierdlem51  42641  fourierdlem52  42642  fourierdlem64  42654  fourierdlem73  42663  fourierdlem76  42666  fourierdlem81  42671  fourierdlem92  42682  fourierdlem102  42692  fourierdlem103  42693  fourierdlem104  42694  fourierdlem114  42704  rrxsnicc  42784  salgencntex  42825  fge0iccico  42851  gsumge0cl  42852  sge0sn  42860  sge0tsms  42861  sge0cl  42862  sge0ge0  42865  sge0fsum  42868  sge0pr  42875  sge0prle  42882  sge0p1  42895  sge0rernmpt  42903  meage0  42956  omessre  42991  omeiunltfirp  43000  carageniuncllem2  43003  omege0  43014  ovnlerp  43043  ovn0lem  43046  hoidmvlelem1  43076  hoidmvlelem2  43077  hoidmvlelem3  43078
  Copyright terms: Public domain W3C validator