Theorem 1lt2 9485

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 8331	. . 3 |- 1 e. RR
2	1	ltp1i 9243	. 2 |- 1 < ( 1 + 1 )
3		df-2 9372	. 2 |- 2 = ( 1 + 1 )
4	2, 3	breqtrri 4158	1 |- 1 < 2

This proof depends on syntax axioms:   class class class wbr 4131  (class class class)co 6088   1c1 8186   + caddc 8188   < clt 8366   2c2 9364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-addcom 8285  ax-addass 8287  ax-i2m1 8290  ax-0lt1 8291  ax-0id 8293  ax-rnegex 8294  ax-pre-ltadd 8301

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-xp 4782  df-iota 5340  df-fv 5388  df-ov 6091  df-pnf 8368  df-mnf 8369  df-ltxr 8371  df-2 9372

This theorem is used by:  1lt3  9487  1lt4  9490  1lt6  9499  1lt7  9505  1lt8  9512  1lt9  9520  1ne2  9522  1ap2  9523  1le2  9524  halflt1  9533  nn0ge2m1nn  9636  nn0n0n1ge2b  9734  halfnz  9752  1lt10  9930  fztpval  10506  ige2m2fzo  10632  wrdlenge2n0  11361  s3fv1g  11585  sqrt2gt1lt2  11836  ege2le3  12462  cos12dec  12559  ene1  12576  eap1  12577  n2dvds1  12703  bits0o  12741  bitsfzolem  12745  bitsfzo  12746  bitsfi  12748  2prm  12929  3prm  12930  4nprm  12931  isprm5  12945  dec2dvds  13218  dec5nprm  13221  dec2nprm  13222  2expltfac  13247  5prm  13251  6nprm  13252  7prm  13253  8nprm  13254  11prm  13257  13prm  13258  17prm  13259  19prm  13260  37prm  13263  83prm  13265  317prm  13268  631prm  13269  ballotfilem2  13285  basendxltplusgndx  13525  grpstrg  13538  grpbaseg  13539  grpplusgg  13540  rngstrg  13547  lmodstrd  13576  topgrpstrd  13608  reeff1o  16016  cosz12  16024  logdivlt  16141  2logb9irrALT  16227  sqrt2cxp2logb9e3  16228  ppi1  16287  cht1  16288  chtqrpcl  16296  chtqub  16313  mersenne  16314  perfectlem1  16316  perfectlem2  16317  bpos1  16327  bposlem1  16328  bposlem6  16333  bposlem7  16334  bposlem8  16335  lgseisenlem1  16411  clwwlkext2edg  16885  eupth2lem3lem4fi  16936