Theorem 1lt2 12417

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 11212	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12123	. 2 ⊢ 1 < (1 + 1)
3		df-2 12307	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5138	1 ⊢ 1 < 2

This proof depends on syntax axioms:   class class class wbr 5109  (class class class)co 7410  1c1 11105   + caddc 11107   < clt 11247  2c2 12299

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180  ax-pre-mulgt0 11181

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11447  df-neg 11448  df-2 12307

This theorem is used by:  1lt3  12420  1lt4  12423  1lt6  12432  1lt7  12438  1lt8  12445  1lt9  12453  1ne2  12455  1le2  12456  halflt1  12465  nn0n0n1ge2b  12577  nn0ge2m1nn  12578  halfnz  12678  1lt10OLD  12861  fztpval  13619  ige2m2fzo  13762  faclbnd5  14339  hashgt23el  14466  hashfun  14479  hashge2el2dif  14522  tpf1ofv2  14540  wrdlenge2n0  14594  ccat2s1p2  14673  s3fv1  14934  pfx2  14989  wwlktovf  14998  sqrt2gt1lt2  15330  ege2le3  16148  ene1  16270  mod2eq1n2dvds  16409  bits0o  16492  bitsfzolem  16496  bitsfzo  16497  bitsfi  16499  2prm  16754  4nprm  16757  iserodd  16899  dec2dvds  17127  dec5nprm  17130  dec2nprm  17131  2expltfac  17156  5prm  17172  6nprm  17173  7prm  17174  8nprm  17175  10nprmOLD  17178  11prm  17179  13prm  17180  17prm  17181  19prm  17182  37prm  17185  83prm  17187  317prm  17190  631prm  17191  basendxltplusgndx  17343  rngstr  17355  lmodstr  17382  topgrpstr  17418  psgnunilem2  19569  isnzr2hash  20626  dyadss  25762  opnmbllem  25769  lhop1lem  26181  aaliou3lem8  26517  zetacvg  27188  lgamgulmlem4  27205  ppi1  27337  cht1  27338  chtrpcl  27348  ppiltx  27350  chtub  27385  chpval2  27391  mersenne  27400  perfectlem1  27402  perfectlem2  27403  bpos1  27456  bposlem1  27457  bposlem6  27462  bposlem7  27463  bposlem8  27464  lgseisenlem1  27548  2sqblem  27604  chebbnd1lem1  27642  chebbnd1lem3  27644  chebbnd1  27645  chtppilimlem1  27646  chtppilimlem2  27647  chtppilim  27648  chto1ub  27649  chebbnd2  27650  chto1lb  27651  mulog2sumlem2  27708  pntrmax  27737  pntrlog2bndlem2  27751  pntrlog2bndlem4  27753  pntpbnd1a  27758  pntibndlem3  27765  pntibnd  27766  pntlemb  27770  pntlemk  27779  pnt  27787  axlowdim  29320  lfgrnloop  29484  lfuhgr1v0e  29613  nbusgrvtxm1  29738  cusgrsizeindb1  29809  lfgrwlkprop  30044  usgr2pthlem  30121  uspgrn2crct  30166  clwlkclwwlklem2fv2  30356  clwwlkext2edg  30416  eupth2lem3lem4  30591  ex-mod  30809  9p10ne21  30830  cshw1s2  33289  drngidlhash  33750  rtelextdg2lem  34125  fib1  34799  ballotlem2  34888  chtvalz  35025  hgt750lemd  35044  hgt750lem  35047  hgt750leme  35054  lfuhgr2  35619  subfacp1lem1  35679  subfacp1lem5  35684  knoppndvlem12  37140  knoppndvlem18  37146  relowlpssretop  38038  tan2h  38291  opnmbllem0  38335  heiborlem7  38496  lcmineqlem22  42845  3lexlogpow5ineq2  42850  3lexlogpow5ineq4  42851  3lexlogpow5ineq3  42852  3lexlogpow2ineq1  42853  3lexlogpow2ineq2  42854  3lexlogpow5ineq5  42855  aks4d1lem1  42857  dvrelog2b  42861  dvrelogpow2b  42863  aks4d1p1p3  42864  aks4d1p1p2  42865  aks4d1p1p4  42866  aks4d1p1p6  42868  aks4d1p1p7  42869  aks4d1p1p5  42870  aks4d1p1  42871  aks4d1p2  42872  aks4d1p3  42873  aks4d1p5  42875  aks4d1p6  42876  aks4d1p7d1  42877  aks4d1p7  42878  aks4d1p8  42882  aks4d1p9  42883  aks6d1c3  42918  aks6d1c6lem4  42968  aks6d1c7lem2  42976  flt4lem7  43419  pellfundgt1  43638  stoweidlem13  46755  stoweidlem26  46768  wallispilem4  46810  wallispi  46812  wallispi2lem1  46813  wallispi2lem2  46814  wallispi2  46815  stirlinglem1  46816  dirkertrigeqlem1  46840  dirkercncflem1  46845  fouriersw  46973  etransclem23  46999  salexct2  47081  nthrucw  47635  ceilhalfgt1  48098  ceil5half3  48111  difmodm1lt  48130  2timesltsqm1  48144  fmtnoge3  48310  fmtnof1  48315  fmtno4prm  48355  2pwp1prm  48369  127prm  48379  sfprmdvdsmersenne  48383  lighneallem2  48386  nprmdvdsfacm1lem4  48403  ppivalnn  48412  dfodd4  48452  perfectALTVlem1  48514  perfectALTVlem2  48515  nnsum4primesevenALTV  48594  gpgprismgrusgra  48851  cznnring  49055  pw2m1lepw2m1  49328  rege1logbzge0  49367  logbpw2m1  49375  fllog2  49376  blenpw2m1  49387  nnpw2blen  49388  dignn0flhalflem1  49423