Theorem 1lt2 12338

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 11135	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12051	. 2 ⊢ 1 < (1 + 1)
3		df-2 12235	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5113	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5086  (class class class)co 7360  1c1 11030   + caddc 11032   < clt 11170  2c2 12227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-2 12235

This theorem is referenced by:  1lt3  12340  1lt4  12343  1lt6  12352  1lt7  12358  1lt8  12365  1lt9  12373  1ne2  12375  1le2  12376  halflt1  12385  nn0n0n1ge2b  12497  nn0ge2m1nn  12498  halfnz  12598  1lt10  12774  fztpval  13531  ige2m2fzo  13674  faclbnd5  14251  hashgt23el  14377  hashfun  14390  hashge2el2dif  14433  tpf1ofv2  14451  wrdlenge2n0  14505  ccat2s1p2  14584  s3fv1  14845  pfx2  14900  wwlktovf  14909  sqrt2gt1lt2  15227  ege2le3  16046  ene1  16168  mod2eq1n2dvds  16307  bits0o  16390  bitsfzolem  16394  bitsfzo  16395  bitsfi  16397  2prm  16652  4nprm  16655  iserodd  16797  dec2dvds  17025  dec5nprm  17028  dec2nprm  17029  2expltfac  17054  5prm  17070  6nprm  17071  7prm  17072  8nprm  17073  10nprm  17075  11prm  17076  13prm  17077  17prm  17078  19prm  17079  37prm  17082  83prm  17084  317prm  17087  631prm  17088  basendxltplusgndx  17240  rngstr  17252  lmodstr  17279  topgrpstr  17315  psgnunilem2  19461  isnzr2hash  20487  dyadss  25571  opnmbllem  25578  lhop1lem  25990  aaliou3lem8  26322  zetacvg  26992  lgamgulmlem4  27009  ppi1  27141  cht1  27142  chtrpcl  27152  ppiltx  27154  chtub  27189  chpval2  27195  mersenne  27204  perfectlem1  27206  perfectlem2  27207  bpos1  27260  bposlem1  27261  bposlem6  27266  bposlem7  27267  bposlem8  27268  lgseisenlem1  27352  2sqblem  27408  chebbnd1lem1  27446  chebbnd1lem3  27448  chebbnd1  27449  chtppilimlem1  27450  chtppilimlem2  27451  chtppilim  27452  chto1ub  27453  chebbnd2  27454  chto1lb  27455  mulog2sumlem2  27512  pntrmax  27541  pntrlog2bndlem2  27555  pntrlog2bndlem4  27557  pntpbnd1a  27562  pntibndlem3  27569  pntibnd  27570  pntlemb  27574  pntlemk  27583  pnt  27591  axlowdim  29044  lfgrnloop  29208  lfuhgr1v0e  29337  nbusgrvtxm1  29462  cusgrsizeindb1  29534  lfgrwlkprop  29769  usgr2pthlem  29846  uspgrn2crct  29891  clwlkclwwlklem2fv2  30081  clwwlkext2edg  30141  eupth2lem3lem4  30316  ex-mod  30534  9p10ne21  30555  cshw1s2  33035  drngidlhash  33509  rtelextdg2lem  33886  fib1  34560  ballotlem2  34649  chtvalz  34789  hgt750lemd  34808  hgt750lem  34811  hgt750leme  34818  lfuhgr2  35317  subfacp1lem1  35377  subfacp1lem5  35382  knoppndvlem12  36799  knoppndvlem18  36805  relowlpssretop  37694  tan2h  37947  opnmbllem0  37991  heiborlem7  38152  lcmineqlem22  42503  3lexlogpow5ineq2  42508  3lexlogpow5ineq4  42509  3lexlogpow5ineq3  42510  3lexlogpow2ineq1  42511  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1lem1  42515  dvrelog2b  42519  dvrelogpow2b  42521  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  aks4d1p9  42541  aks6d1c3  42576  aks6d1c6lem4  42626  aks6d1c7lem2  42634  flt4lem7  43106  pellfundgt1  43329  stoweidlem13  46459  stoweidlem26  46472  wallispilem4  46514  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  wallispi2  46519  stirlinglem1  46520  dirkertrigeqlem1  46544  dirkercncflem1  46549  fouriersw  46677  etransclem23  46703  salexct2  46785  nthrucw  47332  ceilhalfgt1  47793  ceil5half3  47806  difmodm1lt  47825  2timesltsqm1  47839  fmtnoge3  48005  fmtnof1  48010  fmtno4prm  48050  2pwp1prm  48064  127prm  48074  sfprmdvdsmersenne  48078  lighneallem2  48081  nprmdvdsfacm1lem4  48098  ppivalnn  48107  dfodd4  48147  perfectALTVlem1  48209  perfectALTVlem2  48210  nnsum4primesevenALTV  48289  gpgprismgrusgra  48546  cznnring  48750  pw2m1lepw2m1  49008  rege1logbzge0  49047  logbpw2m1  49055  fllog2  49056  blenpw2m1  49067  nnpw2blen  49068  dignn0flhalflem1  49103