Theorem 1lt2 12542

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 11335	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12248	. 2 ⊢ 1 < (1 + 1)
3		df-2 12432	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5135	1 ⊢ 1 < 2

This proof depends on syntax axioms:   class class class wbr 5106  (class class class)co 7443  1c1 11228   + caddc 11230   < clt 11370  2c2 12424

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-2 12432

This theorem is used by:  1lt3  12545  1lt4  12548  1lt6  12557  1lt7  12563  1lt8  12570  1lt9  12578  1ne2  12580  1le2  12581  halflt1  12590  nn0n0n1ge2b  12702  nn0ge2m1nn  12703  halfnz  12804  1lt10OLD  12987  fztpval  13747  ige2m2fzo  13890  faclbnd5  14469  hashgt23el  14596  hashfun  14609  hashge2el2dif  14652  tpf1ofv2  14670  wrdlenge2n0  14724  ccat2s1p2  14806  s3fv1  15072  pfx2  15127  wwlktovf  15138  sqrt2gt1lt2  15470  ege2le3  16285  ene1  16407  mod2eq1n2dvds  16546  bits0o  16629  bitsfzolem  16633  bitsfzo  16634  bitsfi  16636  2prm  16896  4nprm  16899  iserodd  17042  dec2dvds  17270  dec5nprm  17273  dec2nprm  17274  2expltfac  17299  5prm  17315  6nprm  17316  7prm  17317  8nprm  17318  10nprmOLD  17321  11prm  17322  13prm  17323  17prm  17324  19prm  17325  37prm  17328  83prm  17330  317prm  17333  631prm  17334  basendxltplusgndx  17486  rngstr  17498  lmodstr  17525  topgrpstr  17561  psgnunilem2  19739  isnzr2hash  20800  dyadss  25945  opnmbllem  25952  lhop1lem  26363  aaliou3lem8  26702  zetacvg  27372  lgamgulmlem4  27389  ppi1  27521  cht1  27522  chtrpcl  27532  ppiltx  27534  chtub  27569  chpval2  27575  mersenne  27584  perfectlem1  27586  perfectlem2  27587  bpos1  27640  bposlem1  27641  bposlem6  27646  bposlem7  27647  bposlem8  27648  lgseisenlem1  27732  2sqblem  27788  chebbnd1lem1  27826  chebbnd1lem3  27828  chebbnd1  27829  chtppilimlem1  27830  chtppilimlem2  27831  chtppilim  27832  chto1ub  27833  chebbnd2  27834  chto1lb  27835  mulog2sumlem2  27892  pntrmax  27921  pntrlog2bndlem2  27935  pntrlog2bndlem4  27937  pntpbnd1a  27942  pntibndlem3  27949  pntibnd  27950  pntlemb  27954  pntlemk  27963  pnt  27971  fltoprmlem2  28024  angmgmlem  29425  angmgmbas  29428  axlowdim  29569  lfgrnloop  29733  lfuhgr2  29757  lfuhgr1v0e  29865  nbusgrvtxm1  29990  cusgrsizeindb1  30061  lfgrwlkprop  30300  usgr2pthlem  30379  uspgrn2crct  30427  clwlkclwwlklem2fv2  30617  clwwlkext2edg  30677  eupth2lem3lem4  30862  ex-mod  31080  9p10ne21  31101  cshw1s2  33591  drngidlhash  34053  rtelextdg2lem  34428  fib1  35102  ballotlem2  35191  chtvalz  35328  hgt750lemd  35347  hgt750lem  35350  hgt750leme  35357  subfacp1lem1  36111  subfacp1lem5  36116  knoppndvlem12  37567  knoppndvlem18  37573  relowlpssretop  38479  tan2h  38727  opnmbllem0  38766  heiborlem7  38943  lcmineqlem22  43292  3lexlogpow5ineq2  43297  3lexlogpow5ineq4  43298  3lexlogpow5ineq3  43299  3lexlogpow2ineq1  43300  3lexlogpow2ineq2  43301  3lexlogpow5ineq5  43302  aks4d1lem1  43304  dvrelog2b  43308  dvrelogpow2b  43310  aks4d1p1p3  43311  aks4d1p1p2  43312  aks4d1p1p4  43313  aks4d1p1p6  43315  aks4d1p1p7  43316  aks4d1p1p5  43317  aks4d1p1  43318  aks4d1p2  43319  aks4d1p3  43320  aks4d1p5  43322  aks4d1p6  43323  aks4d1p7d1  43324  aks4d1p7  43325  aks4d1p8  43329  aks4d1p9  43330  aks6d1c3  43365  aks6d1c6lem4  43415  aks6d1c7lem2  43423  pellfundgt1  44083  stoweidlem13  47228  stoweidlem26  47241  wallispilem4  47283  wallispi  47285  wallispi2lem1  47286  wallispi2lem2  47287  wallispi2  47288  stirlinglem1  47289  dirkertrigeqlem1  47313  dirkercncflem1  47318  fouriersw  47446  etransclem23  47472  salexct2  47554  numtowerdt  48121  ceilhalfgt1  48608  ceil5half3  48621  difmodm1lt  48640  2timesltsqm1  48654  fmtnoge3  48820  fmtnof1  48825  fmtno4prm  48865  2pwp1prm  48879  127prm  48889  sfprmdvdsmersenne  48893  lighneallem2  48896  nprmdvdsfacm1lem4  48913  ppivalnn  48922  dfodd4  48962  perfectALTVlem1  49024  perfectALTVlem2  49025  nnsum4primesevenALTV  49104  gpgprismgrusgra  49361  cznnring  49564  pw2m1lepw2m1  49837  rege1logbzge0  49876  logbpw2m1  49884  fllog2  49885  blenpw2m1  49896  nnpw2blen  49897  dignn0flhalflem1  49932