Theorem 0lt1 8146

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 7978	. 2 ⊢ 0 <ℝ 1
2		0re 8019	. . 3 ⊢ 0 ∈ ℝ
3		1re 8018	. . 3 ⊢ 1 ∈ ℝ
4		ltxrlt 8085	. . 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 2164   class class class wbr 4029  ℝcr 7871  0cc0 7872  1c1 7873   <_ℝ cltrr 7876   < clt 8054

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969  ax-0lt1 7978  ax-rnegex 7981

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-xp 4665  df-pnf 8056  df-mnf 8057  df-ltxr 8059

This theorem is referenced by:  ine0  8413  0le1  8500  inelr  8603  1ap0  8609  eqneg  8751  ltp1  8863  ltm1  8865  recgt0  8869  mulgt1  8882  reclt1  8915  recgt1  8916  recgt1i  8917  recp1lt1  8918  recreclt  8919  sup3exmid  8976  nnge1  9005  nngt0  9007  0nnn  9009  nnrecgt0  9020  0ne1  9049  2pos  9073  3pos  9076  4pos  9079  5pos  9082  6pos  9083  7pos  9084  8pos  9085  9pos  9086  neg1lt0  9090  halflt1  9199  nn0p1gt0  9269  elnnnn0c  9285  elnnz1  9340  recnz  9410  1rp  9723  divlt1lt  9790  divle1le  9791  ledivge1le  9792  nnledivrp  9832  fz10  10112  fzpreddisj  10137  elfz1b  10156  modqfrac  10408  expgt1  10648  ltexp2a  10662  leexp2a  10663  expnbnd  10734  expnlbnd  10735  expnlbnd2  10736  nn0ltexp2  10780  expcanlem  10786  expcan  10787  bcn1  10829  resqrexlem1arp  11149  mulcn2  11455  reccn2ap  11456  georeclim  11656  geoisumr  11661  cos1bnd  11902  sin01gt0  11905  sincos1sgn  11908  p1modz1  11937  nnoddm1d2  12051  dvdsnprmd  12263  divdenle  12335  znidomb  14146  mopnex  14673  ivthdichlem  14805  reeff1olem  14906  cos02pilt1  14986  rplogcl  15014  cxplt  15050  cxple  15051  ltexp2  15074  apdiff  15538