![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2lt3 | Structured version Visualization version GIF version |
Description: 2 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Ref | Expression |
---|---|
2lt3 | ⊢ 2 < 3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2re 11565 | . . 3 ⊢ 2 ∈ ℝ | |
2 | 1 | ltp1i 11398 | . 2 ⊢ 2 < (2 + 1) |
3 | df-3 11555 | . 2 ⊢ 3 = (2 + 1) | |
4 | 2, 3 | breqtrri 4995 | 1 ⊢ 2 < 3 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 4968 (class class class)co 7023 1c1 10391 + caddc 10393 < clt 10528 2c2 11546 3c3 11547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 ax-pre-mulgt0 10467 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-po 5369 df-so 5370 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-er 8146 df-en 8365 df-dom 8366 df-sdom 8367 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-sub 10725 df-neg 10726 df-2 11554 df-3 11555 |
This theorem is referenced by: 1lt3 11664 2lt4 11666 2lt6 11675 2lt7 11681 2lt8 11688 2lt9 11696 3halfnz 11915 2lt10 12090 uzuzle23 12142 uz3m2nn 12144 fztpval 12823 expnass 13424 s4fv2 14099 f1oun2prg 14119 caucvgrlem 14867 cos01gt0 15381 3lcm2e6 15905 5prm 16275 11prm 16281 17prm 16283 23prm 16285 83prm 16289 317prm 16292 4001lem4 16310 plusgndxnmulrndx 16450 rngstr 16452 oppradd 19074 cnfldstr 20233 cnfldfun 20243 2logb9irr 25058 2logb3irr 25060 log2le1 25214 chtub 25474 bpos1 25545 bposlem6 25551 chto1ub 25738 dchrvmasumiflem1 25763 istrkg3ld 25933 tgcgr4 26003 axlowdimlem2 26416 axlowdimlem16 26430 axlowdimlem17 26431 axlowdim 26434 usgrexmpldifpr 26727 upgr3v3e3cycl 27645 konigsbergiedgw 27713 konigsberglem1 27717 konigsberglem2 27718 konigsberglem3 27719 ex-pss 27895 ex-res 27908 ex-fv 27910 ex-fl 27914 ex-mod 27916 prodfzo03 31487 cnndvlem1 33487 poimirlem9 34453 rabren3dioph 38918 jm2.20nn 39100 wallispilem4 41917 fourierdlem87 42042 smfmullem4 42633 257prm 43227 31prm 43264 9fppr8 43406 fpprel2 43410 nnsum3primes4 43457 nnsum3primesgbe 43461 nnsum3primesle9 43463 nnsum4primesodd 43465 nnsum4primesoddALTV 43466 tgoldbach 43486 zlmodzxznm 44054 zlmodzxzldeplem 44055 |
Copyright terms: Public domain | W3C validator |