Theorem 1lt2 12383

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 11174	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12089	. 2 ⊢ 1 < (1 + 1)
3		df-2 12273	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5124	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5097  (class class class)co 7390  1c1 11067   + caddc 11069   < clt 11209  2c2 12265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142  ax-pre-mulgt0 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-sub 11409  df-neg 11410  df-2 12273

This theorem is referenced by:  1lt3  12386  1lt4  12389  1lt6  12398  1lt7  12404  1lt8  12411  1lt9  12419  1ne2  12421  1le2  12422  halflt1  12431  nn0n0n1ge2b  12543  nn0ge2m1nn  12544  halfnz  12644  1lt10OLD  12827  fztpval  13584  ige2m2fzo  13727  faclbnd5  14304  hashgt23el  14430  hashfun  14443  hashge2el2dif  14486  tpf1ofv2  14504  wrdlenge2n0  14558  ccat2s1p2  14637  s3fv1  14898  pfx2  14953  wwlktovf  14962  sqrt2gt1lt2  15291  ege2le3  16110  ene1  16232  mod2eq1n2dvds  16371  bits0o  16454  bitsfzolem  16458  bitsfzo  16459  bitsfi  16461  2prm  16716  4nprm  16719  iserodd  16861  dec2dvds  17089  dec5nprm  17092  dec2nprm  17093  2expltfac  17118  5prm  17134  6nprm  17135  7prm  17136  8nprm  17137  10nprmOLD  17140  11prm  17141  13prm  17142  17prm  17143  19prm  17144  37prm  17147  83prm  17149  317prm  17152  631prm  17153  basendxltplusgndx  17305  rngstr  17317  lmodstr  17344  topgrpstr  17380  psgnunilem2  19525  isnzr2hash  20555  dyadss  25643  opnmbllem  25650  lhop1lem  26062  aaliou3lem8  26396  zetacvg  27066  lgamgulmlem4  27083  ppi1  27215  cht1  27216  chtrpcl  27226  ppiltx  27228  chtub  27263  chpval2  27269  mersenne  27278  perfectlem1  27280  perfectlem2  27281  bpos1  27334  bposlem1  27335  bposlem6  27340  bposlem7  27341  bposlem8  27342  lgseisenlem1  27426  2sqblem  27482  chebbnd1lem1  27520  chebbnd1lem3  27522  chebbnd1  27523  chtppilimlem1  27524  chtppilimlem2  27525  chtppilim  27526  chto1ub  27527  chebbnd2  27528  chto1lb  27529  mulog2sumlem2  27586  pntrmax  27615  pntrlog2bndlem2  27629  pntrlog2bndlem4  27631  pntpbnd1a  27636  pntibndlem3  27643  pntibnd  27644  pntlemb  27648  pntlemk  27657  pnt  27665  axlowdim  29118  lfgrnloop  29282  lfuhgr1v0e  29411  nbusgrvtxm1  29536  cusgrsizeindb1  29607  lfgrwlkprop  29842  usgr2pthlem  29919  uspgrn2crct  29964  clwlkclwwlklem2fv2  30154  clwwlkext2edg  30214  eupth2lem3lem4  30389  ex-mod  30607  9p10ne21  30628  cshw1s2  33098  drngidlhash  33580  rtelextdg2lem  33983  fib1  34657  ballotlem2  34746  chtvalz  34883  hgt750lemd  34902  hgt750lem  34905  hgt750leme  34912  lfuhgr2  35429  subfacp1lem1  35489  subfacp1lem5  35494  knoppndvlem12  36921  knoppndvlem18  36927  relowlpssretop  37818  tan2h  38071  opnmbllem0  38115  heiborlem7  38276  lcmineqlem22  42627  3lexlogpow5ineq2  42632  3lexlogpow5ineq4  42633  3lexlogpow5ineq3  42634  3lexlogpow2ineq1  42635  3lexlogpow2ineq2  42636  3lexlogpow5ineq5  42637  aks4d1lem1  42639  dvrelog2b  42643  dvrelogpow2b  42645  aks4d1p1p3  42646  aks4d1p1p2  42647  aks4d1p1p4  42648  aks4d1p1p6  42650  aks4d1p1p7  42651  aks4d1p1p5  42652  aks4d1p1  42653  aks4d1p2  42654  aks4d1p3  42655  aks4d1p5  42657  aks4d1p6  42658  aks4d1p7d1  42659  aks4d1p7  42660  aks4d1p8  42664  aks4d1p9  42665  aks6d1c3  42700  aks6d1c6lem4  42750  aks6d1c7lem2  42758  flt4lem7  43201  pellfundgt1  43420  stoweidlem13  46547  stoweidlem26  46560  wallispilem4  46602  wallispi  46604  wallispi2lem1  46605  wallispi2lem2  46606  wallispi2  46607  stirlinglem1  46608  dirkertrigeqlem1  46632  dirkercncflem1  46637  fouriersw  46765  etransclem23  46791  salexct2  46873  nthrucw  47422  ceilhalfgt1  47887  ceil5half3  47900  difmodm1lt  47919  2timesltsqm1  47933  fmtnoge3  48099  fmtnof1  48104  fmtno4prm  48144  2pwp1prm  48158  127prm  48168  sfprmdvdsmersenne  48172  lighneallem2  48175  nprmdvdsfacm1lem4  48192  ppivalnn  48201  dfodd4  48241  perfectALTVlem1  48303  perfectALTVlem2  48304  nnsum4primesevenALTV  48383  gpgprismgrusgra  48640  cznnring  48844  pw2m1lepw2m1  49102  rege1logbzge0  49141  logbpw2m1  49149  fllog2  49150  blenpw2m1  49161  nnpw2blen  49162  dignn0flhalflem1  49197