Theorem 0elunit 13601

Description: Zero is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.)

Assertion

Ref	Expression
0elunit	⊢ 0 ∈ (0[,]1)

Proof of Theorem 0elunit

Step	Hyp	Ref	Expression
1		0re 11311	. 2 ⊢ 0 ∈ ℝ
2		0le0 12445	. 2 ⊢ 0 ≤ 0
3		0le1 11840	. 2 ⊢ 0 ≤ 1
4		elicc01 13598	. 2 ⊢ (0 ∈ (0[,]1) ↔ (0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 ≤ 1))
5	1, 2, 3, 4	mpbir3an 1360	1 ⊢ 0 ∈ (0[,]1)

This proof depends on syntax axioms:   ∈ wcel 2144   class class class wbr 5102  (class class class)co 7420  ℝcr 11200  0cc0 11201  1c1 11202   ≤ cle 11345  [,]cicc 13480

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11257  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277  ax-pre-mulgt0 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8718  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11346  df-mnf 11347  df-xr 11348  df-ltxr 11349  df-le 11350  df-sub 11544  df-neg 11545  df-icc 13484

This theorem is used by:  xrhmeo  25268  htpycom  25298  htpyid  25299  htpyco1  25300  htpyco2  25301  htpycc  25302  phtpy01  25307  phtpycom  25310  phtpyid  25311  phtpyco2  25312  phtpycc  25313  reparphti  25319  pcocn  25339  pcohtpylem  25341  pcoptcl  25343  pcopt  25344  pcopt2  25345  pcoass  25346  pcorevcl  25347  pcorevlem  25348  pi1xfrf  25375  pi1xfr  25377  pi1xfrcnvlem  25378  pi1xfrcnv  25379  pi1cof  25381  pi1coghm  25383  dvlipcn  26315  lgamgulmlem2  27358  ttgcontlem1  29463  brbtwn2  29484  axsegconlem1  29496  axpaschlem  29519  axcontlem7  29549  axcontlem8  29550  xrge0iifcnv  34608  xrge0iifiso  34610  xrge0iifhom  34612  cnpconn  36064  pconnconn  36065  txpconn  36066  ptpconn  36067  indispconn  36068  connpconn  36069  sconnpi1  36073  txsconnlem  36074  txsconn  36075  cvxpconn  36076  cvxsconn  36077  cvmliftlem14  36131  cvmlift2lem2  36138  cvmlift2lem3  36139  cvmlift2lem8  36144  cvmlift2lem12  36148  cvmlift2lem13  36149  cvmliftphtlem  36151  cvmliftpht  36152  cvmlift3lem1  36153  cvmlift3lem2  36154  cvmlift3lem4  36156  cvmlift3lem5  36157  cvmlift3lem6  36158  cvmlift3lem9  36161  lcmineqlem12  43166