Theorem 0lt1 11634

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 11107	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11070	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11632	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11059	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11111	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5111	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2111   ≠ wne 2928   class class class wbr 5086  (class class class)co 7341  ℝcr 11000  0cc0 11001  1c1 11002   · cmul 11006   < clt 11141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077  ax-pre-mulgt0 11078

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-po 5519  df-so 5520  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-sub 11341  df-neg 11342

This theorem is referenced by:  0le1  11635  eqneg  11836  elimgt0  11954  ltp1  11956  ltm1  11958  recgt0  11962  mulgt1OLD  11975  mulgt1  11978  reclt1  12012  recgt1  12013  recgt1i  12014  recp1lt1  12015  recreclt  12016  recgt0ii  12023  neg1lt0  12108  nnge1  12148  nngt0  12151  0nnnALT  12157  nnrecgt0  12163  2pos  12223  3pos  12225  4pos  12227  5pos  12229  6pos  12230  7pos  12231  8pos  12232  9pos  12233  halflt1  12333  nn0p1gt0  12405  elnnnn0c  12421  elnnz1  12493  nn0lt10b  12530  recnz  12543  1rp  12889  divlt1lt  12956  divle1le  12957  ledivge1le  12958  nnledivrp  12999  xmulrid  13173  0nelfz1  13438  fz10  13440  fzpreddisj  13468  elfznelfzob  13669  1mod  13802  expgt1  14002  ltexp2a  14068  expcan  14071  ltexp2  14072  leexp2  14073  leexp2a  14074  expnbnd  14134  expnlbnd  14135  expnlbnd2  14136  expmulnbnd  14137  discr1  14141  bcn1  14215  hashnn0n0nn  14293  s2fv0  14789  swrd2lsw  14854  2swrd2eqwrdeq  14855  sgn1  14994  resqrex  15152  mulcn2  15498  cvgrat  15785  bpoly4  15961  cos1bnd  16091  sin01gt0  16094  sincos1sgn  16097  ruclem8  16141  p1modz1  16165  nnoddm1d2  16292  sadcadd  16364  dvdsnprmd  16596  isprm7  16614  divdenle  16655  43prm  17028  plendxnocndx  17283  ipostr  18430  srgbinomlem4  20142  abvtrivd  20742  gzrngunit  21365  znidomb  21493  psgnodpmr  21522  leordtval2  23122  mopnex  24429  dscopn  24483  metnrmlem1a  24769  xrhmph  24867  evth  24880  xlebnum  24886  vitalilem5  25535  vitali  25536  ply1remlem  26092  plyremlem  26234  plyrem  26235  vieta1lem2  26241  reeff1olem  26378  sinhalfpilem  26394  rplogcl  26535  logtayllem  26590  cxplt  26625  cxple  26626  atanlogaddlem  26845  ressatans  26866  rlimcnp  26897  rlimcnp2  26898  cxp2limlem  26908  cxp2lim  26909  cxploglim2  26911  amgmlem  26922  emcllem2  26929  harmonicubnd  26942  fsumharmonic  26944  zetacvg  26947  ftalem1  27005  ftalem2  27006  chpchtsum  27152  chpub  27153  mersenne  27160  perfectlem2  27163  efexple  27214  chebbnd1  27405  dchrmusumlema  27426  dchrvmasumlem2  27431  dchrvmasumiflem1  27434  dchrisum0flblem2  27442  dchrisum0lema  27447  dchrisum0lem1  27449  dchrisum0lem2a  27450  mulog2sumlem1  27467  chpdifbndlem1  27486  chpdifbnd  27488  selberg3lem1  27490  pntrmax  27497  pntrsumo1  27498  pntpbnd1a  27518  pntpbnd2  27520  pntibndlem1  27522  pntlem3  27542  pnt  27547  ostth2lem1  27551  ostth2lem3  27568  ostth2lem4  27569  axcontlem2  28938  wwlksn0s  29834  clwwlkf1  30021  sgnnbi  32813  sgnpbi  32814  sgnmulsgp  32818  cos9thpiminplylem1  33787  cos9thpiminply  33793  esumcst  34068  hasheuni  34090  ballotlemi1  34508  ballotlemic  34512  signsply0  34556  signswch  34566  hgt750lem  34656  unblimceq0  36541  knoppndvlem1  36546  knoppndvlem2  36547  knoppndvlem7  36552  knoppndvlem13  36558  knoppndvlem14  36559  knoppndvlem15  36560  knoppndvlem17  36562  knoppndvlem20  36565  irrdiff  37360  poimirlem22  37682  poimirlem31  37691  asindmre  37743  areacirclem4  37751  60gcd7e1  42038  3lexlogpow5ineq2  42088  aks4d1p1p2  42103  aks4d1p7  42116  aks4d1p8d2  42118  aks4d1p8d3  42119  aks4d1p8  42120  aks4d1p9  42121  aks6d1c5lem3  42170  sticksstones11  42189  aks6d1c6lem1  42203  aks6d1c6lem4  42206  aks6d1c7lem2  42214  explt1d  42356  3cubeslem1  42717  pellexlem2  42863  pellexlem6  42867  pell14qrgt0  42892  elpell1qr2  42905  pellfundex  42919  pellfundrp  42921  rmxypos  42980  relexp01min  43746  imo72b2  44205  radcnvrat  44347  reclt0d  45425  sqrlearg  45593  sumnnodd  45670  liminf10ex  45812  liminfltlimsupex  45819  dvnmul  45981  stoweidlem7  46045  stoweidlem36  46074  stoweidlem38  46076  stoweidlem42  46080  stoweidlem51  46089  stoweidlem59  46097  stirlinglem5  46116  stirlinglem7  46118  stirlinglem10  46121  stirlinglem11  46122  stirlinglem12  46123  stirlinglem15  46126  dirkeritg  46140  fourierdlem11  46156  fourierdlem30  46175  fourierdlem47  46191  fourierdlem79  46223  fourierdlem103  46247  fourierdlem104  46248  fouriersw  46269  etransclem4  46276  etransclem31  46303  etransclem32  46304  etransclem35  46307  etransclem41  46313  salexct2  46377  hoidmvlelem1  46633  cjnpoly  46920  m1mod0mod1  47385  m1modmmod  47389  nfermltl2rev  47774  regt1loggt0  48568  rege1logbrege0  48590  nnlog2ge0lt1  48598  eenglngeehlnmlem2  48770  amgmwlem  49834