Theorem 0lt1 8083

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 <ℝ 1
2		0re 7956	. . 3 ⊢ 0 ∈ ℝ
3		1re 7955	. . 3 ⊢ 1 ∈ ℝ
4		ltxrlt 8022	. . 3 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 1 ↔ 0 <ℝ 1))
5	2, 3, 4	mp2an 426	. 2 ⊢ (0 < 1 ↔ 0 <ℝ 1)
6	1, 5	mpbir 146	1 ⊢ 0 < 1

Syntax hints:   ↔ wb 105   ∈ wcel 2148   class class class wbr 4003  ℝcr 7809  0cc0 7810  1c1 7811   <_ℝ cltrr 7814   < clt 7991

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 7993  df-mnf 7994  df-ltxr 7996

This theorem is referenced by:  ine0  8350  0le1  8437  inelr  8540  1ap0  8546  eqneg  8688  ltp1  8800  ltm1  8802  recgt0  8806  mulgt1  8819  reclt1  8852  recgt1  8853  recgt1i  8854  recp1lt1  8855  recreclt  8856  sup3exmid  8913  nnge1  8941  nngt0  8943  0nnn  8945  nnrecgt0  8956  0ne1  8985  2pos  9009  3pos  9012  4pos  9015  5pos  9018  6pos  9019  7pos  9020  8pos  9021  9pos  9022  neg1lt0  9026  halflt1  9135  nn0p1gt0  9204  elnnnn0c  9220  elnnz1  9275  recnz  9345  1rp  9656  divlt1lt  9723  divle1le  9724  ledivge1le  9725  nnledivrp  9765  fz10  10045  fzpreddisj  10070  elfz1b  10089  modqfrac  10336  expgt1  10557  ltexp2a  10571  leexp2a  10572  expnbnd  10643  expnlbnd  10644  expnlbnd2  10645  nn0ltexp2  10688  expcanlem  10694  expcan  10695  bcn1  10737  resqrexlem1arp  11013  mulcn2  11319  reccn2ap  11320  georeclim  11520  geoisumr  11525  cos1bnd  11766  sin01gt0  11768  sincos1sgn  11771  p1modz1  11800  nnoddm1d2  11914  dvdsnprmd  12124  divdenle  12196  mopnex  13975  reeff1olem  14162  cos02pilt1  14242  rplogcl  14270  cxplt  14306  cxple  14307  ltexp2  14330  apdiff  14766