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

Theorem iccgelb 12215
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 12204 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵)))
21biimpa 501 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵))
32simp2d 1072 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴𝐶)
433impa 1257 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,]𝐵)) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036  wcel 1988   class class class wbr 4644  (class class class)co 6635  *cxr 10058  cle 10060  [,]cicc 12163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-xr 10063  df-icc 12167
This theorem is referenced by:  supicc  12305  ttgcontlem1  25746  xrge0infss  29499  xrge0addgt0  29665  xrge0adddir  29666  esumcst  30099  esumpinfval  30109  oms0  30333  probmeasb  30466  broucube  33414  areaquad  37621  lefldiveq  39318  xadd0ge  39349  xrge0nemnfd  39361  eliccelioc  39550  iccintsng  39552  ge0nemnf2  39558  eliccnelico  39559  eliccelicod  39560  ge0xrre  39561  inficc  39564  iccdificc  39569  iccgelbd  39573  cncfiooiccre  39871  iblspltprt  39952  itgioocnicc  39956  itgspltprt  39958  itgiccshift  39959  fourierdlem1  40088  fourierdlem20  40107  fourierdlem24  40111  fourierdlem25  40112  fourierdlem27  40114  fourierdlem43  40130  fourierdlem44  40131  fourierdlem50  40136  fourierdlem51  40137  fourierdlem52  40138  fourierdlem64  40150  fourierdlem73  40159  fourierdlem76  40162  fourierdlem81  40167  fourierdlem92  40178  fourierdlem102  40188  fourierdlem103  40189  fourierdlem104  40190  fourierdlem114  40200  rrxsnicc  40283  salgencntex  40324  fge0iccico  40350  gsumge0cl  40351  sge0sn  40359  sge0tsms  40360  sge0cl  40361  sge0ge0  40364  sge0fsum  40367  sge0pr  40374  sge0prle  40381  sge0p1  40394  sge0rernmpt  40402  meage0  40455  omessre  40487  omeiunltfirp  40496  carageniuncllem2  40499  omege0  40510  ovnlerp  40539  ovn0lem  40542  hoidmvlelem1  40572  hoidmvlelem2  40573  hoidmvlelem3  40574
  Copyright terms: Public domain W3C validator