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 12056 | . . 3 ⊢ 2 ∈ ℝ | |
2 | 1re 10984 | . . 3 ⊢ 1 ∈ ℝ | |
3 | 2pos 12085 | . . 3 ⊢ 0 < 2 | |
4 | 0lt1 11506 | . . 3 ⊢ 0 < 1 | |
5 | 1, 2, 3, 4 | addgt0ii 11526 | . 2 ⊢ 0 < (2 + 1) |
6 | df-3 12046 | . 2 ⊢ 3 = (2 + 1) | |
7 | 5, 6 | breqtrri 5102 | 1 ⊢ 0 < 3 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 5075 (class class class)co 7284 0cc0 10880 1c1 10881 + caddc 10883 < clt 11018 2c2 12037 3c3 12038 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5076 df-opab 5138 df-mpt 5159 df-id 5490 df-po 5504 df-so 5505 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-er 8507 df-en 8743 df-dom 8744 df-sdom 8745 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-2 12045 df-3 12046 |
This theorem is referenced by: 3ne0 12088 4pos 12089 3rp 12745 fz0to4untppr 13368 s4fv0 14617 sqrlem7 14969 sqrt9 14994 ef01bndlem 15902 cos2bnd 15906 sin01gt0 15908 cos01gt0 15909 rpnnen2lem3 15934 rpnnen2lem4 15935 rpnnen2lem9 15940 flodddiv4 16131 43prm 16832 slotsdifunifndx 17120 cnfldfunALTOLD 20620 tangtx 25671 sincos6thpi 25681 pige3ALT 25685 log2cnv 26103 log2tlbnd 26104 ppiub 26361 bposlem2 26442 bposlem3 26443 bposlem4 26444 bposlem5 26445 lgsdir2lem1 26482 dchrvmasumiflem1 26658 tgcgr4 26901 frgrogt3nreg 28770 friendshipgt3 28771 ex-gcd 28830 cyc3fv3 31415 cyc3conja 31433 hgt750lemd 32637 hgt750lem2 32641 heiborlem5 35982 heiborlem7 35984 3lexlogpow5ineq2 40070 3lexlogpow5ineq4 40071 3lexlogpow5ineq3 40072 3lexlogpow2ineq1 40073 3lexlogpow2ineq2 40074 3lexlogpow5ineq5 40075 aks4d1lem1 40077 aks4d1p1p6 40088 aks4d1p1p5 40090 aks4d1p1 40091 aks4d1p2 40092 aks4d1p3 40093 aks4d1p5 40095 aks4d1p6 40096 aks4d1p7d1 40097 aks4d1p7 40098 aks4d1p8 40102 aks4d1p9 40103 acos1half 40177 jm2.23 40825 stoweidlem13 43561 stoweidlem26 43574 stoweidlem34 43582 stoweidlem42 43590 stoweidlem59 43607 stoweid 43611 wallispilem4 43616 smfmullem4 44339 257prm 45024 127prm 45062 nfermltl2rev 45206 sepfsepc 46232 |
Copyright terms: Public domain | W3C validator |