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 11901 | . . 3 ⊢ 2 ∈ ℝ | |
2 | 1 | ltp1i 11733 | . 2 ⊢ 2 < (2 + 1) |
3 | df-3 11891 | . 2 ⊢ 3 = (2 + 1) | |
4 | 2, 3 | breqtrri 5077 | 1 ⊢ 2 < 3 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 5050 (class class class)co 7210 1c1 10727 + caddc 10729 < clt 10864 2c2 11882 3c3 11883 |
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-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-2 11890 df-3 11891 |
This theorem is referenced by: 1lt3 12000 2lt4 12002 2lt6 12011 2lt7 12017 2lt8 12024 2lt9 12032 3halfnz 12253 2lt10 12428 uzuzle23 12482 uz3m2nn 12484 fztpval 13171 expnass 13773 s4fv2 14459 f1oun2prg 14479 caucvgrlem 15233 cos01gt0 15749 3lcm2e6 16285 5prm 16659 11prm 16665 17prm 16667 23prm 16669 83prm 16673 317prm 16676 4001lem4 16694 plusgndxnmulrndx 16837 rngstr 16838 oppradd 19645 cnfldstr 20362 cnfldfun 20372 2logb9irr 25675 2logb3irr 25677 log2le1 25830 chtub 26090 bpos1 26161 bposlem6 26167 chto1ub 26354 dchrvmasumiflem1 26379 istrkg3ld 26549 tgcgr4 26619 axlowdimlem2 27031 axlowdimlem16 27045 axlowdimlem17 27046 axlowdim 27049 usgrexmpldifpr 27343 upgr3v3e3cycl 28260 konigsbergiedgw 28328 konigsberglem1 28332 konigsberglem2 28333 konigsberglem3 28334 ex-pss 28508 ex-res 28521 ex-fv 28523 ex-fl 28527 ex-mod 28529 prodfzo03 32292 cnndvlem1 34451 poimirlem9 35521 3lexlogpow2ineq1 39798 aks4d1p1p6 39812 aks4d1p1p5 39814 2ap1caineq 39821 rabren3dioph 40338 jm2.20nn 40520 mnringaddgd 41509 wallispilem4 43282 fourierdlem87 43407 smfmullem4 43998 257prm 44684 31prm 44720 9fppr8 44860 fpprel2 44864 nnsum3primes4 44911 nnsum3primesgbe 44915 nnsum3primesle9 44917 nnsum4primesodd 44919 nnsum4primesoddALTV 44920 tgoldbach 44940 zlmodzxznm 45509 zlmodzxzldeplem 45510 sepfsepc 45892 |
Copyright terms: Public domain | W3C validator |