Theorem 1lt2 12352

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 12087	. 2 ⊢ 1 < (1 + 1)
3		df-2 12249	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5134	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5107  (class class class)co 7387  1c1 11069   + caddc 11071   < clt 11208  2c2 12241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-2 12249

This theorem is referenced by:  1lt3  12354  1lt4  12357  1lt6  12366  1lt7  12372  1lt8  12379  1lt9  12387  1ne2  12389  1le2  12390  halflt1  12399  nn0n0n1ge2b  12511  nn0ge2m1nn  12512  halfnz  12612  1lt10  12788  fztpval  13547  ige2m2fzo  13689  faclbnd5  14263  hashgt23el  14389  hashfun  14402  hashge2el2dif  14445  tpf1ofv2  14463  wrdlenge2n0  14517  ccat2s1p2  14595  s3fv1  14858  pfx2  14913  wwlktovf  14922  sqrt2gt1lt2  15240  ege2le3  16056  ene1  16178  mod2eq1n2dvds  16317  bits0o  16400  bitsfzolem  16404  bitsfzo  16405  bitsfi  16407  2prm  16662  4nprm  16665  iserodd  16806  dec2dvds  17034  dec5nprm  17037  dec2nprm  17038  2expltfac  17063  5prm  17079  6nprm  17080  7prm  17081  8nprm  17082  10nprm  17084  11prm  17085  13prm  17086  17prm  17087  19prm  17088  37prm  17091  83prm  17093  317prm  17096  631prm  17097  basendxltplusgndx  17249  rngstr  17261  lmodstr  17288  topgrpstr  17324  psgnunilem2  19425  isnzr2hash  20428  dyadss  25495  opnmbllem  25502  lhop1lem  25918  aaliou3lem8  26253  zetacvg  26925  lgamgulmlem4  26942  ppi1  27074  cht1  27075  chtrpcl  27085  ppiltx  27087  chtub  27123  chpval2  27129  mersenne  27138  perfectlem1  27140  perfectlem2  27141  bpos1  27194  bposlem1  27195  bposlem6  27200  bposlem7  27201  bposlem8  27202  lgseisenlem1  27286  2sqblem  27342  chebbnd1lem1  27380  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chtppilimlem2  27385  chtppilim  27386  chto1ub  27387  chebbnd2  27388  chto1lb  27389  mulog2sumlem2  27446  pntrmax  27475  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntpbnd1a  27496  pntibndlem3  27503  pntibnd  27504  pntlemb  27508  pntlemk  27517  pnt  27525  axlowdim  28888  lfgrnloop  29052  lfuhgr1v0e  29181  nbusgrvtxm1  29306  cusgrsizeindb1  29378  lfgrwlkprop  29615  usgr2pthlem  29693  uspgrn2crct  29738  clwlkclwwlklem2fv2  29925  clwwlkext2edg  29985  eupth2lem3lem4  30160  ex-mod  30378  9p10ne21  30399  cshw1s2  32882  drngidlhash  33405  rtelextdg2lem  33716  fib1  34391  ballotlem2  34480  chtvalz  34620  hgt750lemd  34639  hgt750lem  34642  hgt750leme  34649  lfuhgr2  35106  subfacp1lem1  35166  subfacp1lem5  35171  knoppndvlem12  36511  knoppndvlem18  36517  relowlpssretop  37352  tan2h  37606  opnmbllem0  37650  heiborlem7  37811  lcmineqlem22  42038  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  dvrelog2b  42054  dvrelogpow2b  42056  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  aks6d1c3  42111  aks6d1c6lem4  42161  aks6d1c7lem2  42169  flt4lem7  42647  pellfundgt1  42871  stoweidlem13  46011  stoweidlem26  46024  wallispilem4  46066  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  dirkertrigeqlem1  46096  dirkercncflem1  46101  fouriersw  46229  etransclem23  46255  salexct2  46337  ceilhalfgt1  47330  ceil5half3  47341  difmodm1lt  47360  fmtnoge3  47531  fmtnof1  47536  fmtno4prm  47576  2pwp1prm  47590  127prm  47600  sfprmdvdsmersenne  47604  lighneallem2  47607  dfodd4  47660  perfectALTVlem1  47722  perfectALTVlem2  47723  nnsum4primesevenALTV  47802  gpgprismgrusgra  48049  cznnring  48250  pw2m1lepw2m1  48509  rege1logbzge0  48548  logbpw2m1  48556  fllog2  48557  blenpw2m1  48568  nnpw2blen  48569  dignn0flhalflem1  48604