Theorem 1lt2 12409

Description: 1 is less than 2. (Contributed by NM, 24-Feb-2005.)

Assertion

Ref	Expression
1lt2	⊢ 1 < 2

Proof of Theorem 1lt2

Step	Hyp	Ref	Expression
1		1re 11233	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12144	. 2 ⊢ 1 < (1 + 1)
3		df-2 12301	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5146	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5119  (class class class)co 7403  1c1 11128   + caddc 11130   < clt 11267  2c2 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-2 12301

This theorem is referenced by:  1lt3  12411  1lt4  12414  1lt6  12423  1lt7  12429  1lt8  12436  1lt9  12444  1ne2  12446  1le2  12447  halflt1  12456  nn0n0n1ge2b  12568  nn0ge2m1nn  12569  halfnz  12669  1lt10  12845  fztpval  13601  ige2m2fzo  13742  faclbnd5  14314  hashgt23el  14440  hashfun  14453  hashge2el2dif  14496  tpf1ofv2  14514  wrdlenge2n0  14568  ccat2s1p2  14646  s3fv1  14909  pfx2  14964  wwlktovf  14973  sqrt2gt1lt2  15291  ege2le3  16104  ene1  16226  mod2eq1n2dvds  16364  bits0o  16447  bitsfzolem  16451  bitsfzo  16452  bitsfi  16454  2prm  16709  4nprm  16712  iserodd  16853  dec2dvds  17081  dec5nprm  17084  dec2nprm  17085  2expltfac  17110  5prm  17126  6nprm  17127  7prm  17128  8nprm  17129  10nprm  17131  11prm  17132  13prm  17133  17prm  17134  19prm  17135  37prm  17138  83prm  17140  317prm  17143  631prm  17144  basendxltplusgndx  17298  rngstr  17310  lmodstr  17337  topgrpstr  17373  psgnunilem2  19474  isnzr2hash  20477  dyadss  25545  opnmbllem  25552  lhop1lem  25968  aaliou3lem8  26303  zetacvg  26975  lgamgulmlem4  26992  ppi1  27124  cht1  27125  chtrpcl  27135  ppiltx  27137  chtub  27173  chpval2  27179  mersenne  27188  perfectlem1  27190  perfectlem2  27191  bpos1  27244  bposlem1  27245  bposlem6  27250  bposlem7  27251  bposlem8  27252  lgseisenlem1  27336  2sqblem  27392  chebbnd1lem1  27430  chebbnd1lem3  27432  chebbnd1  27433  chtppilimlem1  27434  chtppilimlem2  27435  chtppilim  27436  chto1ub  27437  chebbnd2  27438  chto1lb  27439  mulog2sumlem2  27496  pntrmax  27525  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntpbnd1a  27546  pntibndlem3  27553  pntibnd  27554  pntlemb  27558  pntlemk  27567  pnt  27575  axlowdim  28886  lfgrnloop  29050  lfuhgr1v0e  29179  nbusgrvtxm1  29304  cusgrsizeindb1  29376  lfgrwlkprop  29613  usgr2pthlem  29691  uspgrn2crct  29736  clwlkclwwlklem2fv2  29923  clwwlkext2edg  29983  eupth2lem3lem4  30158  ex-mod  30376  9p10ne21  30397  cshw1s2  32882  drngidlhash  33395  rtelextdg2lem  33706  fib1  34378  ballotlem2  34467  chtvalz  34607  hgt750lemd  34626  hgt750lem  34629  hgt750leme  34636  lfuhgr2  35087  subfacp1lem1  35147  subfacp1lem5  35152  knoppndvlem12  36487  knoppndvlem18  36493  relowlpssretop  37328  tan2h  37582  opnmbllem0  37626  heiborlem7  37787  lcmineqlem22  42009  3lexlogpow5ineq2  42014  3lexlogpow5ineq4  42015  3lexlogpow5ineq3  42016  3lexlogpow2ineq1  42017  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1lem1  42021  dvrelog2b  42025  dvrelogpow2b  42027  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p2  42036  aks4d1p3  42037  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  aks4d1p9  42047  aks6d1c3  42082  aks6d1c6lem4  42132  aks6d1c7lem2  42140  flt4lem7  42629  pellfundgt1  42853  stoweidlem13  45990  stoweidlem26  46003  wallispilem4  46045  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  dirkertrigeqlem1  46075  dirkercncflem1  46080  fouriersw  46208  etransclem23  46234  salexct2  46316  ceilhalfgt1  47306  ceil5half3  47317  fmtnoge3  47492  fmtnof1  47497  fmtno4prm  47537  2pwp1prm  47551  127prm  47561  sfprmdvdsmersenne  47565  lighneallem2  47568  dfodd4  47621  perfectALTVlem1  47683  perfectALTVlem2  47684  nnsum4primesevenALTV  47763  gpgprismgrusgra  48010  cznnring  48185  pw2m1lepw2m1  48444  difmodm1lt  48450  rege1logbzge0  48487  logbpw2m1  48495  fllog2  48496  blenpw2m1  48507  nnpw2blen  48508  dignn0flhalflem1  48543