Theorem iccgelb 13320

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

Step	Hyp	Ref	Expression
1		elicc1 13307	. . . 4 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
2	1	biimpa 476	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))
3	2	simp2d 1144	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶)
4	3	3impa 1110	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5097  (class class class)co 7358  ℝ^*cxr 11167   ≤ cle 11169  [,]cicc 13266

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376  ax-un 7680  ax-cnex 11084  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6447  df-fun 6493  df-fv 6499  df-ov 7361  df-oprab 7362  df-mpo 7363  df-xr 11172  df-icc 13270

This theorem is referenced by:  xrge0neqmnf  13370  supicc  13419  ttgcontlem1  28938  xrge0infss  32819  xrge0addgt0  33078  xrge0adddir  33079  esumcst  34199  esumpinfval  34209  oms0  34433  probmeasb  34566  broucube  37824  areaquad  43495  lefldiveq  45577  xadd0ge  45604  xrge0nemnfd  45614  eliccelioc  45804  iccintsng  45806  eliccnelico  45812  eliccelicod  45813  ge0xrre  45814  inficc  45817  iccdificc  45822  iccgelbd  45826  cncfiooiccre  46176  iblspltprt  46254  itgioocnicc  46258  itgspltprt  46260  itgiccshift  46261  fourierdlem1  46389  fourierdlem20  46408  fourierdlem24  46412  fourierdlem25  46413  fourierdlem27  46415  fourierdlem43  46431  fourierdlem44  46432  fourierdlem50  46437  fourierdlem51  46438  fourierdlem52  46439  fourierdlem64  46451  fourierdlem73  46460  fourierdlem76  46463  fourierdlem81  46468  fourierdlem92  46479  fourierdlem102  46489  fourierdlem103  46490  fourierdlem104  46491  fourierdlem114  46501  rrxsnicc  46581  salgencntex  46624  fge0iccico  46651  gsumge0cl  46652  sge0sn  46660  sge0tsms  46661  sge0cl  46662  sge0ge0  46665  sge0fsum  46668  sge0pr  46675  sge0prle  46682  sge0p1  46695  sge0rernmpt  46703  meage0  46756  omessre  46791  omeiunltfirp  46800  carageniuncllem2  46803  omege0  46814  ovnlerp  46843  ovn0lem  46846  hoidmvlelem1  46876  hoidmvlelem2  46877  hoidmvlelem3  46878