Theorem 1lt2 12401

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 11196	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12107	. 2 ⊢ 1 < (1 + 1)
3		df-2 12291	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5131	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5104  (class class class)co 7400  1c1 11089   + caddc 11091   < clt 11231  2c2 12283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-2 12291

This theorem is referenced by:  1lt3  12404  1lt4  12407  1lt6  12416  1lt7  12422  1lt8  12429  1lt9  12437  1ne2  12439  1le2  12440  halflt1  12449  nn0n0n1ge2b  12561  nn0ge2m1nn  12562  halfnz  12662  1lt10OLD  12845  fztpval  13602  ige2m2fzo  13745  faclbnd5  14322  hashgt23el  14449  hashfun  14462  hashge2el2dif  14505  tpf1ofv2  14523  wrdlenge2n0  14577  ccat2s1p2  14656  s3fv1  14917  pfx2  14972  wwlktovf  14981  sqrt2gt1lt2  15313  ege2le3  16132  ene1  16254  mod2eq1n2dvds  16393  bits0o  16476  bitsfzolem  16480  bitsfzo  16481  bitsfi  16483  2prm  16738  4nprm  16741  iserodd  16883  dec2dvds  17111  dec5nprm  17114  dec2nprm  17115  2expltfac  17140  5prm  17156  6nprm  17157  7prm  17158  8nprm  17159  10nprmOLD  17162  11prm  17163  13prm  17164  17prm  17165  19prm  17166  37prm  17169  83prm  17171  317prm  17174  631prm  17175  basendxltplusgndx  17327  rngstr  17339  lmodstr  17366  topgrpstr  17402  psgnunilem2  19553  isnzr2hash  20591  dyadss  25710  opnmbllem  25717  lhop1lem  26129  aaliou3lem8  26463  zetacvg  27133  lgamgulmlem4  27150  ppi1  27282  cht1  27283  chtrpcl  27293  ppiltx  27295  chtub  27330  chpval2  27336  mersenne  27345  perfectlem1  27347  perfectlem2  27348  bpos1  27401  bposlem1  27402  bposlem6  27407  bposlem7  27408  bposlem8  27409  lgseisenlem1  27493  2sqblem  27549  chebbnd1lem1  27587  chebbnd1lem3  27589  chebbnd1  27590  chtppilimlem1  27591  chtppilimlem2  27592  chtppilim  27593  chto1ub  27594  chebbnd2  27595  chto1lb  27596  mulog2sumlem2  27653  pntrmax  27682  pntrlog2bndlem2  27696  pntrlog2bndlem4  27698  pntpbnd1a  27703  pntibndlem3  27710  pntibnd  27711  pntlemb  27715  pntlemk  27724  pnt  27732  axlowdim  29216  lfgrnloop  29380  lfuhgr1v0e  29509  nbusgrvtxm1  29634  cusgrsizeindb1  29705  lfgrwlkprop  29940  usgr2pthlem  30017  uspgrn2crct  30062  clwlkclwwlklem2fv2  30252  clwwlkext2edg  30312  eupth2lem3lem4  30487  ex-mod  30705  9p10ne21  30726  cshw1s2  33188  drngidlhash  33653  rtelextdg2lem  34028  fib1  34702  ballotlem2  34791  chtvalz  34928  hgt750lemd  34947  hgt750lem  34950  hgt750leme  34957  lfuhgr2  35477  subfacp1lem1  35537  subfacp1lem5  35542  knoppndvlem12  36969  knoppndvlem18  36975  relowlpssretop  37865  tan2h  38118  opnmbllem0  38162  heiborlem7  38323  lcmineqlem22  42674  3lexlogpow5ineq2  42679  3lexlogpow5ineq4  42680  3lexlogpow5ineq3  42681  3lexlogpow2ineq1  42682  3lexlogpow2ineq2  42683  3lexlogpow5ineq5  42684  aks4d1lem1  42686  dvrelog2b  42690  dvrelogpow2b  42692  aks4d1p1p3  42693  aks4d1p1p2  42694  aks4d1p1p4  42695  aks4d1p1p6  42697  aks4d1p1p7  42698  aks4d1p1p5  42699  aks4d1p1  42700  aks4d1p2  42701  aks4d1p3  42702  aks4d1p5  42704  aks4d1p6  42705  aks4d1p7d1  42706  aks4d1p7  42707  aks4d1p8  42711  aks4d1p9  42712  aks6d1c3  42747  aks6d1c6lem4  42797  aks6d1c7lem2  42805  flt4lem7  43248  pellfundgt1  43467  stoweidlem13  46586  stoweidlem26  46599  wallispilem4  46641  wallispi  46643  wallispi2lem1  46644  wallispi2lem2  46645  wallispi2  46646  stirlinglem1  46647  dirkertrigeqlem1  46671  dirkercncflem1  46676  fouriersw  46804  etransclem23  46830  salexct2  46912  nthrucw  47461  ceilhalfgt1  47926  ceil5half3  47939  difmodm1lt  47958  2timesltsqm1  47972  fmtnoge3  48138  fmtnof1  48143  fmtno4prm  48183  2pwp1prm  48197  127prm  48207  sfprmdvdsmersenne  48211  lighneallem2  48214  nprmdvdsfacm1lem4  48231  ppivalnn  48240  dfodd4  48280  perfectALTVlem1  48342  perfectALTVlem2  48343  nnsum4primesevenALTV  48422  gpgprismgrusgra  48679  cznnring  48883  pw2m1lepw2m1  49152  rege1logbzge0  49191  logbpw2m1  49199  fllog2  49200  blenpw2m1  49211  nnpw2blen  49212  dignn0flhalflem1  49247