Theorem 0lt1 8402

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 8235	. 2 |- 0 <RR 1
2		0re 8276	. . 3 |- 0 e. RR
3		1re 8275	. . 3 |- 1 e. RR
4		ltxrlt 8341	. . 3 |- ( ( 0 e. RR /\ 1 e. RR ) -> ( 0 < 1 <-> 0 <RR 1 ) )
5	2, 3, 4	mp2an 426	. 2 |- ( 0 < 1 <-> 0 <RR 1 )
6	1, 5	mpbir 146	1 |- 0 < 1

Syntax hints:   <-> wb 105   e. wcel 2205   class class class wbr 4111   RRcr 8128   0cc0 8129   1c1 8130   <RR cltrr 8133   < clt 8310

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-cnex 8220  ax-resscn 8221  ax-1re 8223  ax-addrcl 8226  ax-0lt1 8235  ax-rnegex 8238

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-xp 4757  df-pnf 8312  df-mnf 8313  df-ltxr 8315

This theorem is referenced by:  ine0  8669  0le1  8757  inelr  8860  1ap0  8866  eqneg  9008  ltp1  9120  ltm1  9122  recgt0  9126  mulgt1  9139  reclt1  9172  recgt1  9173  recgt1i  9174  recp1lt1  9175  recreclt  9176  sup3exmid  9233  nnge1  9262  nngt0  9264  0nnn  9266  nnrecgt0  9277  0ne1  9306  2pos  9330  3pos  9333  4pos  9336  5pos  9339  6pos  9340  7pos  9341  8pos  9342  9pos  9343  neg1lt0  9347  halflt1  9457  nn0p1gt0  9527  elnnnn0c  9543  elnnz1  9602  recnz  9674  1rp  9993  divlt1lt  10060  divle1le  10061  ledivge1le  10062  nnledivrp  10102  fz10  10383  fzpreddisj  10409  elfz1b  10428  modqfrac  10703  expgt1  10943  ltexp2a  10957  leexp2a  10958  expnbnd  11029  expnlbnd  11030  expnlbnd2  11031  nn0ltexp2  11075  expcanlem  11081  expcan  11082  bcn1  11124  ssenneg  11208  s2fv0g  11483  resqrexlem1arp  11694  mulcn2  12001  reccn2ap  12002  georeclim  12203  geoisumr  12208  cos1bnd  12449  sin01gt0  12452  sincos1sgn  12455  p1modz1  12484  nnoddm1d2  12600  dvdsnprmd  12826  divdenle  12898  plendxnocndx  13444  znidomb  14823  mopnex  15387  ivthdichlem  15533  reeff1olem  15653  cos02pilt1  15733  rplogcl  15761  cxplt  15798  cxple  15799  ltexp2  15823  pellexlem2  15863  mersenne  15882  perfectlem2  15885  apdiff  16849