Theorem iccgelb 13064

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 13052	. . . 4 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
2	1	biimpa 476	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))
3	2	simp2d 1141	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶)
4	3	3impa 1108	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   ∈ wcel 2108   class class class wbr 5070  (class class class)co 7255  ℝ^*cxr 10939   ≤ cle 10941  [,]cicc 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-xr 10944  df-icc 13015

This theorem is referenced by:  xrge0neqmnf  13113  supicc  13162  ttgcontlem1  27155  xrge0infss  30985  xrge0addgt0  31202  xrge0adddir  31203  esumcst  31931  esumpinfval  31941  oms0  32164  probmeasb  32297  broucube  35738  areaquad  40963  lefldiveq  42721  xadd0ge  42749  xrge0nemnfd  42761  eliccelioc  42949  iccintsng  42951  eliccnelico  42957  eliccelicod  42958  ge0xrre  42959  inficc  42962  iccdificc  42967  iccgelbd  42971  cncfiooiccre  43326  iblspltprt  43404  itgioocnicc  43408  itgspltprt  43410  itgiccshift  43411  fourierdlem1  43539  fourierdlem20  43558  fourierdlem24  43562  fourierdlem25  43563  fourierdlem27  43565  fourierdlem43  43581  fourierdlem44  43582  fourierdlem50  43587  fourierdlem51  43588  fourierdlem52  43589  fourierdlem64  43601  fourierdlem73  43610  fourierdlem76  43613  fourierdlem81  43618  fourierdlem92  43629  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  rrxsnicc  43731  salgencntex  43772  fge0iccico  43798  gsumge0cl  43799  sge0sn  43807  sge0tsms  43808  sge0cl  43809  sge0ge0  43812  sge0fsum  43815  sge0pr  43822  sge0prle  43829  sge0p1  43842  sge0rernmpt  43850  meage0  43903  omessre  43938  omeiunltfirp  43947  carageniuncllem2  43950  omege0  43961  ovnlerp  43990  ovn0lem  43993  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025