Theorem 0lt1 8082

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 7916	. 2 |- 0 <RR 1
2		0re 7956	. . 3 |- 0 e. RR
3		1re 7955	. . 3 |- 1 e. RR
4		ltxrlt 8021	. . 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 2148   class class class wbr 4003   RRcr 7809   0cc0 7810   1c1 7811   <RR cltrr 7814   < clt 7990

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907  ax-0lt1 7916  ax-rnegex 7919

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-xp 4632  df-pnf 7992  df-mnf 7993  df-ltxr 7995

This theorem is referenced by:  ine0  8349  0le1  8436  inelr  8539  1ap0  8545  eqneg  8687  ltp1  8799  ltm1  8801  recgt0  8805  mulgt1  8818  reclt1  8851  recgt1  8852  recgt1i  8853  recp1lt1  8854  recreclt  8855  sup3exmid  8912  nnge1  8940  nngt0  8942  0nnn  8944  nnrecgt0  8955  0ne1  8984  2pos  9008  3pos  9011  4pos  9014  5pos  9017  6pos  9018  7pos  9019  8pos  9020  9pos  9021  neg1lt0  9025  halflt1  9134  nn0p1gt0  9203  elnnnn0c  9219  elnnz1  9274  recnz  9344  1rp  9655  divlt1lt  9722  divle1le  9723  ledivge1le  9724  nnledivrp  9764  fz10  10043  fzpreddisj  10068  elfz1b  10087  modqfrac  10334  expgt1  10555  ltexp2a  10569  leexp2a  10570  expnbnd  10640  expnlbnd  10641  expnlbnd2  10642  nn0ltexp2  10685  expcanlem  10690  expcan  10691  bcn1  10733  resqrexlem1arp  11009  mulcn2  11315  reccn2ap  11316  georeclim  11516  geoisumr  11521  cos1bnd  11762  sin01gt0  11764  sincos1sgn  11767  p1modz1  11796  nnoddm1d2  11909  dvdsnprmd  12119  divdenle  12191  mopnex  13936  reeff1olem  14123  cos02pilt1  14203  rplogcl  14231  cxplt  14267  cxple  14268  ltexp2  14291  apdiff  14716