Theorem 1lt2 9268

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 8133	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 9040	. 2 ⊢ 1 < (1 + 1)
3		df-2 9157	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 4109	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 4082  (class class class)co 5994  1c1 7988   + caddc 7990   < clt 8169  2c2 9149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-setind 4626  ax-cnex 8078  ax-resscn 8079  ax-1cn 8080  ax-1re 8081  ax-icn 8082  ax-addcl 8083  ax-addrcl 8084  ax-mulcl 8085  ax-addcom 8087  ax-addass 8089  ax-i2m1 8092  ax-0lt1 8093  ax-0id 8095  ax-rnegex 8096  ax-pre-ltadd 8103

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-xp 4722  df-iota 5274  df-fv 5322  df-ov 5997  df-pnf 8171  df-mnf 8172  df-ltxr 8174  df-2 9157

This theorem is referenced by:  1lt3  9270  1lt4  9273  1lt6  9282  1lt7  9288  1lt8  9295  1lt9  9303  1ne2  9305  1ap2  9306  1le2  9307  halflt1  9316  nn0ge2m1nn  9417  nn0n0n1ge2b  9514  halfnz  9531  1lt10  9704  fztpval  10267  ige2m2fzo  10391  wrdlenge2n0  11093  s3fv1g  11310  sqrt2gt1lt2  11546  ege2le3  12168  cos12dec  12265  ene1  12282  eap1  12283  n2dvds1  12409  bits0o  12447  bitsfzolem  12451  bitsfzo  12452  bitsfi  12454  2prm  12635  3prm  12636  4nprm  12637  isprm5  12650  dec2dvds  12920  dec5nprm  12923  dec2nprm  12924  2expltfac  12948  basendxltplusgndx  13132  grpstrg  13145  grpbaseg  13146  grpplusgg  13147  rngstrg  13154  lmodstrd  13183  topgrpstrd  13215  reeff1o  15432  cosz12  15439  2logb9irrALT  15633  sqrt2cxp2logb9e3  15634  mersenne  15656  perfectlem1  15658  perfectlem2  15659  lgseisenlem1  15734