Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 1elunit | Structured version Visualization version GIF version |
Description: One is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
Ref | Expression |
---|---|
1elunit | ⊢ 1 ∈ (0[,]1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 10830 | . 2 ⊢ 1 ∈ ℝ | |
2 | 0le1 11352 | . 2 ⊢ 0 ≤ 1 | |
3 | 1le1 11457 | . 2 ⊢ 1 ≤ 1 | |
4 | elicc01 13051 | . 2 ⊢ (1 ∈ (0[,]1) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 ≤ 1)) | |
5 | 1, 2, 3, 4 | mpbir3an 1343 | 1 ⊢ 1 ∈ (0[,]1) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 class class class wbr 5050 (class class class)co 7210 ℝcr 10725 0cc0 10726 1c1 10727 ≤ cle 10865 [,]cicc 12935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pow 5255 ax-pr 5319 ax-un 7520 ax-cnex 10782 ax-resscn 10783 ax-1cn 10784 ax-icn 10785 ax-addcl 10786 ax-addrcl 10787 ax-mulcl 10788 ax-mulrcl 10789 ax-mulcom 10790 ax-addass 10791 ax-mulass 10792 ax-distr 10793 ax-i2m1 10794 ax-1ne0 10795 ax-1rid 10796 ax-rnegex 10797 ax-rrecex 10798 ax-cnre 10799 ax-pre-lttri 10800 ax-pre-lttrn 10801 ax-pre-ltadd 10802 ax-pre-mulgt0 10803 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2940 df-nel 3044 df-ral 3063 df-rex 3064 df-reu 3065 df-rab 3067 df-v 3407 df-sbc 3692 df-csb 3809 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-pw 4512 df-sn 4539 df-pr 4541 df-op 4545 df-uni 4817 df-br 5051 df-opab 5113 df-mpt 5133 df-id 5452 df-po 5465 df-so 5466 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6335 df-fun 6379 df-fn 6380 df-f 6381 df-f1 6382 df-fo 6383 df-f1o 6384 df-fv 6385 df-riota 7167 df-ov 7213 df-oprab 7214 df-mpo 7215 df-er 8388 df-en 8624 df-dom 8625 df-sdom 8626 df-pnf 10866 df-mnf 10867 df-xr 10868 df-ltxr 10869 df-le 10870 df-sub 11061 df-neg 11062 df-icc 12939 |
This theorem is referenced by: iccpnfcnv 23838 htpycom 23870 htpyid 23871 htpyco1 23872 htpyco2 23873 htpycc 23874 phtpy01 23879 phtpycom 23882 phtpyid 23883 phtpyco2 23884 phtpycc 23885 reparphti 23891 pco1 23909 pcohtpylem 23913 pcoptcl 23915 pcopt 23916 pcopt2 23917 pcoass 23918 pcorevcl 23919 pcorevlem 23920 pi1xfrf 23947 pi1xfr 23949 pi1xfrcnvlem 23950 pi1xfrcnv 23951 pi1cof 23953 pi1coghm 23955 dvlipcn 24888 leibpi 25822 lgamgulmlem2 25909 ttgcontlem1 26973 axpaschlem 27028 iistmd 31563 xrge0iif1 31599 xrge0iifmhm 31600 cnpconn 32902 pconnconn 32903 txpconn 32904 ptpconn 32905 indispconn 32906 connpconn 32907 txsconnlem 32912 txsconn 32913 cvxpconn 32914 cvxsconn 32915 cvmliftphtlem 32989 cvmlift3lem2 32992 cvmlift3lem4 32994 cvmlift3lem5 32995 cvmlift3lem6 32996 cvmlift3lem9 32999 lcmineqlem12 39780 k0004val0 41439 |
Copyright terms: Public domain | W3C validator |