Theorem 1lt2 12345

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 11142	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12058	. 2 ⊢ 1 < (1 + 1)
3		df-2 12242	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5106	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5079  (class class class)co 7363  1c1 11037   + caddc 11039   < clt 11177  2c2 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-2 12242

This theorem is referenced by:  1lt3  12347  1lt4  12350  1lt6  12359  1lt7  12365  1lt8  12372  1lt9  12380  1ne2  12382  1le2  12383  halflt1  12392  nn0n0n1ge2b  12504  nn0ge2m1nn  12505  halfnz  12605  1lt10  12781  fztpval  13538  ige2m2fzo  13681  faclbnd5  14258  hashgt23el  14384  hashfun  14397  hashge2el2dif  14440  tpf1ofv2  14458  wrdlenge2n0  14512  ccat2s1p2  14591  s3fv1  14852  pfx2  14907  wwlktovf  14916  sqrt2gt1lt2  15234  ege2le3  16053  ene1  16175  mod2eq1n2dvds  16314  bits0o  16397  bitsfzolem  16401  bitsfzo  16402  bitsfi  16404  2prm  16659  4nprm  16662  iserodd  16804  dec2dvds  17032  dec5nprm  17035  dec2nprm  17036  2expltfac  17061  5prm  17077  6nprm  17078  7prm  17079  8nprm  17080  10nprm  17082  11prm  17083  13prm  17084  17prm  17085  19prm  17086  37prm  17089  83prm  17091  317prm  17094  631prm  17095  basendxltplusgndx  17247  rngstr  17259  lmodstr  17286  topgrpstr  17322  psgnunilem2  19468  isnzr2hash  20498  dyadss  25586  opnmbllem  25593  lhop1lem  26005  aaliou3lem8  26336  zetacvg  27003  lgamgulmlem4  27020  ppi1  27152  cht1  27153  chtrpcl  27163  ppiltx  27165  chtub  27200  chpval2  27206  mersenne  27215  perfectlem1  27217  perfectlem2  27218  bpos1  27271  bposlem1  27272  bposlem6  27277  bposlem7  27278  bposlem8  27279  lgseisenlem1  27363  2sqblem  27419  chebbnd1lem1  27457  chebbnd1lem3  27459  chebbnd1  27460  chtppilimlem1  27461  chtppilimlem2  27462  chtppilim  27463  chto1ub  27464  chebbnd2  27465  chto1lb  27466  mulog2sumlem2  27523  pntrmax  27552  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntpbnd1a  27573  pntibndlem3  27580  pntibnd  27581  pntlemb  27585  pntlemk  27594  pnt  27602  axlowdim  29055  lfgrnloop  29219  lfuhgr1v0e  29348  nbusgrvtxm1  29473  cusgrsizeindb1  29544  lfgrwlkprop  29779  usgr2pthlem  29856  uspgrn2crct  29901  clwlkclwwlklem2fv2  30091  clwwlkext2edg  30151  eupth2lem3lem4  30326  ex-mod  30544  9p10ne21  30565  cshw1s2  33046  drngidlhash  33524  rtelextdg2lem  33917  fib1  34591  ballotlem2  34680  chtvalz  34820  hgt750lemd  34839  hgt750lem  34842  hgt750leme  34849  lfuhgr2  35354  subfacp1lem1  35414  subfacp1lem5  35419  knoppndvlem12  36836  knoppndvlem18  36842  relowlpssretop  37733  tan2h  37986  opnmbllem0  38030  heiborlem7  38191  lcmineqlem22  42542  3lexlogpow5ineq2  42547  3lexlogpow5ineq4  42548  3lexlogpow5ineq3  42549  3lexlogpow2ineq1  42550  3lexlogpow2ineq2  42551  3lexlogpow5ineq5  42552  aks4d1lem1  42554  dvrelog2b  42558  dvrelogpow2b  42560  aks4d1p1p3  42561  aks4d1p1p2  42562  aks4d1p1p4  42563  aks4d1p1p6  42565  aks4d1p1p7  42566  aks4d1p1p5  42567  aks4d1p1  42568  aks4d1p2  42569  aks4d1p3  42570  aks4d1p5  42572  aks4d1p6  42573  aks4d1p7d1  42574  aks4d1p7  42575  aks4d1p8  42579  aks4d1p9  42580  aks6d1c3  42615  aks6d1c6lem4  42665  aks6d1c7lem2  42673  flt4lem7  43116  pellfundgt1  43335  stoweidlem13  46463  stoweidlem26  46476  wallispilem4  46518  wallispi  46520  wallispi2lem1  46521  wallispi2lem2  46522  wallispi2  46523  stirlinglem1  46524  dirkertrigeqlem1  46548  dirkercncflem1  46553  fouriersw  46681  etransclem23  46707  salexct2  46789  nthrucw  47338  ceilhalfgt1  47803  ceil5half3  47816  difmodm1lt  47835  2timesltsqm1  47849  fmtnoge3  48015  fmtnof1  48020  fmtno4prm  48060  2pwp1prm  48074  127prm  48084  sfprmdvdsmersenne  48088  lighneallem2  48091  nprmdvdsfacm1lem4  48108  ppivalnn  48117  dfodd4  48157  perfectALTVlem1  48219  perfectALTVlem2  48220  nnsum4primesevenALTV  48299  gpgprismgrusgra  48556  cznnring  48760  pw2m1lepw2m1  49018  rege1logbzge0  49057  logbpw2m1  49065  fllog2  49066  blenpw2m1  49077  nnpw2blen  49078  dignn0flhalflem1  49113