Theorem 0lt1 8269

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 8101	. 2 ⊢ 0 <ℝ 1
2		0re 8142	. . 3 ⊢ 0 ∈ ℝ
3		1re 8141	. . 3 ⊢ 1 ∈ ℝ
4		ltxrlt 8208	. . 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 2200   class class class wbr 4082  ℝcr 7994  0cc0 7995  1c1 7996   <_ℝ cltrr 7999   < clt 8177

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092  ax-0lt1 8101  ax-rnegex 8104

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-xp 4724  df-pnf 8179  df-mnf 8180  df-ltxr 8182

This theorem is referenced by:  ine0  8536  0le1  8624  inelr  8727  1ap0  8733  eqneg  8875  ltp1  8987  ltm1  8989  recgt0  8993  mulgt1  9006  reclt1  9039  recgt1  9040  recgt1i  9041  recp1lt1  9042  recreclt  9043  sup3exmid  9100  nnge1  9129  nngt0  9131  0nnn  9133  nnrecgt0  9144  0ne1  9173  2pos  9197  3pos  9200  4pos  9203  5pos  9206  6pos  9207  7pos  9208  8pos  9209  9pos  9210  neg1lt0  9214  halflt1  9324  nn0p1gt0  9394  elnnnn0c  9410  elnnz1  9465  recnz  9536  1rp  9849  divlt1lt  9916  divle1le  9917  ledivge1le  9918  nnledivrp  9958  fz10  10238  fzpreddisj  10263  elfz1b  10282  modqfrac  10554  expgt1  10794  ltexp2a  10808  leexp2a  10809  expnbnd  10880  expnlbnd  10881  expnlbnd2  10882  nn0ltexp2  10926  expcanlem  10932  expcan  10933  bcn1  10975  s2fv0g  11314  resqrexlem1arp  11511  mulcn2  11818  reccn2ap  11819  georeclim  12019  geoisumr  12024  cos1bnd  12265  sin01gt0  12268  sincos1sgn  12271  p1modz1  12300  nnoddm1d2  12416  dvdsnprmd  12642  divdenle  12714  plendxnocndx  13242  znidomb  14616  mopnex  15173  ivthdichlem  15319  reeff1olem  15439  cos02pilt1  15519  rplogcl  15547  cxplt  15584  cxple  15585  ltexp2  15609  mersenne  15665  perfectlem2  15668  apdiff  16375