Theorem iccgelb 13457

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 13444	. . . 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 2145   class class class wbr 5107  (class class class)co 7416  ℝ^*cxr 11269   ≤ cle 11271  [,]cicc 13403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-un 7739  ax-cnex 11183  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-xr 11274  df-icc 13407

This theorem is used by:  xrge0neqmnf  13507  supicc  13556  ttgcontlem1  29327  xrge0infss  33218  xrge0addgt0  33444  xrge0adddir  33445  esumcst  34560  esumpinfval  34570  oms0  34795  probmeasb  34928  broucube  38390  areaquad  44044  lefldiveq  46112  xadd0ge  46139  xrge0nemnfd  46149  eliccelioc  46338  iccintsng  46340  eliccnelico  46346  eliccelicod  46347  ge0xrre  46348  inficc  46351  iccdificc  46356  iccgelbd  46360  cncfiooiccre  46710  iblspltprt  46788  itgioocnicc  46792  itgspltprt  46794  itgiccshift  46795  fourierdlem1  46923  fourierdlem20  46942  fourierdlem24  46946  fourierdlem25  46947  fourierdlem27  46949  fourierdlem43  46965  fourierdlem44  46966  fourierdlem50  46971  fourierdlem51  46972  fourierdlem52  46973  fourierdlem64  46985  fourierdlem73  46994  fourierdlem76  46997  fourierdlem81  47002  fourierdlem92  47013  fourierdlem102  47023  fourierdlem103  47024  fourierdlem104  47025  fourierdlem114  47035  rrxsnicc  47115  salgencntex  47158  fge0iccico  47185  gsumge0cl  47186  sge0sn  47194  sge0tsms  47195  sge0cl  47196  sge0ge0  47199  sge0fsum  47202  sge0pr  47209  sge0prle  47216  sge0p1  47229  sge0rernmpt  47237  meage0  47290  omessre  47325  omeiunltfirp  47334  carageniuncllem2  47337  omege0  47348  ovnlerp  47377  ovn0lem  47380  hoidmvlelem1  47410  hoidmvlelem2  47411  hoidmvlelem3  47412