Theorem iccgelb 13339

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 13326	. . . 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 11183   ≤ cle 11185  [,]cicc 13285

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 11100  ax-resscn 11101

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 11188  df-icc 13289

This theorem is referenced by:  xrge0neqmnf  13389  supicc  13438  ttgcontlem1  28865  xrge0infss  32733  xrge0addgt0  33001  xrge0adddir  33002  esumcst  34046  esumpinfval  34056  oms0  34281  probmeasb  34414  broucube  37641  areaquad  43198  lefldiveq  45283  xadd0ge  45310  xrge0nemnfd  45321  eliccelioc  45512  iccintsng  45514  eliccnelico  45520  eliccelicod  45521  ge0xrre  45522  inficc  45525  iccdificc  45530  iccgelbd  45534  cncfiooiccre  45886  iblspltprt  45964  itgioocnicc  45968  itgspltprt  45970  itgiccshift  45971  fourierdlem1  46099  fourierdlem20  46118  fourierdlem24  46122  fourierdlem25  46123  fourierdlem27  46125  fourierdlem43  46141  fourierdlem44  46142  fourierdlem50  46147  fourierdlem51  46148  fourierdlem52  46149  fourierdlem64  46161  fourierdlem73  46170  fourierdlem76  46173  fourierdlem81  46178  fourierdlem92  46189  fourierdlem102  46199  fourierdlem103  46200  fourierdlem104  46201  fourierdlem114  46211  rrxsnicc  46291  salgencntex  46334  fge0iccico  46361  gsumge0cl  46362  sge0sn  46370  sge0tsms  46371  sge0cl  46372  sge0ge0  46375  sge0fsum  46378  sge0pr  46385  sge0prle  46392  sge0p1  46405  sge0rernmpt  46413  meage0  46466  omessre  46501  omeiunltfirp  46510  carageniuncllem2  46513  omege0  46524  ovnlerp  46553  ovn0lem  46556  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588