Theorem 0lt1 11703

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 11175	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11136	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11701	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 702	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11125	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11180	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5122	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2141   ≠ wne 2956   class class class wbr 5097  (class class class)co 7391  ℝcr 11066  0cc0 11067  1c1 11068   · cmul 11072   < clt 11210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411

This theorem is referenced by:  0le1  11704  eqneg  11905  elimgt0  12023  ltp1  12025  ltm1  12027  recgt0  12031  mulgt1OLD  12044  mulgt1  12047  reclt1  12081  recgt1  12082  recgt1i  12083  recp1lt1  12084  recreclt  12085  recgt0ii  12092  neg1lt0  12177  nnge1  12235  nngt0  12238  0nnnALT  12244  nnrecgt0  12250  2posOLD  12317  halflt1  12432  nn0p1gt0  12504  elnnnn0c  12520  elnnz1  12591  nn0lt10b  12629  recnz  12642  1rp  12991  divlt1lt  13058  divle1le  13059  ledivge1le  13060  nnledivrp  13101  xmulrid  13276  0nelfz1  13542  fz10  13544  fzpreddisj  13572  elfznelfzob  13774  1mod  13907  expgt1  14107  ltexp2a  14173  expcan  14176  ltexp2  14177  leexp2  14178  leexp2a  14179  expnbnd  14239  expnlbnd  14240  expnlbnd2  14241  expmulnbnd  14242  discr1  14246  bcn1  14320  hashnn0n0nn  14398  s2fv0  14894  swrd2lsw  14959  2swrd2eqwrdeq  14960  sgn1  15099  sgnnbi  15108  sgnpbi  15109  resqrex  15268  mulcn2  15614  cvgrat  15904  bpoly4  16080  cos1bnd  16210  sin01gt0  16213  sincos1sgn  16216  ruclem8  16260  p1modz1  16284  nnoddm1d2  16411  sadcadd  16483  dvdsnprmd  16715  isprm7  16734  divdenle  16775  43prm  17149  plendxnocndx  17404  ipostr  18552  srgbinomlem4  20266  abvtrivd  20869  gzrngunit  21473  znidomb  21601  psgnodpmr  21630  leordtval2  23260  mopnex  24567  dscopn  24621  metnrmlem1a  24907  xrhmph  24997  evth  25009  xlebnum  25015  vitalilem5  25662  vitali  25663  ply1remlem  26213  plyremlem  26356  plyrem  26357  vieta1lem2  26363  reeff1olem  26497  sinhalfpilem  26516  rplogcl  26657  logtayllem  26712  cxplt  26747  cxple  26748  atanlogaddlem  26966  ressatans  26987  rlimcnp  27018  rlimcnp2  27019  cxp2limlem  27028  cxp2lim  27029  cxploglim2  27031  amgmlem  27042  emcllem2  27049  harmonicubnd  27062  fsumharmonic  27064  zetacvg  27067  ftalem1  27125  ftalem2  27126  chpchtsum  27271  chpub  27272  mersenne  27279  perfectlem2  27282  efexple  27333  chebbnd1  27524  dchrmusumlema  27545  dchrvmasumlem2  27550  dchrvmasumiflem1  27553  dchrisum0flblem2  27561  dchrisum0lema  27566  dchrisum0lem1  27568  dchrisum0lem2a  27569  mulog2sumlem1  27586  chpdifbndlem1  27605  chpdifbnd  27607  selberg3lem1  27609  pntrmax  27616  pntrsumo1  27617  pntpbnd1a  27637  pntpbnd2  27639  pntibndlem1  27641  pntlem3  27661  pnt  27666  ostth2lem1  27670  ostth2lem3  27687  ostth2lem4  27688  axcontlem2  29123  wwlksn0s  30018  clwwlkf1  30208  sgnmulsgp  32995  vietadeg1  33836  cos9thpiminplylem1  34040  cos9thpiminply  34046  esumcst  34321  hasheuni  34343  ballotlemi1  34761  ballotlemic  34765  signsply0  34806  signswch  34816  hgt750lem  34906  unblimceq0  36906  knoppndvlem1  36911  knoppndvlem2  36912  knoppndvlem7  36917  knoppndvlem13  36923  knoppndvlem14  36924  knoppndvlem15  36925  knoppndvlem17  36927  knoppndvlem20  36930  irrdiff  37779  poimirlem22  38102  poimirlem31  38111  asindmre  38163  areacirclem4  38171  60gcd7e1  42583  3lexlogpow5ineq2  42633  aks4d1p1p2  42648  aks4d1p7  42661  aks4d1p8d2  42663  aks4d1p8d3  42664  aks4d1p8  42665  aks4d1p9  42666  aks6d1c5lem3  42715  sticksstones11  42734  aks6d1c6lem1  42748  aks6d1c6lem4  42751  aks6d1c7lem2  42759  explt1d  42893  3cubeslem1  43226  pellexlem2  43368  pellexlem6  43372  pell14qrgt0  43397  elpell1qr2  43410  pellfundex  43424  pellfundrp  43426  rmxypos  43485  relexp01min  44250  imo72b2  44709  radcnvrat  44851  reclt0d  45923  sqrlearg  46090  sumnnodd  46167  liminf10ex  46309  liminfltlimsupex  46316  dvnmul  46478  stoweidlem7  46542  stoweidlem36  46571  stoweidlem38  46573  stoweidlem42  46577  stoweidlem51  46586  stoweidlem59  46594  stirlinglem5  46613  stirlinglem7  46615  stirlinglem10  46618  stirlinglem11  46619  stirlinglem12  46620  stirlinglem15  46623  dirkeritg  46637  fourierdlem11  46653  fourierdlem30  46672  fourierdlem47  46688  fourierdlem79  46720  fourierdlem103  46744  fourierdlem104  46745  fouriersw  46766  etransclem4  46773  etransclem31  46800  etransclem32  46801  etransclem35  46804  etransclem41  46810  salexct2  46874  hoidmvlelem1  47130  cjnpoly  47444  m1mod0mod1  47915  m1modmmod  47919  muldvdsfacgt  47941  muldvdsfacm1  47942  nfermltl2rev  48326  regt1loggt0  49119  rege1logbrege0  49141  nnlog2ge0lt1  49149  eenglngeehlnmlem2  49321  amgmwlem  50384