Theorem iccgelb 13557

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2147   class class class wbr 5106  (class class class)co 7440  ℝ^*cxr 11366   ≤ cle 11368  [,]cicc 13503

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6509  df-fun 6557  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-xr 11371  df-icc 13507

This theorem is used by:  xrge0neqmnf  13607  supicc  13656  ttgcontlem1  29489  xrge0infss  33419  xrge0addgt0  33645  xrge0adddir  33646  esumcst  34762  esumpinfval  34772  oms0  34996  probmeasb  35129  broucube  38763  areaquad  44408  lefldiveq  46511  xadd0ge  46537  xrge0nemnfd  46547  eliccelioc  46736  iccintsng  46738  eliccnelico  46744  eliccelicod  46745  ge0xrre  46746  inficc  46749  iccdificc  46754  iccgelbd  46758  cncfiooiccre  47108  iblspltprt  47186  itgioocnicc  47190  itgspltprt  47192  itgiccshift  47193  fourierdlem1  47321  fourierdlem20  47340  fourierdlem24  47344  fourierdlem25  47345  fourierdlem27  47347  fourierdlem43  47363  fourierdlem44  47364  fourierdlem50  47369  fourierdlem51  47370  fourierdlem52  47371  fourierdlem64  47383  fourierdlem73  47392  fourierdlem76  47395  fourierdlem81  47400  fourierdlem92  47411  fourierdlem102  47421  fourierdlem103  47422  fourierdlem104  47423  fourierdlem114  47433  rrxsnicc  47513  salgencntex  47556  fge0iccico  47583  gsumge0cl  47584  sge0sn  47592  sge0tsms  47593  sge0cl  47594  sge0ge0  47597  sge0fsum  47600  sge0pr  47607  sge0prle  47614  sge0p1  47627  sge0rernmpt  47635  meage0  47688  omessre  47723  omeiunltfirp  47732  carageniuncllem2  47735  omege0  47746  ovnlerp  47775  ovn0lem  47778  hoidmvlelem1  47808  hoidmvlelem2  47809  hoidmvlelem3  47810