Theorem 1lt2 12300

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 11121	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12035	. 2 ⊢ 1 < (1 + 1)
3		df-2 12197	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5122	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5095  (class class class)co 7354  1c1 11016   + caddc 11018   < clt 11155  2c2 12189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-resscn 11072  ax-1cn 11073  ax-icn 11074  ax-addcl 11075  ax-addrcl 11076  ax-mulcl 11077  ax-mulrcl 11078  ax-mulcom 11079  ax-addass 11080  ax-mulass 11081  ax-distr 11082  ax-i2m1 11083  ax-1ne0 11084  ax-1rid 11085  ax-rnegex 11086  ax-rrecex 11087  ax-cnre 11088  ax-pre-lttri 11089  ax-pre-lttrn 11090  ax-pre-ltadd 11091  ax-pre-mulgt0 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7311  df-ov 7357  df-oprab 7358  df-mpo 7359  df-er 8630  df-en 8878  df-dom 8879  df-sdom 8880  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160  df-le 11161  df-sub 11355  df-neg 11356  df-2 12197

This theorem is referenced by:  1lt3  12302  1lt4  12305  1lt6  12314  1lt7  12320  1lt8  12327  1lt9  12335  1ne2  12337  1le2  12338  halflt1  12347  nn0n0n1ge2b  12459  nn0ge2m1nn  12460  halfnz  12559  1lt10  12735  fztpval  13490  ige2m2fzo  13632  faclbnd5  14209  hashgt23el  14335  hashfun  14348  hashge2el2dif  14391  tpf1ofv2  14409  wrdlenge2n0  14463  ccat2s1p2  14542  s3fv1  14803  pfx2  14858  wwlktovf  14867  sqrt2gt1lt2  15185  ege2le3  16001  ene1  16123  mod2eq1n2dvds  16262  bits0o  16345  bitsfzolem  16349  bitsfzo  16350  bitsfi  16352  2prm  16607  4nprm  16610  iserodd  16751  dec2dvds  16979  dec5nprm  16982  dec2nprm  16983  2expltfac  17008  5prm  17024  6nprm  17025  7prm  17026  8nprm  17027  10nprm  17029  11prm  17030  13prm  17031  17prm  17032  19prm  17033  37prm  17036  83prm  17038  317prm  17041  631prm  17042  basendxltplusgndx  17194  rngstr  17206  lmodstr  17233  topgrpstr  17269  psgnunilem2  19411  isnzr2hash  20438  dyadss  25525  opnmbllem  25532  lhop1lem  25948  aaliou3lem8  26283  zetacvg  26955  lgamgulmlem4  26972  ppi1  27104  cht1  27105  chtrpcl  27115  ppiltx  27117  chtub  27153  chpval2  27159  mersenne  27168  perfectlem1  27170  perfectlem2  27171  bpos1  27224  bposlem1  27225  bposlem6  27230  bposlem7  27231  bposlem8  27232  lgseisenlem1  27316  2sqblem  27372  chebbnd1lem1  27410  chebbnd1lem3  27412  chebbnd1  27413  chtppilimlem1  27414  chtppilimlem2  27415  chtppilim  27416  chto1ub  27417  chebbnd2  27418  chto1lb  27419  mulog2sumlem2  27476  pntrmax  27505  pntrlog2bndlem2  27519  pntrlog2bndlem4  27521  pntpbnd1a  27526  pntibndlem3  27533  pntibnd  27534  pntlemb  27538  pntlemk  27547  pnt  27555  axlowdim  28943  lfgrnloop  29107  lfuhgr1v0e  29236  nbusgrvtxm1  29361  cusgrsizeindb1  29433  lfgrwlkprop  29668  usgr2pthlem  29745  uspgrn2crct  29790  clwlkclwwlklem2fv2  29980  clwwlkext2edg  30040  eupth2lem3lem4  30215  ex-mod  30433  9p10ne21  30454  cshw1s2  32950  drngidlhash  33408  rtelextdg2lem  33762  fib1  34436  ballotlem2  34525  chtvalz  34665  hgt750lemd  34684  hgt750lem  34687  hgt750leme  34694  lfuhgr2  35186  subfacp1lem1  35246  subfacp1lem5  35251  knoppndvlem12  36590  knoppndvlem18  36596  relowlpssretop  37431  tan2h  37675  opnmbllem0  37719  heiborlem7  37880  lcmineqlem22  42166  3lexlogpow5ineq2  42171  3lexlogpow5ineq4  42172  3lexlogpow5ineq3  42173  3lexlogpow2ineq1  42174  3lexlogpow2ineq2  42175  3lexlogpow5ineq5  42176  aks4d1lem1  42178  dvrelog2b  42182  dvrelogpow2b  42184  aks4d1p1p3  42185  aks4d1p1p2  42186  aks4d1p1p4  42187  aks4d1p1p6  42189  aks4d1p1p7  42190  aks4d1p1p5  42191  aks4d1p1  42192  aks4d1p2  42193  aks4d1p3  42194  aks4d1p5  42196  aks4d1p6  42197  aks4d1p7d1  42198  aks4d1p7  42199  aks4d1p8  42203  aks4d1p9  42204  aks6d1c3  42239  aks6d1c6lem4  42289  aks6d1c7lem2  42297  flt4lem7  42780  pellfundgt1  43003  stoweidlem13  46138  stoweidlem26  46151  wallispilem4  46193  wallispi  46195  wallispi2lem1  46196  wallispi2lem2  46197  wallispi2  46198  stirlinglem1  46199  dirkertrigeqlem1  46223  dirkercncflem1  46228  fouriersw  46356  etransclem23  46382  salexct2  46464  nthrucw  47011  ceilhalfgt1  47456  ceil5half3  47467  difmodm1lt  47486  fmtnoge3  47657  fmtnof1  47662  fmtno4prm  47702  2pwp1prm  47716  127prm  47726  sfprmdvdsmersenne  47730  lighneallem2  47733  dfodd4  47786  perfectALTVlem1  47848  perfectALTVlem2  47849  nnsum4primesevenALTV  47928  gpgprismgrusgra  48185  cznnring  48389  pw2m1lepw2m1  48648  rege1logbzge0  48687  logbpw2m1  48695  fllog2  48696  blenpw2m1  48707  nnpw2blen  48708  dignn0flhalflem1  48743