Theorem 0lt1 7996

Description: 0 is less than 1. Theorem I.21 of [Apostol] p. 20. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 17-Jan-1997.)

Assertion

Ref	Expression
0lt1	|- 0 < 1

Proof of Theorem 0lt1

Step	Hyp	Ref	Expression
1		ax-0lt1 7832	. 2 |- 0 <RR 1
2		0re 7872	. . 3 |- 0 e. RR
3		1re 7871	. . 3 |- 1 e. RR
4		ltxrlt 7937	. . 3 |- ( ( 0 e. RR /\ 1 e. RR ) -> ( 0 < 1 <-> 0 <RR 1 ) )
5	2, 3, 4	mp2an 423	. 2 |- ( 0 < 1 <-> 0 <RR 1 )
6	1, 5	mpbir 145	1 |- 0 < 1

Syntax hints:   <-> wb 104   e. wcel 2128   class class class wbr 3965   RRcr 7725   0cc0 7726   1c1 7727   <RR cltrr 7730   < clt 7906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495  ax-cnex 7817  ax-resscn 7818  ax-1re 7820  ax-addrcl 7823  ax-0lt1 7832  ax-rnegex 7835

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-xp 4591  df-pnf 7908  df-mnf 7909  df-ltxr 7911

This theorem is referenced by:  ine0  8263  0le1  8350  inelr  8453  1ap0  8459  eqneg  8599  ltp1  8709  ltm1  8711  recgt0  8715  mulgt1  8728  reclt1  8761  recgt1  8762  recgt1i  8763  recp1lt1  8764  recreclt  8765  sup3exmid  8822  nnge1  8850  nngt0  8852  0nnn  8854  nnrecgt0  8865  0ne1  8894  2pos  8918  3pos  8921  4pos  8924  5pos  8927  6pos  8928  7pos  8929  8pos  8930  9pos  8931  neg1lt0  8935  halflt1  9044  nn0p1gt0  9113  elnnnn0c  9129  elnnz1  9184  recnz  9251  1rp  9557  divlt1lt  9624  divle1le  9625  ledivge1le  9626  nnledivrp  9666  fz10  9941  fzpreddisj  9966  elfz1b  9985  modqfrac  10229  expgt1  10450  ltexp2a  10464  leexp2a  10465  expnbnd  10534  expnlbnd  10535  expnlbnd2  10536  expcanlem  10582  expcan  10583  bcn1  10625  resqrexlem1arp  10898  mulcn2  11202  reccn2ap  11203  georeclim  11403  geoisumr  11408  cos1bnd  11649  sin01gt0  11651  sincos1sgn  11654  p1modz1  11683  nnoddm1d2  11793  dvdsnprmd  11993  divdenle  12062  mopnex  12876  reeff1olem  13063  cos02pilt1  13143  rplogcl  13171  cxplt  13207  cxple  13208  apdiff  13590