Theorem iccgelb 13377

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084   ∈ wcel 2098   class class class wbr 5138  (class class class)co 7401  ℝ^*cxr 11244   ≤ cle 11246  [,]cicc 13324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6485  df-fun 6535  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-xr 11249  df-icc 13328

This theorem is referenced by:  xrge0neqmnf  13426  supicc  13475  ttgcontlem1  28611  xrge0infss  32442  xrge0addgt0  32657  xrge0adddir  32658  esumcst  33550  esumpinfval  33560  oms0  33785  probmeasb  33918  broucube  37012  areaquad  42454  lefldiveq  44487  xadd0ge  44515  xrge0nemnfd  44527  eliccelioc  44719  iccintsng  44721  eliccnelico  44727  eliccelicod  44728  ge0xrre  44729  inficc  44732  iccdificc  44737  iccgelbd  44741  cncfiooiccre  45096  iblspltprt  45174  itgioocnicc  45178  itgspltprt  45180  itgiccshift  45181  fourierdlem1  45309  fourierdlem20  45328  fourierdlem24  45332  fourierdlem25  45333  fourierdlem27  45335  fourierdlem43  45351  fourierdlem44  45352  fourierdlem50  45357  fourierdlem51  45358  fourierdlem52  45359  fourierdlem64  45371  fourierdlem73  45380  fourierdlem76  45383  fourierdlem81  45388  fourierdlem92  45399  fourierdlem102  45409  fourierdlem103  45410  fourierdlem104  45411  fourierdlem114  45421  rrxsnicc  45501  salgencntex  45544  fge0iccico  45571  gsumge0cl  45572  sge0sn  45580  sge0tsms  45581  sge0cl  45582  sge0ge0  45585  sge0fsum  45588  sge0pr  45595  sge0prle  45602  sge0p1  45615  sge0rernmpt  45623  meage0  45676  omessre  45711  omeiunltfirp  45720  carageniuncllem2  45723  omege0  45734  ovnlerp  45763  ovn0lem  45766  hoidmvlelem1  45796  hoidmvlelem2  45797  hoidmvlelem3  45798