Theorem 1lt2 12414

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 11209	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12120	. 2 ⊢ 1 < (1 + 1)
3		df-2 12304	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5139	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5110  (class class class)co 7412  1c1 11102   + caddc 11104   < clt 11244  2c2 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-2 12304

This theorem is referenced by:  1lt3  12417  1lt4  12420  1lt6  12429  1lt7  12435  1lt8  12442  1lt9  12450  1ne2  12452  1le2  12453  halflt1  12462  nn0n0n1ge2b  12574  nn0ge2m1nn  12575  halfnz  12675  1lt10OLD  12858  fztpval  13616  ige2m2fzo  13759  faclbnd5  14336  hashgt23el  14463  hashfun  14476  hashge2el2dif  14519  tpf1ofv2  14537  wrdlenge2n0  14591  ccat2s1p2  14670  s3fv1  14931  pfx2  14986  wwlktovf  14995  sqrt2gt1lt2  15327  ege2le3  16145  ene1  16267  mod2eq1n2dvds  16406  bits0o  16489  bitsfzolem  16493  bitsfzo  16494  bitsfi  16496  2prm  16751  4nprm  16754  iserodd  16896  dec2dvds  17124  dec5nprm  17127  dec2nprm  17128  2expltfac  17153  5prm  17169  6nprm  17170  7prm  17171  8nprm  17172  10nprmOLD  17175  11prm  17176  13prm  17177  17prm  17178  19prm  17179  37prm  17182  83prm  17184  317prm  17187  631prm  17188  basendxltplusgndx  17340  rngstr  17352  lmodstr  17379  topgrpstr  17415  psgnunilem2  19566  isnzr2hash  20604  dyadss  25734  opnmbllem  25741  lhop1lem  26153  aaliou3lem8  26489  zetacvg  27160  lgamgulmlem4  27177  ppi1  27309  cht1  27310  chtrpcl  27320  ppiltx  27322  chtub  27357  chpval2  27363  mersenne  27372  perfectlem1  27374  perfectlem2  27375  bpos1  27428  bposlem1  27429  bposlem6  27434  bposlem7  27435  bposlem8  27436  lgseisenlem1  27520  2sqblem  27576  chebbnd1lem1  27614  chebbnd1lem3  27616  chebbnd1  27617  chtppilimlem1  27618  chtppilimlem2  27619  chtppilim  27620  chto1ub  27621  chebbnd2  27622  chto1lb  27623  mulog2sumlem2  27680  pntrmax  27709  pntrlog2bndlem2  27723  pntrlog2bndlem4  27725  pntpbnd1a  27730  pntibndlem3  27737  pntibnd  27738  pntlemb  27742  pntlemk  27751  pnt  27759  axlowdim  29292  lfgrnloop  29456  lfuhgr1v0e  29585  nbusgrvtxm1  29710  cusgrsizeindb1  29781  lfgrwlkprop  30016  usgr2pthlem  30093  uspgrn2crct  30138  clwlkclwwlklem2fv2  30328  clwwlkext2edg  30388  eupth2lem3lem4  30563  ex-mod  30781  9p10ne21  30802  cshw1s2  33261  drngidlhash  33722  rtelextdg2lem  34097  fib1  34771  ballotlem2  34860  chtvalz  34997  hgt750lemd  35016  hgt750lem  35019  hgt750leme  35026  lfuhgr2  35592  subfacp1lem1  35652  subfacp1lem5  35657  knoppndvlem12  37093  knoppndvlem18  37099  relowlpssretop  37991  tan2h  38244  opnmbllem0  38288  heiborlem7  38449  lcmineqlem22  42798  3lexlogpow5ineq2  42803  3lexlogpow5ineq4  42804  3lexlogpow5ineq3  42805  3lexlogpow2ineq1  42806  3lexlogpow2ineq2  42807  3lexlogpow5ineq5  42808  aks4d1lem1  42810  dvrelog2b  42814  dvrelogpow2b  42816  aks4d1p1p3  42817  aks4d1p1p2  42818  aks4d1p1p4  42819  aks4d1p1p6  42821  aks4d1p1p7  42822  aks4d1p1p5  42823  aks4d1p1  42824  aks4d1p2  42825  aks4d1p3  42826  aks4d1p5  42828  aks4d1p6  42829  aks4d1p7d1  42830  aks4d1p7  42831  aks4d1p8  42835  aks4d1p9  42836  aks6d1c3  42871  aks6d1c6lem4  42921  aks6d1c7lem2  42929  flt4lem7  43374  pellfundgt1  43593  stoweidlem13  46710  stoweidlem26  46723  wallispilem4  46765  wallispi  46767  wallispi2lem1  46768  wallispi2lem2  46769  wallispi2  46770  stirlinglem1  46771  dirkertrigeqlem1  46795  dirkercncflem1  46800  fouriersw  46928  etransclem23  46954  salexct2  47036  nthrucw  47590  ceilhalfgt1  48053  ceil5half3  48066  difmodm1lt  48085  2timesltsqm1  48099  fmtnoge3  48265  fmtnof1  48270  fmtno4prm  48310  2pwp1prm  48324  127prm  48334  sfprmdvdsmersenne  48338  lighneallem2  48341  nprmdvdsfacm1lem4  48358  ppivalnn  48367  dfodd4  48407  perfectALTVlem1  48469  perfectALTVlem2  48470  nnsum4primesevenALTV  48549  gpgprismgrusgra  48806  cznnring  49010  pw2m1lepw2m1  49283  rege1logbzge0  49322  logbpw2m1  49330  fllog2  49331  blenpw2m1  49342  nnpw2blen  49343  dignn0flhalflem1  49378