Theorem iccgelb 13322

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5099  (class class class)co 7360  ℝ^*cxr 11169   ≤ cle 11171  [,]cicc 13268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-ov 7363  df-oprab 7364  df-mpo 7365  df-xr 11174  df-icc 13272

This theorem is referenced by:  xrge0neqmnf  13372  supicc  13421  ttgcontlem1  28961  xrge0infss  32842  xrge0addgt0  33101  xrge0adddir  33102  esumcst  34222  esumpinfval  34232  oms0  34456  probmeasb  34589  broucube  37857  areaquad  43525  lefldiveq  45607  xadd0ge  45634  xrge0nemnfd  45644  eliccelioc  45834  iccintsng  45836  eliccnelico  45842  eliccelicod  45843  ge0xrre  45844  inficc  45847  iccdificc  45852  iccgelbd  45856  cncfiooiccre  46206  iblspltprt  46284  itgioocnicc  46288  itgspltprt  46290  itgiccshift  46291  fourierdlem1  46419  fourierdlem20  46438  fourierdlem24  46442  fourierdlem25  46443  fourierdlem27  46445  fourierdlem43  46461  fourierdlem44  46462  fourierdlem50  46467  fourierdlem51  46468  fourierdlem52  46469  fourierdlem64  46481  fourierdlem73  46490  fourierdlem76  46493  fourierdlem81  46498  fourierdlem92  46509  fourierdlem102  46519  fourierdlem103  46520  fourierdlem104  46521  fourierdlem114  46531  rrxsnicc  46611  salgencntex  46654  fge0iccico  46681  gsumge0cl  46682  sge0sn  46690  sge0tsms  46691  sge0cl  46692  sge0ge0  46695  sge0fsum  46698  sge0pr  46705  sge0prle  46712  sge0p1  46725  sge0rernmpt  46733  meage0  46786  omessre  46821  omeiunltfirp  46830  carageniuncllem2  46833  omege0  46844  ovnlerp  46873  ovn0lem  46876  hoidmvlelem1  46906  hoidmvlelem2  46907  hoidmvlelem3  46908