Theorem iccgelb 12519

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113   ∈ wcel 2166   class class class wbr 4874  (class class class)co 6906  ℝ^*cxr 10391   ≤ cle 10393  [,]cicc 12467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pr 5128  ax-un 7210  ax-cnex 10309  ax-resscn 10310

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-opab 4937  df-id 5251  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-iota 6087  df-fun 6126  df-fv 6132  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-xr 10396  df-icc 12471

This theorem is referenced by:  xrge0neqmnf  12566  supicc  12614  ttgcontlem1  26185  xrge0infss  30073  xrge0addgt0  30237  xrge0adddir  30238  esumcst  30671  esumpinfval  30681  oms0  30905  probmeasb  31039  broucube  33988  areaquad  38645  lefldiveq  40305  xadd0ge  40334  xrge0nemnfd  40346  eliccelioc  40544  iccintsng  40546  eliccnelico  40552  eliccelicod  40553  ge0xrre  40554  inficc  40557  iccdificc  40562  iccgelbd  40566  cncfiooiccre  40904  iblspltprt  40984  itgioocnicc  40988  itgspltprt  40990  itgiccshift  40991  fourierdlem1  41120  fourierdlem20  41139  fourierdlem24  41143  fourierdlem25  41144  fourierdlem27  41146  fourierdlem43  41162  fourierdlem44  41163  fourierdlem50  41168  fourierdlem51  41169  fourierdlem52  41170  fourierdlem64  41182  fourierdlem73  41191  fourierdlem76  41194  fourierdlem81  41199  fourierdlem92  41210  fourierdlem102  41220  fourierdlem103  41221  fourierdlem104  41222  fourierdlem114  41232  rrxsnicc  41312  salgencntex  41353  fge0iccico  41379  gsumge0cl  41380  sge0sn  41388  sge0tsms  41389  sge0cl  41390  sge0ge0  41393  sge0fsum  41396  sge0pr  41403  sge0prle  41410  sge0p1  41423  sge0rernmpt  41431  meage0  41484  omessre  41519  omeiunltfirp  41528  carageniuncllem2  41531  omege0  41542  ovnlerp  41571  ovn0lem  41574  hoidmvlelem1  41604  hoidmvlelem2  41605  hoidmvlelem3  41606