![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3pos | Structured version Visualization version GIF version |
Description: The number 3 is positive. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
3pos | ⊢ 0 < 3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2re 11561 | . . 3 ⊢ 2 ∈ ℝ | |
2 | 1re 10490 | . . 3 ⊢ 1 ∈ ℝ | |
3 | 2pos 11590 | . . 3 ⊢ 0 < 2 | |
4 | 0lt1 11012 | . . 3 ⊢ 0 < 1 | |
5 | 1, 2, 3, 4 | addgt0ii 11032 | . 2 ⊢ 0 < (2 + 1) |
6 | df-3 11551 | . 2 ⊢ 3 = (2 + 1) | |
7 | 5, 6 | breqtrri 4991 | 1 ⊢ 0 < 3 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 4964 (class class class)co 7019 0cc0 10386 1c1 10387 + caddc 10389 < clt 10524 2c2 11542 3c3 11543 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-resscn 10443 ax-1cn 10444 ax-icn 10445 ax-addcl 10446 ax-addrcl 10447 ax-mulcl 10448 ax-mulrcl 10449 ax-mulcom 10450 ax-addass 10451 ax-mulass 10452 ax-distr 10453 ax-i2m1 10454 ax-1ne0 10455 ax-1rid 10456 ax-rnegex 10457 ax-rrecex 10458 ax-cnre 10459 ax-pre-lttri 10460 ax-pre-lttrn 10461 ax-pre-ltadd 10462 ax-pre-mulgt0 10463 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-nel 3090 df-ral 3109 df-rex 3110 df-reu 3111 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-br 4965 df-opab 5027 df-mpt 5044 df-id 5351 df-po 5365 df-so 5366 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-riota 6980 df-ov 7022 df-oprab 7023 df-mpo 7024 df-er 8142 df-en 8361 df-dom 8362 df-sdom 8363 df-pnf 10526 df-mnf 10527 df-xr 10528 df-ltxr 10529 df-le 10530 df-sub 10721 df-neg 10722 df-2 11550 df-3 11551 |
This theorem is referenced by: 3ne0 11593 4pos 11594 3rp 12245 fz0to4untppr 12860 s4fv0 14093 sqrlem7 14442 sqrt9 14467 ef01bndlem 15370 cos2bnd 15374 sin01gt0 15376 cos01gt0 15377 rpnnen2lem3 15402 rpnnen2lem4 15403 rpnnen2lem9 15408 flodddiv4 15597 43prm 16284 cnfldfun 20239 tangtx 24774 sincos6thpi 24784 pige3ALT 24788 log2cnv 25204 log2tlbnd 25205 ppiub 25462 bposlem2 25543 bposlem3 25544 bposlem4 25545 bposlem5 25546 lgsdir2lem1 25583 dchrvmasumiflem1 25759 tgcgr4 25999 frgrogt3nreg 27860 friendshipgt3 27861 ex-gcd 27920 cyc3fv3 30410 cyc3conja 30429 hgt750lemd 31528 hgt750lem2 31532 heiborlem5 34638 heiborlem7 34640 jm2.23 39091 stoweidlem13 41854 stoweidlem26 41867 stoweidlem34 41875 stoweidlem42 41883 stoweidlem59 41900 stoweid 41904 wallispilem4 41909 smfmullem4 42625 257prm 43219 127prm 43259 nfermltl2rev 43404 |
Copyright terms: Public domain | W3C validator |