ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0lt1 GIF version

Theorem 0lt1 8074
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
StepHypRef Expression
1 ax-0lt1 7908 . 2 0 < 1
2 0re 7948 . . 3 0 ∈ ℝ
3 1re 7947 . . 3 1 ∈ ℝ
4 ltxrlt 8013 . . 3 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 1 ↔ 0 < 1))
52, 3, 4mp2an 426 . 2 (0 < 1 ↔ 0 < 1)
61, 5mpbir 146 1 0 < 1
Colors of variables: wff set class
Syntax hints:  wb 105  wcel 2148   class class class wbr 4000  cr 7801  0cc0 7802  1c1 7803   < cltrr 7806   < clt 7982
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 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894  ax-1re 7896  ax-addrcl 7899  ax-0lt1 7908  ax-rnegex 7911
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 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-xp 4629  df-pnf 7984  df-mnf 7985  df-ltxr 7987
This theorem is referenced by:  ine0  8341  0le1  8428  inelr  8531  1ap0  8537  eqneg  8678  ltp1  8790  ltm1  8792  recgt0  8796  mulgt1  8809  reclt1  8842  recgt1  8843  recgt1i  8844  recp1lt1  8845  recreclt  8846  sup3exmid  8903  nnge1  8931  nngt0  8933  0nnn  8935  nnrecgt0  8946  0ne1  8975  2pos  8999  3pos  9002  4pos  9005  5pos  9008  6pos  9009  7pos  9010  8pos  9011  9pos  9012  neg1lt0  9016  halflt1  9125  nn0p1gt0  9194  elnnnn0c  9210  elnnz1  9265  recnz  9335  1rp  9644  divlt1lt  9711  divle1le  9712  ledivge1le  9713  nnledivrp  9753  fz10  10032  fzpreddisj  10057  elfz1b  10076  modqfrac  10323  expgt1  10544  ltexp2a  10558  leexp2a  10559  expnbnd  10629  expnlbnd  10630  expnlbnd2  10631  nn0ltexp2  10674  expcanlem  10679  expcan  10680  bcn1  10722  resqrexlem1arp  10998  mulcn2  11304  reccn2ap  11305  georeclim  11505  geoisumr  11510  cos1bnd  11751  sin01gt0  11753  sincos1sgn  11756  p1modz1  11785  nnoddm1d2  11898  dvdsnprmd  12108  divdenle  12180  mopnex  13672  reeff1olem  13859  cos02pilt1  13939  rplogcl  13967  cxplt  14003  cxple  14004  ltexp2  14027  apdiff  14452
  Copyright terms: Public domain W3C validator