Theorem 0lt1 11812

Description: 0 is less than 1. Theorem I.21 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.)

Assertion

Ref	Expression
0lt1	⊢ 0 < 1

Proof of Theorem 0lt1

Step	Hyp	Ref	Expression
1		1re 11290	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11253	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11810	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 691	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11294	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5191	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2108   ≠ wne 2946   class class class wbr 5166  (class class class)co 7448  ℝcr 11183  0cc0 11184  1c1 11185   · cmul 11189   < clt 11324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523

This theorem is referenced by:  0le1  11813  eqneg  12014  elimgt0  12132  ltp1  12134  ltm1  12136  recgt0  12140  mulgt1OLD  12153  mulgt1  12156  reclt1  12190  recgt1  12191  recgt1i  12192  recp1lt1  12193  recreclt  12194  recgt0ii  12201  inelr  12283  nnge1  12321  nngt0  12324  0nnnALT  12330  nnrecgt0  12336  2pos  12396  3pos  12398  4pos  12400  5pos  12402  6pos  12403  7pos  12404  8pos  12405  9pos  12406  neg1lt0  12410  halflt1  12511  nn0p1gt0  12582  elnnnn0c  12598  elnnz1  12669  nn0lt10b  12705  recnz  12718  1rp  13061  divlt1lt  13126  divle1le  13127  ledivge1le  13128  nnledivrp  13169  xmulrid  13341  0nelfz1  13603  fz10  13605  fzpreddisj  13633  elfznelfzob  13823  1mod  13954  expgt1  14151  ltexp2a  14216  expcan  14219  ltexp2  14220  leexp2  14221  leexp2a  14222  expnbnd  14281  expnlbnd  14282  expnlbnd2  14283  expmulnbnd  14284  discr1  14288  bcn1  14362  hashnn0n0nn  14440  s2fv0  14936  swrd2lsw  15001  2swrd2eqwrdeq  15002  sgn1  15141  resqrex  15299  mulcn2  15642  cvgrat  15931  bpoly4  16107  cos1bnd  16235  sin01gt0  16238  sincos1sgn  16241  ruclem8  16285  p1modz1  16309  nnoddm1d2  16434  sadcadd  16504  dvdsnprmd  16737  isprm7  16755  divdenle  16796  43prm  17169  plendxnocndx  17443  ipostr  18599  srgbinomlem4  20256  abvtrivd  20855  gzrngunit  21474  znidomb  21603  psgnodpmr  21631  thlleOLD  21740  leordtval2  23241  mopnex  24553  dscopn  24607  metnrmlem1a  24899  xrhmph  24997  evth  25010  xlebnum  25016  vitalilem5  25666  vitali  25667  ply1remlem  26224  plyremlem  26364  plyrem  26365  vieta1lem2  26371  reeff1olem  26508  sinhalfpilem  26523  rplogcl  26664  logtayllem  26719  cxplt  26754  cxple  26755  atanlogaddlem  26974  ressatans  26995  rlimcnp  27026  rlimcnp2  27027  cxp2limlem  27037  cxp2lim  27038  cxploglim2  27040  amgmlem  27051  emcllem2  27058  harmonicubnd  27071  fsumharmonic  27073  zetacvg  27076  ftalem1  27134  ftalem2  27135  chpchtsum  27281  chpub  27282  mersenne  27289  perfectlem2  27292  efexple  27343  chebbnd1  27534  dchrmusumlema  27555  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  dchrisum0flblem2  27571  dchrisum0lema  27576  dchrisum0lem1  27578  dchrisum0lem2a  27579  mulog2sumlem1  27596  chpdifbndlem1  27615  chpdifbnd  27617  selberg3lem1  27619  pntrmax  27626  pntrsumo1  27627  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem1  27651  pntlem3  27671  pnt  27676  ostth2lem1  27680  ostth2lem3  27697  ostth2lem4  27698  axcontlem2  28998  wwlksn0s  29894  clwwlkf1  30081  esumcst  34027  hasheuni  34049  ballotlemi1  34467  ballotlemic  34471  sgnnbi  34510  sgnpbi  34511  sgnmulsgp  34515  signsply0  34528  signswch  34538  hgt750lem  34628  unblimceq0  36473  knoppndvlem1  36478  knoppndvlem2  36479  knoppndvlem7  36484  knoppndvlem13  36490  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem17  36494  knoppndvlem20  36497  irrdiff  37292  poimirlem22  37602  poimirlem31  37611  asindmre  37663  areacirclem4  37671  60gcd7e1  41962  3lexlogpow5ineq2  42012  aks4d1p1p2  42027  aks4d1p7  42040  aks4d1p8d2  42042  aks4d1p8d3  42043  aks4d1p8  42044  aks4d1p9  42045  aks6d1c5lem3  42094  sticksstones11  42113  aks6d1c6lem1  42127  aks6d1c6lem4  42130  aks6d1c7lem2  42138  2xp3dxp2ge1d  42198  explt1d  42310  3cubeslem1  42640  pellexlem2  42786  pellexlem6  42790  pell14qrgt0  42815  elpell1qr2  42828  pellfundex  42842  pellfundrp  42844  rmxypos  42904  relexp01min  43675  imo72b2  44134  radcnvrat  44283  reclt0d  45302  sqrlearg  45471  sumnnodd  45551  liminf10ex  45695  liminfltlimsupex  45702  dvnmul  45864  stoweidlem7  45928  stoweidlem36  45957  stoweidlem38  45959  stoweidlem42  45963  stoweidlem51  45972  stoweidlem59  45980  stirlinglem5  45999  stirlinglem7  46001  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  stirlinglem15  46009  dirkeritg  46023  fourierdlem11  46039  fourierdlem30  46058  fourierdlem47  46074  fourierdlem79  46106  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  etransclem4  46159  etransclem31  46186  etransclem32  46187  etransclem35  46190  etransclem41  46196  salexct2  46260  hoidmvlelem1  46516  tworepnotupword  46805  m1mod0mod1  47243  nfermltl2rev  47617  m1modmmod  48255  regt1loggt0  48270  rege1logbrege0  48292  nnlog2ge0lt1  48300  eenglngeehlnmlem2  48472  amgmwlem  48896