Theorem 1lt2 12311

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 11132	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12046	. 2 ⊢ 1 < (1 + 1)
3		df-2 12208	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5125	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5098  (class class class)co 7358  1c1 11027   + caddc 11029   < clt 11166  2c2 12200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-2 12208

This theorem is referenced by:  1lt3  12313  1lt4  12316  1lt6  12325  1lt7  12331  1lt8  12338  1lt9  12346  1ne2  12348  1le2  12349  halflt1  12358  nn0n0n1ge2b  12470  nn0ge2m1nn  12471  halfnz  12570  1lt10  12746  fztpval  13502  ige2m2fzo  13644  faclbnd5  14221  hashgt23el  14347  hashfun  14360  hashge2el2dif  14403  tpf1ofv2  14421  wrdlenge2n0  14475  ccat2s1p2  14554  s3fv1  14815  pfx2  14870  wwlktovf  14879  sqrt2gt1lt2  15197  ege2le3  16013  ene1  16135  mod2eq1n2dvds  16274  bits0o  16357  bitsfzolem  16361  bitsfzo  16362  bitsfi  16364  2prm  16619  4nprm  16622  iserodd  16763  dec2dvds  16991  dec5nprm  16994  dec2nprm  16995  2expltfac  17020  5prm  17036  6nprm  17037  7prm  17038  8nprm  17039  10nprm  17041  11prm  17042  13prm  17043  17prm  17044  19prm  17045  37prm  17048  83prm  17050  317prm  17053  631prm  17054  basendxltplusgndx  17206  rngstr  17218  lmodstr  17245  topgrpstr  17281  psgnunilem2  19424  isnzr2hash  20452  dyadss  25551  opnmbllem  25558  lhop1lem  25974  aaliou3lem8  26309  zetacvg  26981  lgamgulmlem4  26998  ppi1  27130  cht1  27131  chtrpcl  27141  ppiltx  27143  chtub  27179  chpval2  27185  mersenne  27194  perfectlem1  27196  perfectlem2  27197  bpos1  27250  bposlem1  27251  bposlem6  27256  bposlem7  27257  bposlem8  27258  lgseisenlem1  27342  2sqblem  27398  chebbnd1lem1  27436  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  chtppilimlem2  27441  chtppilim  27442  chto1ub  27443  chebbnd2  27444  chto1lb  27445  mulog2sumlem2  27502  pntrmax  27531  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  pntpbnd1a  27552  pntibndlem3  27559  pntibnd  27560  pntlemb  27564  pntlemk  27573  pnt  27581  axlowdim  29034  lfgrnloop  29198  lfuhgr1v0e  29327  nbusgrvtxm1  29452  cusgrsizeindb1  29524  lfgrwlkprop  29759  usgr2pthlem  29836  uspgrn2crct  29881  clwlkclwwlklem2fv2  30071  clwwlkext2edg  30131  eupth2lem3lem4  30306  ex-mod  30524  9p10ne21  30545  cshw1s2  33042  drngidlhash  33515  rtelextdg2lem  33883  fib1  34557  ballotlem2  34646  chtvalz  34786  hgt750lemd  34805  hgt750lem  34808  hgt750leme  34815  lfuhgr2  35313  subfacp1lem1  35373  subfacp1lem5  35378  knoppndvlem12  36723  knoppndvlem18  36729  relowlpssretop  37569  tan2h  37813  opnmbllem0  37857  heiborlem7  38018  lcmineqlem22  42304  3lexlogpow5ineq2  42309  3lexlogpow5ineq4  42310  3lexlogpow5ineq3  42311  3lexlogpow2ineq1  42312  3lexlogpow2ineq2  42313  3lexlogpow5ineq5  42314  aks4d1lem1  42316  dvrelog2b  42320  dvrelogpow2b  42322  aks4d1p1p3  42323  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p5  42334  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  aks4d1p9  42342  aks6d1c3  42377  aks6d1c6lem4  42427  aks6d1c7lem2  42435  flt4lem7  42902  pellfundgt1  43125  stoweidlem13  46257  stoweidlem26  46270  wallispilem4  46312  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  wallispi2  46317  stirlinglem1  46318  dirkertrigeqlem1  46342  dirkercncflem1  46347  fouriersw  46475  etransclem23  46501  salexct2  46583  nthrucw  47130  ceilhalfgt1  47575  ceil5half3  47586  difmodm1lt  47605  fmtnoge3  47776  fmtnof1  47781  fmtno4prm  47821  2pwp1prm  47835  127prm  47845  sfprmdvdsmersenne  47849  lighneallem2  47852  dfodd4  47905  perfectALTVlem1  47967  perfectALTVlem2  47968  nnsum4primesevenALTV  48047  gpgprismgrusgra  48304  cznnring  48508  pw2m1lepw2m1  48766  rege1logbzge0  48805  logbpw2m1  48813  fllog2  48814  blenpw2m1  48825  nnpw2blen  48826  dignn0flhalflem1  48861