Theorem 1lt2 11800

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 10633	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 11536	. 2 ⊢ 1 < (1 + 1)
3		df-2 11692	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5084	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5057  (class class class)co 7148  1c1 10530   + caddc 10532   < clt 10667  2c2 11684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-2 11692

This theorem is referenced by:  1lt3  11802  1lt4  11805  1lt6  11814  1lt7  11820  1lt8  11827  1lt9  11835  1ne2  11837  1le2  11838  halflt1  11847  nn0n0n1ge2b  11955  nn0ge2m1nn  11956  halfnz  12052  1lt10  12229  fztpval  12961  ige2m2fzo  13092  faclbnd5  13650  hashgt23el  13777  hashfun  13790  hashge2el2dif  13830  wrdlenge2n0  13896  ccat2s1p2  13978  ccat2s1p2OLD  13980  s3fv1  14246  pfx2  14301  wwlktovf  14312  sqrt2gt1lt2  14626  ege2le3  15435  ene1  15555  mod2eq1n2dvds  15688  n2dvds1OLD  15710  bits0o  15771  bitsfzolem  15775  bitsfzo  15776  bitsfi  15778  2prm  16028  4nprm  16031  iserodd  16164  dec2dvds  16391  dec5nprm  16394  dec2nprm  16395  2expltfac  16418  5prm  16434  6nprm  16435  7prm  16436  8nprm  16437  10nprm  16439  11prm  16440  13prm  16441  17prm  16442  19prm  16443  37prm  16446  83prm  16448  317prm  16451  631prm  16452  grpstr  16601  grpbase  16602  grpplusg  16603  ressplusg  16604  rngstr  16611  lmodstr  16628  topgrpstr  16653  psgnunilem2  18615  isnzr2hash  20029  dyadss  24187  opnmbllem  24194  lhop1lem  24602  aaliou3lem8  24926  zetacvg  25584  lgamgulmlem4  25601  ppi1  25733  cht1  25734  chtrpcl  25744  ppiltx  25746  chtub  25780  chpval2  25786  mersenne  25795  perfectlem1  25797  perfectlem2  25798  bpos1  25851  bposlem1  25852  bposlem6  25857  bposlem7  25858  bposlem8  25859  lgseisenlem1  25943  2sqblem  25999  chebbnd1lem1  26037  chebbnd1lem3  26039  chebbnd1  26040  chtppilimlem1  26041  chtppilimlem2  26042  chtppilim  26043  chto1ub  26044  chebbnd2  26045  chto1lb  26046  mulog2sumlem2  26103  pntrmax  26132  pntrlog2bndlem2  26146  pntrlog2bndlem4  26148  pntpbnd1a  26153  pntibndlem3  26160  pntibnd  26161  pntlemb  26165  pntlemk  26174  pnt  26182  axlowdim  26739  lfgrnloop  26902  lfuhgr1v0e  27028  nbusgrvtxm1  27153  cusgrsizeindb1  27224  lfgrwlkprop  27461  usgr2pthlem  27536  uspgrn2crct  27578  clwlkclwwlklem2fv2  27766  clwwlkext2edg  27827  eupth2lem3lem4  28002  ex-mod  28220  9p10ne21  28241  cshw1s2  30627  fib1  31651  ballotlem2  31739  chtvalz  31893  hgt750lemd  31912  hgt750lem  31915  hgt750leme  31922  lfuhgr2  32358  subfacp1lem1  32419  subfacp1lem5  32424  knoppndvlem12  33855  knoppndvlem18  33861  relowlpssretop  34637  tan2h  34876  opnmbllem0  34920  heiborlem7  35087  pellfundgt1  39470  stoweidlem13  42288  stoweidlem26  42301  wallispilem4  42343  wallispi  42345  wallispi2lem1  42346  wallispi2lem2  42347  wallispi2  42348  stirlinglem1  42349  dirkertrigeqlem1  42373  dirkercncflem1  42378  fouriersw  42506  etransclem23  42532  salexct2  42612  fmtnoge3  43682  fmtnof1  43687  fmtno4prm  43727  2pwp1prm  43741  127prm  43753  sfprmdvdsmersenne  43758  lighneallem2  43761  dfodd4  43814  perfectALTVlem1  43876  perfectALTVlem2  43877  nnsum4primesevenALTV  43956  cznnring  44217  pw2m1lepw2m1  44565  difmodm1lt  44572  rege1logbzge0  44609  logbpw2m1  44617  fllog2  44618  blenpw2m1  44629  nnpw2blen  44630  dignn0flhalflem1  44665