Theorem iccgelb 13533

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2144   class class class wbr 5102  (class class class)co 7420  ℝ^*cxr 11342   ≤ cle 11344  [,]cicc 13479

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-xr 11347  df-icc 13483

This theorem is used by:  xrge0neqmnf  13583  supicc  13632  ttgcontlem1  29462  xrge0infss  33352  xrge0addgt0  33578  xrge0adddir  33579  esumcst  34695  esumpinfval  34705  oms0  34929  probmeasb  35062  broucube  38573  areaquad  44218  lefldiveq  46308  xadd0ge  46334  xrge0nemnfd  46344  eliccelioc  46533  iccintsng  46535  eliccnelico  46541  eliccelicod  46542  ge0xrre  46543  inficc  46546  iccdificc  46551  iccgelbd  46555  cncfiooiccre  46905  iblspltprt  46983  itgioocnicc  46987  itgspltprt  46989  itgiccshift  46990  fourierdlem1  47118  fourierdlem20  47137  fourierdlem24  47141  fourierdlem25  47142  fourierdlem27  47144  fourierdlem43  47160  fourierdlem44  47161  fourierdlem50  47166  fourierdlem51  47167  fourierdlem52  47168  fourierdlem64  47180  fourierdlem73  47189  fourierdlem76  47192  fourierdlem81  47197  fourierdlem92  47208  fourierdlem102  47218  fourierdlem103  47219  fourierdlem104  47220  fourierdlem114  47230  rrxsnicc  47310  salgencntex  47353  fge0iccico  47380  gsumge0cl  47381  sge0sn  47389  sge0tsms  47390  sge0cl  47391  sge0ge0  47394  sge0fsum  47397  sge0pr  47404  sge0prle  47411  sge0p1  47424  sge0rernmpt  47432  meage0  47485  omessre  47520  omeiunltfirp  47529  carageniuncllem2  47532  omege0  47543  ovnlerp  47572  ovn0lem  47575  hoidmvlelem1  47605  hoidmvlelem2  47606  hoidmvlelem3  47607