Theorem 1lt2 12496

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 11289	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12202	. 2 ⊢ 1 < (1 + 1)
3		df-2 12386	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5132	1 ⊢ 1 < 2

This proof depends on syntax axioms:   class class class wbr 5103  (class class class)co 7412  1c1 11182   + caddc 11184   < clt 11324  2c2 12378

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  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 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-2 12386

This theorem is used by:  1lt3  12499  1lt4  12502  1lt6  12511  1lt7  12517  1lt8  12524  1lt9  12532  1ne2  12534  1le2  12535  halflt1  12544  nn0n0n1ge2b  12656  nn0ge2m1nn  12657  halfnz  12758  1lt10OLD  12941  fztpval  13700  ige2m2fzo  13843  faclbnd5  14422  hashgt23el  14549  hashfun  14562  hashge2el2dif  14605  tpf1ofv2  14623  wrdlenge2n0  14677  ccat2s1p2  14758  s3fv1  15023  pfx2  15078  wwlktovf  15089  sqrt2gt1lt2  15421  ege2le3  16236  ene1  16358  mod2eq1n2dvds  16497  bits0o  16580  bitsfzolem  16584  bitsfzo  16585  bitsfi  16587  2prm  16847  4nprm  16850  iserodd  16993  dec2dvds  17221  dec5nprm  17224  dec2nprm  17225  2expltfac  17250  5prm  17266  6nprm  17267  7prm  17268  8nprm  17269  10nprmOLD  17272  11prm  17273  13prm  17274  17prm  17275  19prm  17276  37prm  17279  83prm  17281  317prm  17284  631prm  17285  basendxltplusgndx  17437  rngstr  17449  lmodstr  17476  topgrpstr  17512  psgnunilem2  19689  isnzr2hash  20750  dyadss  25895  opnmbllem  25902  lhop1lem  26313  aaliou3lem8  26654  zetacvg  27324  lgamgulmlem4  27341  ppi1  27473  cht1  27474  chtrpcl  27484  ppiltx  27486  chtub  27521  chpval2  27527  mersenne  27536  perfectlem1  27538  perfectlem2  27539  bpos1  27592  bposlem1  27593  bposlem6  27598  bposlem7  27599  bposlem8  27600  lgseisenlem1  27684  2sqblem  27740  chebbnd1lem1  27778  chebbnd1lem3  27780  chebbnd1  27781  chtppilimlem1  27782  chtppilimlem2  27783  chtppilim  27784  chto1ub  27785  chebbnd2  27786  chto1lb  27787  mulog2sumlem2  27844  pntrmax  27873  pntrlog2bndlem2  27887  pntrlog2bndlem4  27889  pntpbnd1a  27894  pntibndlem3  27901  pntibnd  27902  pntlemb  27906  pntlemk  27915  pnt  27923  flt4lem7  27971  fltoprmlem2  27976  angmgmlem  29377  angmgmbas  29380  axlowdim  29521  lfgrnloop  29685  lfuhgr2  29709  lfuhgr1v0e  29817  nbusgrvtxm1  29942  cusgrsizeindb1  30013  lfgrwlkprop  30252  usgr2pthlem  30331  uspgrn2crct  30379  clwlkclwwlklem2fv2  30569  clwwlkext2edg  30629  eupth2lem3lem4  30814  ex-mod  31032  9p10ne21  31053  cshw1s2  33503  drngidlhash  33965  rtelextdg2lem  34340  fib1  35015  ballotlem2  35104  chtvalz  35241  hgt750lemd  35260  hgt750lem  35263  hgt750leme  35270  subfacp1lem1  35913  subfacp1lem5  35918  knoppndvlem12  37359  knoppndvlem18  37365  relowlpssretop  38255  tan2h  38503  opnmbllem0  38542  heiborlem7  38719  lcmineqlem22  43068  3lexlogpow5ineq2  43073  3lexlogpow5ineq4  43074  3lexlogpow5ineq3  43075  3lexlogpow2ineq1  43076  3lexlogpow2ineq2  43077  3lexlogpow5ineq5  43078  aks4d1lem1  43080  dvrelog2b  43084  dvrelogpow2b  43086  aks4d1p1p3  43087  aks4d1p1p2  43088  aks4d1p1p4  43089  aks4d1p1p6  43091  aks4d1p1p7  43092  aks4d1p1p5  43093  aks4d1p1  43094  aks4d1p2  43095  aks4d1p3  43096  aks4d1p5  43098  aks4d1p6  43099  aks4d1p7d1  43100  aks4d1p7  43101  aks4d1p8  43105  aks4d1p9  43106  aks6d1c3  43141  aks6d1c6lem4  43191  aks6d1c7lem2  43199  pellfundgt1  43843  stoweidlem13  46967  stoweidlem26  46980  wallispilem4  47022  wallispi  47024  wallispi2lem1  47025  wallispi2lem2  47026  wallispi2  47027  stirlinglem1  47028  dirkertrigeqlem1  47052  dirkercncflem1  47057  fouriersw  47185  etransclem23  47211  salexct2  47293  numtowerdt  47860  ceilhalfgt1  48347  ceil5half3  48360  difmodm1lt  48379  2timesltsqm1  48393  fmtnoge3  48559  fmtnof1  48564  fmtno4prm  48604  2pwp1prm  48618  127prm  48628  sfprmdvdsmersenne  48632  lighneallem2  48635  nprmdvdsfacm1lem4  48652  ppivalnn  48661  dfodd4  48701  perfectALTVlem1  48763  perfectALTVlem2  48764  nnsum4primesevenALTV  48843  gpgprismgrusgra  49100  cznnring  49303  pw2m1lepw2m1  49576  rege1logbzge0  49615  logbpw2m1  49623  fllog2  49624  blenpw2m1  49635  nnpw2blen  49636  dignn0flhalflem1  49671