Theorem 0lt1 8016

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 7850	. 2 ⊢ 0 <ℝ 1
2		0re 7890	. . 3 ⊢ 0 ∈ ℝ
3		1re 7889	. . 3 ⊢ 1 ∈ ℝ
4		ltxrlt 7955	. . 3 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 1 ↔ 0 <ℝ 1))
5	2, 3, 4	mp2an 423	. 2 ⊢ (0 < 1 ↔ 0 <ℝ 1)
6	1, 5	mpbir 145	1 ⊢ 0 < 1

Syntax hints:   ↔ wb 104   ∈ wcel 2135   class class class wbr 3976  ℝcr 7743  0cc0 7744  1c1 7745   <_ℝ cltrr 7748   < clt 7924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-setind 4508  ax-cnex 7835  ax-resscn 7836  ax-1re 7838  ax-addrcl 7841  ax-0lt1 7850  ax-rnegex 7853

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-rab 2451  df-v 2723  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-xp 4604  df-pnf 7926  df-mnf 7927  df-ltxr 7929

This theorem is referenced by:  ine0  8283  0le1  8370  inelr  8473  1ap0  8479  eqneg  8619  ltp1  8730  ltm1  8732  recgt0  8736  mulgt1  8749  reclt1  8782  recgt1  8783  recgt1i  8784  recp1lt1  8785  recreclt  8786  sup3exmid  8843  nnge1  8871  nngt0  8873  0nnn  8875  nnrecgt0  8886  0ne1  8915  2pos  8939  3pos  8942  4pos  8945  5pos  8948  6pos  8949  7pos  8950  8pos  8951  9pos  8952  neg1lt0  8956  halflt1  9065  nn0p1gt0  9134  elnnnn0c  9150  elnnz1  9205  recnz  9275  1rp  9584  divlt1lt  9651  divle1le  9652  ledivge1le  9653  nnledivrp  9693  fz10  9971  fzpreddisj  9996  elfz1b  10015  modqfrac  10262  expgt1  10483  ltexp2a  10497  leexp2a  10498  expnbnd  10567  expnlbnd  10568  expnlbnd2  10569  nn0ltexp2  10612  expcanlem  10617  expcan  10618  bcn1  10660  resqrexlem1arp  10933  mulcn2  11239  reccn2ap  11240  georeclim  11440  geoisumr  11445  cos1bnd  11686  sin01gt0  11688  sincos1sgn  11691  p1modz1  11720  nnoddm1d2  11832  dvdsnprmd  12036  divdenle  12106  mopnex  13046  reeff1olem  13233  cos02pilt1  13313  rplogcl  13341  cxplt  13377  cxple  13378  ltexp2  13401  apdiff  13761