Theorem 1lt2 12441

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 11236	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12147	. 2 ⊢ 1 < (1 + 1)
3		df-2 12331	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5136	1 ⊢ 1 < 2

This proof depends on syntax axioms:   class class class wbr 5107  (class class class)co 7417  1c1 11129   + caddc 11131   < clt 11271  2c2 12323

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-2 12331

This theorem is used by:  1lt3  12444  1lt4  12447  1lt6  12456  1lt7  12462  1lt8  12469  1lt9  12477  1ne2  12479  1le2  12480  halflt1  12489  nn0n0n1ge2b  12601  nn0ge2m1nn  12602  halfnz  12703  1lt10OLD  12886  fztpval  13645  ige2m2fzo  13788  faclbnd5  14366  hashgt23el  14493  hashfun  14506  hashge2el2dif  14549  tpf1ofv2  14567  wrdlenge2n0  14621  ccat2s1p2  14702  s3fv1  14967  pfx2  15022  wwlktovf  15033  sqrt2gt1lt2  15365  ege2le3  16182  ene1  16304  mod2eq1n2dvds  16443  bits0o  16526  bitsfzolem  16530  bitsfzo  16531  bitsfi  16533  2prm  16788  4nprm  16791  iserodd  16933  dec2dvds  17161  dec5nprm  17164  dec2nprm  17165  2expltfac  17190  5prm  17206  6nprm  17207  7prm  17208  8nprm  17209  10nprmOLD  17212  11prm  17213  13prm  17214  17prm  17215  19prm  17216  37prm  17219  83prm  17221  317prm  17224  631prm  17225  basendxltplusgndx  17377  rngstr  17389  lmodstr  17416  topgrpstr  17452  psgnunilem2  19628  isnzr2hash  20686  dyadss  25828  opnmbllem  25835  lhop1lem  26247  aaliou3lem8  26588  zetacvg  27259  lgamgulmlem4  27276  ppi1  27408  cht1  27409  chtrpcl  27419  ppiltx  27421  chtub  27456  chpval2  27462  mersenne  27471  perfectlem1  27473  perfectlem2  27474  bpos1  27527  bposlem1  27528  bposlem6  27533  bposlem7  27534  bposlem8  27535  lgseisenlem1  27619  2sqblem  27675  chebbnd1lem1  27713  chebbnd1lem3  27715  chebbnd1  27716  chtppilimlem1  27717  chtppilimlem2  27718  chtppilim  27719  chto1ub  27720  chebbnd2  27721  chto1lb  27722  mulog2sumlem2  27779  pntrmax  27808  pntrlog2bndlem2  27822  pntrlog2bndlem4  27824  pntpbnd1a  27829  pntibndlem3  27836  pntibnd  27837  pntlemb  27841  pntlemk  27850  pnt  27858  angmgmlem  29282  angmgmbas  29285  axlowdim  29426  lfgrnloop  29590  lfuhgr2  29614  lfuhgr1v0e  29722  nbusgrvtxm1  29847  cusgrsizeindb1  29918  lfgrwlkprop  30157  usgr2pthlem  30236  uspgrn2crct  30284  clwlkclwwlklem2fv2  30474  clwwlkext2edg  30534  eupth2lem3lem4  30719  ex-mod  30937  9p10ne21  30958  cshw1s2  33408  drngidlhash  33869  rtelextdg2lem  34244  fib1  34919  ballotlem2  35008  chtvalz  35145  hgt750lemd  35164  hgt750lem  35167  hgt750leme  35174  subfacp1lem1  35766  subfacp1lem5  35771  knoppndvlem12  37228  knoppndvlem18  37234  relowlpssretop  38126  tan2h  38374  opnmbllem0  38413  heiborlem7  38575  lcmineqlem22  42924  3lexlogpow5ineq2  42929  3lexlogpow5ineq4  42930  3lexlogpow5ineq3  42931  3lexlogpow2ineq1  42932  3lexlogpow2ineq2  42933  3lexlogpow5ineq5  42934  aks4d1lem1  42936  dvrelog2b  42940  dvrelogpow2b  42942  aks4d1p1p3  42943  aks4d1p1p2  42944  aks4d1p1p4  42945  aks4d1p1p6  42947  aks4d1p1p7  42948  aks4d1p1p5  42949  aks4d1p1  42950  aks4d1p2  42951  aks4d1p3  42952  aks4d1p5  42954  aks4d1p6  42955  aks4d1p7d1  42956  aks4d1p7  42957  aks4d1p8  42961  aks4d1p9  42962  aks6d1c3  42997  aks6d1c6lem4  43047  aks6d1c7lem2  43055  flt4lem7  43513  pellfundgt1  43732  stoweidlem13  46849  stoweidlem26  46862  wallispilem4  46904  wallispi  46906  wallispi2lem1  46907  wallispi2lem2  46908  wallispi2  46909  stirlinglem1  46910  dirkertrigeqlem1  46934  dirkercncflem1  46939  fouriersw  47067  etransclem23  47093  salexct2  47175  numtowerdt  47742  ceilhalfgt1  48229  ceil5half3  48242  difmodm1lt  48261  2timesltsqm1  48275  fmtnoge3  48441  fmtnof1  48446  fmtno4prm  48486  2pwp1prm  48500  127prm  48510  sfprmdvdsmersenne  48514  lighneallem2  48517  nprmdvdsfacm1lem4  48534  ppivalnn  48543  dfodd4  48583  perfectALTVlem1  48645  perfectALTVlem2  48646  nnsum4primesevenALTV  48725  gpgprismgrusgra  48982  cznnring  49185  pw2m1lepw2m1  49458  rege1logbzge0  49497  logbpw2m1  49505  fllog2  49506  blenpw2m1  49517  nnpw2blen  49518  dignn0flhalflem1  49553