Theorem iccgelb 12794

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   ∈ wcel 2114   class class class wbr 5066  (class class class)co 7156  ℝ^*cxr 10674   ≤ cle 10676  [,]cicc 12742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-xr 10679  df-icc 12746

This theorem is referenced by:  xrge0neqmnf  12841  supicc  12887  ttgcontlem1  26671  xrge0infss  30484  xrge0addgt0  30678  xrge0adddir  30679  esumcst  31322  esumpinfval  31332  oms0  31555  probmeasb  31688  broucube  34941  areaquad  39843  lefldiveq  41579  xadd0ge  41608  xrge0nemnfd  41620  eliccelioc  41817  iccintsng  41819  eliccnelico  41825  eliccelicod  41826  ge0xrre  41827  inficc  41830  iccdificc  41835  iccgelbd  41839  cncfiooiccre  42198  iblspltprt  42278  itgioocnicc  42282  itgspltprt  42284  itgiccshift  42285  fourierdlem1  42413  fourierdlem20  42432  fourierdlem24  42436  fourierdlem25  42437  fourierdlem27  42439  fourierdlem43  42455  fourierdlem44  42456  fourierdlem50  42461  fourierdlem51  42462  fourierdlem52  42463  fourierdlem64  42475  fourierdlem73  42484  fourierdlem76  42487  fourierdlem81  42492  fourierdlem92  42503  fourierdlem102  42513  fourierdlem103  42514  fourierdlem104  42515  fourierdlem114  42525  rrxsnicc  42605  salgencntex  42646  fge0iccico  42672  gsumge0cl  42673  sge0sn  42681  sge0tsms  42682  sge0cl  42683  sge0ge0  42686  sge0fsum  42689  sge0pr  42696  sge0prle  42703  sge0p1  42716  sge0rernmpt  42724  meage0  42777  omessre  42812  omeiunltfirp  42821  carageniuncllem2  42824  omege0  42835  ovnlerp  42864  ovn0lem  42867  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899