Theorem iccgelb 13443

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 13431	. . . 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 2108   class class class wbr 5143  (class class class)co 7431  ℝ^*cxr 11294   ≤ cle 11296  [,]cicc 13390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-xr 11299  df-icc 13394

This theorem is referenced by:  xrge0neqmnf  13492  supicc  13541  ttgcontlem1  28899  xrge0infss  32764  xrge0addgt0  33022  xrge0adddir  33023  esumcst  34064  esumpinfval  34074  oms0  34299  probmeasb  34432  broucube  37661  areaquad  43228  lefldiveq  45304  xadd0ge  45332  xrge0nemnfd  45343  eliccelioc  45534  iccintsng  45536  eliccnelico  45542  eliccelicod  45543  ge0xrre  45544  inficc  45547  iccdificc  45552  iccgelbd  45556  cncfiooiccre  45910  iblspltprt  45988  itgioocnicc  45992  itgspltprt  45994  itgiccshift  45995  fourierdlem1  46123  fourierdlem20  46142  fourierdlem24  46146  fourierdlem25  46147  fourierdlem27  46149  fourierdlem43  46165  fourierdlem44  46166  fourierdlem50  46171  fourierdlem51  46172  fourierdlem52  46173  fourierdlem64  46185  fourierdlem73  46194  fourierdlem76  46197  fourierdlem81  46202  fourierdlem92  46213  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  rrxsnicc  46315  salgencntex  46358  fge0iccico  46385  gsumge0cl  46386  sge0sn  46394  sge0tsms  46395  sge0cl  46396  sge0ge0  46399  sge0fsum  46402  sge0pr  46409  sge0prle  46416  sge0p1  46429  sge0rernmpt  46437  meage0  46490  omessre  46525  omeiunltfirp  46534  carageniuncllem2  46537  omege0  46548  ovnlerp  46577  ovn0lem  46580  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612