Theorem iccgelb 13341

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 13328	. . . 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 2109   class class class wbr 5102  (class class class)co 7369  ℝ^*cxr 11185   ≤ cle 11187  [,]cicc 13287

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11102  ax-resscn 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-xr 11190  df-icc 13291

This theorem is referenced by:  xrge0neqmnf  13391  supicc  13440  ttgcontlem1  28866  xrge0infss  32734  xrge0addgt0  33002  xrge0adddir  33003  esumcst  34047  esumpinfval  34057  oms0  34282  probmeasb  34415  broucube  37642  areaquad  43199  lefldiveq  45284  xadd0ge  45311  xrge0nemnfd  45322  eliccelioc  45513  iccintsng  45515  eliccnelico  45521  eliccelicod  45522  ge0xrre  45523  inficc  45526  iccdificc  45531  iccgelbd  45535  cncfiooiccre  45887  iblspltprt  45965  itgioocnicc  45969  itgspltprt  45971  itgiccshift  45972  fourierdlem1  46100  fourierdlem20  46119  fourierdlem24  46123  fourierdlem25  46124  fourierdlem27  46126  fourierdlem43  46142  fourierdlem44  46143  fourierdlem50  46148  fourierdlem51  46149  fourierdlem52  46150  fourierdlem64  46162  fourierdlem73  46171  fourierdlem76  46174  fourierdlem81  46179  fourierdlem92  46190  fourierdlem102  46200  fourierdlem103  46201  fourierdlem104  46202  fourierdlem114  46212  rrxsnicc  46292  salgencntex  46335  fge0iccico  46362  gsumge0cl  46363  sge0sn  46371  sge0tsms  46372  sge0cl  46373  sge0ge0  46376  sge0fsum  46379  sge0pr  46386  sge0prle  46393  sge0p1  46406  sge0rernmpt  46414  meage0  46467  omessre  46502  omeiunltfirp  46511  carageniuncllem2  46514  omege0  46525  ovnlerp  46554  ovn0lem  46557  hoidmvlelem1  46587  hoidmvlelem2  46588  hoidmvlelem3  46589