Theorem 0lt1 8400

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 8233	. 2 ⊢ 0 <ℝ 1
2		0re 8274	. . 3 ⊢ 0 ∈ ℝ
3		1re 8273	. . 3 ⊢ 1 ∈ ℝ
4		ltxrlt 8339	. . 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 2203   class class class wbr 4109  ℝcr 8126  0cc0 8127  1c1 8128   <_ℝ cltrr 8131   < clt 8308

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224  ax-0lt1 8233  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-xp 4755  df-pnf 8310  df-mnf 8311  df-ltxr 8313

This theorem is referenced by:  ine0  8667  0le1  8755  inelr  8858  1ap0  8864  eqneg  9006  ltp1  9118  ltm1  9120  recgt0  9124  mulgt1  9137  reclt1  9170  recgt1  9171  recgt1i  9172  recp1lt1  9173  recreclt  9174  sup3exmid  9231  nnge1  9260  nngt0  9262  0nnn  9264  nnrecgt0  9275  0ne1  9304  2pos  9328  3pos  9331  4pos  9334  5pos  9337  6pos  9338  7pos  9339  8pos  9340  9pos  9341  neg1lt0  9345  halflt1  9455  nn0p1gt0  9525  elnnnn0c  9541  elnnz1  9600  recnz  9671  1rp  9990  divlt1lt  10057  divle1le  10058  ledivge1le  10059  nnledivrp  10099  fz10  10380  fzpreddisj  10405  elfz1b  10424  modqfrac  10699  expgt1  10939  ltexp2a  10953  leexp2a  10954  expnbnd  11025  expnlbnd  11026  expnlbnd2  11027  nn0ltexp2  11071  expcanlem  11077  expcan  11078  bcn1  11120  ssenneg  11204  s2fv0g  11479  resqrexlem1arp  11690  mulcn2  11997  reccn2ap  11998  georeclim  12199  geoisumr  12204  cos1bnd  12445  sin01gt0  12448  sincos1sgn  12451  p1modz1  12480  nnoddm1d2  12596  dvdsnprmd  12822  divdenle  12894  plendxnocndx  13427  znidomb  14806  mopnex  15370  ivthdichlem  15516  reeff1olem  15636  cos02pilt1  15716  rplogcl  15744  cxplt  15781  cxple  15782  ltexp2  15806  pellexlem2  15846  mersenne  15865  perfectlem2  15868  apdiff  16832