Theorem 0lt1 7806

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 7645	. 2 |- 0 <RR 1
2		0re 7684	. . 3 |- 0 e. RR
3		1re 7683	. . 3 |- 1 e. RR
4		ltxrlt 7748	. . 3 |- ( ( 0 e. RR /\ 1 e. RR ) -> ( 0 < 1 <-> 0 <RR 1 ) )
5	2, 3, 4	mp2an 420	. 2 |- ( 0 < 1 <-> 0 <RR 1 )
6	1, 5	mpbir 145	1 |- 0 < 1

Syntax hints:   <-> wb 104   e. wcel 1461   class class class wbr 3893   RRcr 7540   0cc0 7541   1c1 7542   <RR cltrr 7545   < clt 7718

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-cnex 7630  ax-resscn 7631  ax-1re 7633  ax-addrcl 7636  ax-0lt1 7645  ax-rnegex 7648

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-rab 2397  df-v 2657  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-xp 4503  df-pnf 7720  df-mnf 7721  df-ltxr 7723

This theorem is referenced by:  ine0  8069  0le1  8156  inelr  8258  1ap0  8264  eqneg  8399  ltp1  8506  ltm1  8508  recgt0  8512  mulgt1  8525  reclt1  8558  recgt1  8559  recgt1i  8560  recp1lt1  8561  recreclt  8562  sup3exmid  8619  nnge1  8647  nngt0  8649  0nnn  8651  nnrecgt0  8662  0ne1  8691  2pos  8715  3pos  8718  4pos  8721  5pos  8724  6pos  8725  7pos  8726  8pos  8727  9pos  8728  neg1lt0  8732  halflt1  8835  nn0p1gt0  8904  elnnnn0c  8920  elnnz1  8975  recnz  9042  1rp  9341  divlt1lt  9404  divle1le  9405  ledivge1le  9406  nnledivrp  9440  fz10  9713  fzpreddisj  9738  elfz1b  9757  modqfrac  9997  expgt1  10218  ltexp2a  10232  leexp2a  10233  expnbnd  10302  expnlbnd  10303  expnlbnd2  10304  expcanlem  10349  expcan  10350  bcn1  10391  resqrexlem1arp  10663  mulcn2  10967  reccn2ap  10968  georeclim  11168  geoisumr  11173  cos1bnd  11311  sin01gt0  11313  sincos1sgn  11316  nnoddm1d2  11449  dvdsnprmd  11646  divdenle  11714  mopnex  12488