Theorem 0lt1 11663

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 11135	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11098	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11661	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 698	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11140	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5097	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2119   ≠ wne 2934   class class class wbr 5072  (class class class)co 7356  ℝcr 11028  0cc0 11029  1c1 11030   · cmul 11034   < clt 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371

This theorem is referenced by:  0le1  11664  eqneg  11866  elimgt0  11984  ltp1  11986  ltm1  11988  recgt0  11992  mulgt1OLD  12005  mulgt1  12008  reclt1  12042  recgt1  12043  recgt1i  12044  recp1lt1  12045  recreclt  12046  recgt0ii  12053  neg1lt0  12138  nnge1  12196  nngt0  12199  0nnnALT  12205  nnrecgt0  12211  2pos  12275  3pos  12277  4pos  12279  5pos  12281  6pos  12282  7pos  12283  8pos  12284  9pos  12285  halflt1  12385  nn0p1gt0  12457  elnnnn0c  12473  elnnz1  12544  nn0lt10b  12582  recnz  12595  1rp  12937  divlt1lt  13004  divle1le  13005  ledivge1le  13006  nnledivrp  13047  xmulrid  13222  0nelfz1  13488  fz10  13490  fzpreddisj  13518  elfznelfzob  13720  1mod  13853  expgt1  14053  ltexp2a  14119  expcan  14122  ltexp2  14123  leexp2  14124  leexp2a  14125  expnbnd  14185  expnlbnd  14186  expnlbnd2  14187  expmulnbnd  14188  discr1  14192  bcn1  14266  hashnn0n0nn  14344  s2fv0  14840  swrd2lsw  14905  2swrd2eqwrdeq  14906  sgn1  15045  resqrex  15203  mulcn2  15549  cvgrat  15839  bpoly4  16015  cos1bnd  16145  sin01gt0  16148  sincos1sgn  16151  ruclem8  16195  p1modz1  16219  nnoddm1d2  16346  sadcadd  16418  dvdsnprmd  16650  isprm7  16669  divdenle  16710  43prm  17083  plendxnocndx  17338  ipostr  18486  srgbinomlem4  20201  abvtrivd  20804  gzrngunit  21408  znidomb  21536  psgnodpmr  21565  leordtval2  23195  mopnex  24502  dscopn  24556  metnrmlem1a  24842  xrhmph  24932  evth  24944  xlebnum  24950  vitalilem5  25597  vitali  25598  ply1remlem  26148  plyremlem  26288  plyrem  26289  vieta1lem2  26295  reeff1olem  26429  sinhalfpilem  26445  rplogcl  26586  logtayllem  26641  cxplt  26676  cxple  26677  atanlogaddlem  26895  ressatans  26916  rlimcnp  26947  rlimcnp2  26948  cxp2limlem  26957  cxp2lim  26958  cxploglim2  26960  amgmlem  26971  emcllem2  26978  harmonicubnd  26991  fsumharmonic  26993  zetacvg  26996  ftalem1  27054  ftalem2  27055  chpchtsum  27200  chpub  27201  mersenne  27208  perfectlem2  27211  efexple  27262  chebbnd1  27453  dchrmusumlema  27474  dchrvmasumlem2  27479  dchrvmasumiflem1  27482  dchrisum0flblem2  27490  dchrisum0lema  27495  dchrisum0lem1  27497  dchrisum0lem2a  27498  mulog2sumlem1  27515  chpdifbndlem1  27534  chpdifbnd  27536  selberg3lem1  27538  pntrmax  27545  pntrsumo1  27546  pntpbnd1a  27566  pntpbnd2  27568  pntibndlem1  27570  pntlem3  27590  pnt  27595  ostth2lem1  27599  ostth2lem3  27616  ostth2lem4  27617  axcontlem2  29052  wwlksn0s  29947  clwwlkf1  30137  sgnnbi  32930  sgnpbi  32931  sgnmulsgp  32935  vietadeg1  33762  cos9thpiminplylem1  33966  cos9thpiminply  33972  esumcst  34247  hasheuni  34269  ballotlemi1  34687  ballotlemic  34691  signsply0  34735  signswch  34745  hgt750lem  34835  unblimceq0  36813  knoppndvlem1  36818  knoppndvlem2  36819  knoppndvlem7  36824  knoppndvlem13  36830  knoppndvlem14  36831  knoppndvlem15  36832  knoppndvlem17  36834  knoppndvlem20  36837  irrdiff  37686  poimirlem22  38009  poimirlem31  38018  asindmre  38070  areacirclem4  38078  60gcd7e1  42490  3lexlogpow5ineq2  42540  aks4d1p1p2  42555  aks4d1p7  42568  aks4d1p8d2  42570  aks4d1p8d3  42571  aks4d1p8  42572  aks4d1p9  42573  aks6d1c5lem3  42622  sticksstones11  42641  aks6d1c6lem1  42655  aks6d1c6lem4  42658  aks6d1c7lem2  42666  explt1d  42800  3cubeslem1  43133  pellexlem2  43275  pellexlem6  43279  pell14qrgt0  43304  elpell1qr2  43317  pellfundex  43331  pellfundrp  43333  rmxypos  43392  relexp01min  44157  imo72b2  44616  radcnvrat  44758  reclt0d  45831  sqrlearg  45998  sumnnodd  46075  liminf10ex  46217  liminfltlimsupex  46224  dvnmul  46386  stoweidlem7  46450  stoweidlem36  46479  stoweidlem38  46481  stoweidlem42  46485  stoweidlem51  46494  stoweidlem59  46502  stirlinglem5  46521  stirlinglem7  46523  stirlinglem10  46526  stirlinglem11  46527  stirlinglem12  46528  stirlinglem15  46531  dirkeritg  46545  fourierdlem11  46561  fourierdlem30  46580  fourierdlem47  46596  fourierdlem79  46628  fourierdlem103  46652  fourierdlem104  46653  fouriersw  46674  etransclem4  46681  etransclem31  46708  etransclem32  46709  etransclem35  46712  etransclem41  46718  salexct2  46782  hoidmvlelem1  47038  cjnpoly  47352  m1mod0mod1  47823  m1modmmod  47827  muldvdsfacgt  47849  muldvdsfacm1  47850  nfermltl2rev  48234  regt1loggt0  49027  rege1logbrege0  49049  nnlog2ge0lt1  49057  eenglngeehlnmlem2  49229  amgmwlem  50292