Theorem iccgelb 13332

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 13319	. . . 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 5100  (class class class)co 7370  ℝ^*cxr 11179   ≤ cle 11181  [,]cicc 13278

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 2185  ax-ext 2709  ax-sep 5245  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-iota 6458  df-fun 6504  df-fv 6510  df-ov 7373  df-oprab 7374  df-mpo 7375  df-xr 11184  df-icc 13282

This theorem is referenced by:  xrge0neqmnf  13382  supicc  13431  ttgcontlem1  28975  xrge0infss  32857  xrge0addgt0  33116  xrge0adddir  33117  esumcst  34247  esumpinfval  34257  oms0  34481  probmeasb  34614  broucube  37934  areaquad  43602  lefldiveq  45683  xadd0ge  45710  xrge0nemnfd  45720  eliccelioc  45910  iccintsng  45912  eliccnelico  45918  eliccelicod  45919  ge0xrre  45920  inficc  45923  iccdificc  45928  iccgelbd  45932  cncfiooiccre  46282  iblspltprt  46360  itgioocnicc  46364  itgspltprt  46366  itgiccshift  46367  fourierdlem1  46495  fourierdlem20  46514  fourierdlem24  46518  fourierdlem25  46519  fourierdlem27  46521  fourierdlem43  46537  fourierdlem44  46538  fourierdlem50  46543  fourierdlem51  46544  fourierdlem52  46545  fourierdlem64  46557  fourierdlem73  46566  fourierdlem76  46569  fourierdlem81  46574  fourierdlem92  46585  fourierdlem102  46595  fourierdlem103  46596  fourierdlem104  46597  fourierdlem114  46607  rrxsnicc  46687  salgencntex  46730  fge0iccico  46757  gsumge0cl  46758  sge0sn  46766  sge0tsms  46767  sge0cl  46768  sge0ge0  46771  sge0fsum  46774  sge0pr  46781  sge0prle  46788  sge0p1  46801  sge0rernmpt  46809  meage0  46862  omessre  46897  omeiunltfirp  46906  carageniuncllem2  46909  omege0  46920  ovnlerp  46949  ovn0lem  46952  hoidmvlelem1  46982  hoidmvlelem2  46983  hoidmvlelem3  46984