Theorem iccgelb 13312

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2113   class class class wbr 5095  (class class class)co 7355  ℝ^*cxr 11155   ≤ cle 11157  [,]cicc 13258

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-cnex 11072  ax-resscn 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6445  df-fun 6491  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-xr 11160  df-icc 13262

This theorem is referenced by:  xrge0neqmnf  13362  supicc  13411  ttgcontlem1  28873  xrge0infss  32754  xrge0addgt0  33009  xrge0adddir  33010  esumcst  34087  esumpinfval  34097  oms0  34321  probmeasb  34454  broucube  37704  areaquad  43323  lefldiveq  45407  xadd0ge  45434  xrge0nemnfd  45445  eliccelioc  45635  iccintsng  45637  eliccnelico  45643  eliccelicod  45644  ge0xrre  45645  inficc  45648  iccdificc  45653  iccgelbd  45657  cncfiooiccre  46007  iblspltprt  46085  itgioocnicc  46089  itgspltprt  46091  itgiccshift  46092  fourierdlem1  46220  fourierdlem20  46239  fourierdlem24  46243  fourierdlem25  46244  fourierdlem27  46246  fourierdlem43  46262  fourierdlem44  46263  fourierdlem50  46268  fourierdlem51  46269  fourierdlem52  46270  fourierdlem64  46282  fourierdlem73  46291  fourierdlem76  46294  fourierdlem81  46299  fourierdlem92  46310  fourierdlem102  46320  fourierdlem103  46321  fourierdlem104  46322  fourierdlem114  46332  rrxsnicc  46412  salgencntex  46455  fge0iccico  46482  gsumge0cl  46483  sge0sn  46491  sge0tsms  46492  sge0cl  46493  sge0ge0  46496  sge0fsum  46499  sge0pr  46506  sge0prle  46513  sge0p1  46526  sge0rernmpt  46534  meage0  46587  omessre  46622  omeiunltfirp  46631  carageniuncllem2  46634  omege0  46645  ovnlerp  46674  ovn0lem  46677  hoidmvlelem1  46707  hoidmvlelem2  46708  hoidmvlelem3  46709