Theorem 0lt1 8305

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 8137	. 2 ⊢ 0 <ℝ 1
2		0re 8178	. . 3 ⊢ 0 ∈ ℝ
3		1re 8177	. . 3 ⊢ 1 ∈ ℝ
4		ltxrlt 8244	. . 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 2202   class class class wbr 4088  ℝcr 8030  0cc0 8031  1c1 8032   <_ℝ cltrr 8035   < clt 8213

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128  ax-0lt1 8137  ax-rnegex 8140

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-xp 4731  df-pnf 8215  df-mnf 8216  df-ltxr 8218

This theorem is referenced by:  ine0  8572  0le1  8660  inelr  8763  1ap0  8769  eqneg  8911  ltp1  9023  ltm1  9025  recgt0  9029  mulgt1  9042  reclt1  9075  recgt1  9076  recgt1i  9077  recp1lt1  9078  recreclt  9079  sup3exmid  9136  nnge1  9165  nngt0  9167  0nnn  9169  nnrecgt0  9180  0ne1  9209  2pos  9233  3pos  9236  4pos  9239  5pos  9242  6pos  9243  7pos  9244  8pos  9245  9pos  9246  neg1lt0  9250  halflt1  9360  nn0p1gt0  9430  elnnnn0c  9446  elnnz1  9501  recnz  9572  1rp  9891  divlt1lt  9958  divle1le  9959  ledivge1le  9960  nnledivrp  10000  fz10  10280  fzpreddisj  10305  elfz1b  10324  modqfrac  10598  expgt1  10838  ltexp2a  10852  leexp2a  10853  expnbnd  10924  expnlbnd  10925  expnlbnd2  10926  nn0ltexp2  10970  expcanlem  10976  expcan  10977  bcn1  11019  s2fv0g  11367  resqrexlem1arp  11565  mulcn2  11872  reccn2ap  11873  georeclim  12073  geoisumr  12078  cos1bnd  12319  sin01gt0  12322  sincos1sgn  12325  p1modz1  12354  nnoddm1d2  12470  dvdsnprmd  12696  divdenle  12768  plendxnocndx  13296  znidomb  14671  mopnex  15228  ivthdichlem  15374  reeff1olem  15494  cos02pilt1  15574  rplogcl  15602  cxplt  15639  cxple  15640  ltexp2  15664  mersenne  15720  perfectlem2  15723  apdiff  16652