Theorem 1lt2 12435

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 11264	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12170	. 2 ⊢ 1 < (1 + 1)
3		df-2 12327	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5180	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5153  (class class class)co 7424  1c1 11159   + caddc 11161   < clt 11298  2c2 12319

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 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-2 12327

This theorem is referenced by:  1lt3  12437  1lt4  12440  1lt6  12449  1lt7  12455  1lt8  12462  1lt9  12470  1ne2  12472  1le2  12473  halflt1  12482  nn0n0n1ge2b  12592  nn0ge2m1nn  12593  halfnz  12692  1lt10  12868  fztpval  13617  ige2m2fzo  13749  faclbnd5  14315  hashgt23el  14441  hashfun  14454  hashge2el2dif  14499  wrdlenge2n0  14560  ccat2s1p2  14638  s3fv1  14901  pfx2  14956  wwlktovf  14965  sqrt2gt1lt2  15279  ege2le3  16092  ene1  16212  mod2eq1n2dvds  16349  bits0o  16430  bitsfzolem  16434  bitsfzo  16435  bitsfi  16437  2prm  16693  4nprm  16696  iserodd  16837  dec2dvds  17065  dec5nprm  17068  dec2nprm  17069  2expltfac  17095  5prm  17111  6nprm  17112  7prm  17113  8nprm  17114  10nprm  17116  11prm  17117  13prm  17118  17prm  17119  19prm  17120  37prm  17123  83prm  17125  317prm  17128  631prm  17129  basendxltplusgndx  17295  grpstr  17298  grpbaseOLD  17301  grpplusgOLD  17303  rngstr  17312  lmodstr  17339  topgrpstr  17375  psgnunilem2  19493  isnzr2hash  20501  dyadss  25614  opnmbllem  25621  lhop1lem  26037  aaliou3lem8  26373  zetacvg  27043  lgamgulmlem4  27060  ppi1  27192  cht1  27193  chtrpcl  27203  ppiltx  27205  chtub  27241  chpval2  27247  mersenne  27256  perfectlem1  27258  perfectlem2  27259  bpos1  27312  bposlem1  27313  bposlem6  27318  bposlem7  27319  bposlem8  27320  lgseisenlem1  27404  2sqblem  27460  chebbnd1lem1  27498  chebbnd1lem3  27500  chebbnd1  27501  chtppilimlem1  27502  chtppilimlem2  27503  chtppilim  27504  chto1ub  27505  chebbnd2  27506  chto1lb  27507  mulog2sumlem2  27564  pntrmax  27593  pntrlog2bndlem2  27607  pntrlog2bndlem4  27609  pntpbnd1a  27614  pntibndlem3  27621  pntibnd  27622  pntlemb  27626  pntlemk  27635  pnt  27643  axlowdim  28895  lfgrnloop  29061  lfuhgr1v0e  29190  nbusgrvtxm1  29315  cusgrsizeindb1  29387  lfgrwlkprop  29624  usgr2pthlem  29700  uspgrn2crct  29742  clwlkclwwlklem2fv2  29929  clwwlkext2edg  29989  eupth2lem3lem4  30164  ex-mod  30382  9p10ne21  30403  cshw1s2  32824  drngidlhash  33309  rtelextdg2lem  33604  fib1  34234  ballotlem2  34322  chtvalz  34475  hgt750lemd  34494  hgt750lem  34497  hgt750leme  34504  lfuhgr2  34946  subfacp1lem1  35007  subfacp1lem5  35012  knoppndvlem12  36226  knoppndvlem18  36232  relowlpssretop  37071  tan2h  37313  opnmbllem0  37357  heiborlem7  37518  lcmineqlem22  41749  3lexlogpow5ineq2  41754  3lexlogpow5ineq4  41755  3lexlogpow5ineq3  41756  3lexlogpow2ineq1  41757  3lexlogpow2ineq2  41758  3lexlogpow5ineq5  41759  aks4d1lem1  41761  dvrelog2b  41765  dvrelogpow2b  41767  aks4d1p1p3  41768  aks4d1p1p2  41769  aks4d1p1p4  41770  aks4d1p1p6  41772  aks4d1p1p7  41773  aks4d1p1p5  41774  aks4d1p1  41775  aks4d1p2  41776  aks4d1p3  41777  aks4d1p5  41779  aks4d1p6  41780  aks4d1p7d1  41781  aks4d1p7  41782  aks4d1p8  41786  aks4d1p9  41787  aks6d1c3  41821  aks6d1c6lem4  41871  aks6d1c7lem2  41879  flt4lem7  42313  pellfundgt1  42540  stoweidlem13  45634  stoweidlem26  45647  wallispilem4  45689  wallispi  45691  wallispi2lem1  45692  wallispi2lem2  45693  wallispi2  45694  stirlinglem1  45695  dirkertrigeqlem1  45719  dirkercncflem1  45724  fouriersw  45852  etransclem23  45878  salexct2  45960  fmtnoge3  47102  fmtnof1  47107  fmtno4prm  47147  2pwp1prm  47161  127prm  47171  sfprmdvdsmersenne  47175  lighneallem2  47178  dfodd4  47231  perfectALTVlem1  47293  perfectALTVlem2  47294  nnsum4primesevenALTV  47373  cznnring  47639  pw2m1lepw2m1  47903  difmodm1lt  47910  rege1logbzge0  47947  logbpw2m1  47955  fllog2  47956  blenpw2m1  47967  nnpw2blen  47968  dignn0flhalflem1  48003