HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The number 2 is positive. |
| Ref | Expression |
|---|---|
| 2pos |
    |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1re 5407 |
. . 3
   | |
| 2 | lt01 5653 |
. . 3
| |
| 3 | 1, 1, 2, 2 | addgt0i 5575 |
. 2
   |
| 4 | df-2 5917 |
. 2
 | |
| 5 | 3, 4 | breqtrr 2630 |
1
|
| Colors of variables: wff set class |
| Syntax hints: class class
class wbr 2609 (class class class)co 3948
cc0 5206
c1 5207
caddc 5209 clt 5458 c2 5908 |
| This theorem is referenced by: 2ne0 5937 3pos 5938 halfgt0 5976 halflt1 5977 halfpos2t 5984 halfnneg2t 5985 nominpos 5990 avglet 5991 nneo 6144 flhalft 6189 expubndt 6539 discrlem2 6587 nnesq 6592 sqr4 6647 sqr2gt1lt2 6649 sqr2irrlem4 6657 sqr2irr 6659 sqr2re 6660 abstri 6829 climunii 7035 climaddlem3 7052 erelem3 7263 efaddlem8 7287 efaddlem12 7291 efaddlem15 7294 cos01bndlem2 7412 cos2bnd 7417 sin01gt0 7418 sin02gt0 7420 sincos2sgn 7422 sin4lt0 7423 znnen 7445 metge0 7760 bl2in 7783 bcthlem1 7933 bcthlem8 7940 bcthlem21 7953 nvge0 8241 ipid 8297 ubthlem12 8471 ubthlem13 8472 minveclem16 8491 minveclem21 8496 minveclem25 8500 minveclem26 8501 minveclem27 8502 minveclem35 8510 pilem1 8590 pilem2 8591 pilem3 8592 sinhalfpilem 8598 sincosq1lem 8620 sinq12gt0t 8625 sincos4thpi 8627 sincos6thpi 8628 cosh111lem1 8629 efifolem6 8642 normpar2 8944 bcsALT 8967 hlimcaui 9027 hlimunii 9029 projlem2 9103 projlem3 9104 projlem4 9105 projlem5 9106 projlem6 9107 projlem18 9119 projlem28 9129 hmopidmch 9990 cdj3lem1 10266 dmse1 10467 mslb1 10473 msra3 10475 iintlem1 10476 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-inf2 4597 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-nel 1580 df-ral 1641 df-rex 1642 df-reu 1643 df-rab 1644 df-v 1803 df-sbc 1932 df-csb 1992 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-int 2524 df-iun 2558 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-f1 3185 df-fo 3186 df-f1o 3187 df-fv 3188 df-rdg 3917 df-opr 3950 df-oprab 3951 df-1st 4063 df-2nd 4064 df-1o 4117 df-oadd 4119 df-omul 4120 df-er 4245 df-ec 4247 df-qs 4250 df-en 4351 df-dom 4352 df-sdom 4353 df-ni 4972 df-pli 4973 df-mi 4974 df-lti 4975 df-plpq 5007 df-mpq 5008 df-enq 5009 df-nq 5010 df-plq 5011 df-mq 5012 df-rq 5013 df-ltq 5014 df-1q 5015 df-np 5058 df-1p 5059 df-plp 5060 df-mp 5061 df-ltp 5062 df-plpr 5136 df-mpr 5137 df-enr 5138 df-nr 5139 df-plr 5140 df-mr 5141 df-ltr 5142 df-0r 5143 df-1r 5144 df-m1r 5145 df-c 5212 df-0 5213 df-1 5214 df-i 5215 df-r 5216 df-plus 5217 df-mul 5218 df-lt 5219 df-sub 5328 df-neg 5330 df-pnf 5459 df-mnf 5460 df-xr 5461 df-ltxr 5462 df-le 5463 df-2 5917 |