Theorem 0lt1 11878

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 11347	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11308	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11876	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 705	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11297	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11352	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5136	1 ⊢ 0 < 1

This proof depends on syntax axioms:   ∈ wcel 2147   ≠ wne 2959   class class class wbr 5108  (class class class)co 7451  ℝcr 11238  0cc0 11239  1c1 11240   · cmul 11244   < clt 11382

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583

This theorem is used by:  0le1  11879  eqneg  12077  elimgt0  12195  ltp1  12197  ltm1  12199  recgt0  12203  mulgt1  12218  reclt1  12252  recgt1  12253  recgt1i  12254  recp1lt1  12255  recreclt  12256  recgt0ii  12263  neg1lt0  12348  nnge1  12406  nngt0  12409  0nnnALT  12415  nnrecgt0  12421  2posOLD  12488  halflt1  12603  nn0p1gt0  12675  elnnnn0c  12691  elnnz1  12762  nn0lt10b  12801  recnz  12814  1rp  13164  divlt1lt  13231  divle1le  13232  ledivge1le  13233  nnledivrp  13274  xmulrid  13449  0nelfz1  13716  fz10  13718  fzpreddisj  13747  elfznelfzob  13949  1mod  14083  expgt1  14283  ltexp2a  14349  expcan  14352  ltexp2  14353  leexp2  14354  leexp2a  14355  expnbnd  14417  expnlbnd  14418  expnlbnd2  14419  expmulnbnd  14420  discr1  14424  bcn1  14498  hashnn0n0nn  14576  s2fv0  15080  swrd2lsw  15148  2swrd2eqwrdeq  15149  sgn1  15288  sgnnbi  15300  sgnpbi  15301  resqrex  15460  mulcn2  15807  cvgrat  16096  bpoly4  16269  cos1bnd  16399  sin01gt0  16402  sincos1sgn  16405  ruclem8  16449  p1modz1  16473  nnoddm1d2  16600  sadcadd  16672  dvdsnprmd  16909  isprm7  16928  divdenle  16969  43prm  17344  plendxnocndx  17601  ipostr  18753  srgbinomlem4  20506  abvtrivd  21140  gzrngunit  21793  znidomb  21922  psgnodpmr  21951  leordtval2  23585  mopnex  24893  dscopn  24947  metnrmlem1a  25233  xrhmph  25323  evth  25335  xlebnum  25341  vitalilem5  25988  vitali  25989  ply1remlem  26538  plyremlem  26680  plyrem  26681  vieta1lem2  26689  reeff1olem  26830  sinhalfpilem  26849  rplogcl  26989  logtayllem  27044  cxplt  27079  cxple  27080  atanlogaddlem  27298  ressatans  27319  rlimcnp  27350  rlimcnp2  27351  cxp2limlem  27360  cxp2lim  27361  cxploglim2  27363  amgmlem  27374  emcllem2  27381  harmonicubnd  27394  fsumharmonic  27396  zetacvg  27399  ftalem1  27457  ftalem2  27458  chpchtsum  27603  chpub  27604  mersenne  27611  perfectlem2  27614  efexple  27665  chebbnd1  27856  dchrmusumlema  27877  dchrvmasumlem2  27882  dchrvmasumiflem1  27885  dchrisum0flblem2  27893  dchrisum0lema  27898  dchrisum0lem1  27900  dchrisum0lem2a  27901  mulog2sumlem1  27918  chpdifbndlem1  27937  chpdifbnd  27939  selberg3lem1  27941  pntrmax  27948  pntrsumo1  27949  pntpbnd1a  27969  pntpbnd2  27971  pntibndlem1  27973  pntlem3  27993  pnt  27998  ostth2lem1  28002  ostth2lem3  28019  ostth2lem4  28020  axcontlem2  29600  wwlksn0s  30507  clwwlkf1  30697  sgnmulsgp  33519  evls1degle1  34239  rngunsnply1chr2lem1  34250  vietadeg1  34321  cos9thpiminplylem1  34525  cos9thpiminply  34531  esumcst  34806  hasheuni  34828  ballotlemi1  35246  ballotlemic  35250  signsply0  35291  signswch  35301  hgt750lem  35391  unblimceq0  37588  knoppndvlem1  37593  knoppndvlem2  37594  knoppndvlem7  37599  knoppndvlem13  37605  knoppndvlem14  37606  knoppndvlem15  37607  knoppndvlem17  37609  knoppndvlem20  37612  irrdiff  38515  poimirlem22  38828  poimirlem31  38837  asindmre  38889  areacirclem4  38897  60gcd7e1  43321  3lexlogpow5ineq2  43371  aks4d1p1p2  43386  aks4d1p7  43399  aks4d1p8d2  43401  aks4d1p8d3  43402  aks4d1p8  43403  aks4d1p9  43404  aks6d1c5lem3  43453  sticksstones11  43472  aks6d1c6lem1  43486  aks6d1c6lem4  43489  aks6d1c7lem2  43497  explt1d  43646  3cubeslem1  43960  pellexlem2  44103  pellexlem6  44107  pell14qrgt0  44132  elpell1qr2  44145  pellfundex  44159  pellfundrp  44161  rmxypos  44220  relexp01min  44974  imo72b2  45433  radcnvrat  45559  reclt0d  46671  sqrlearg  46838  sumnnodd  46915  liminf10ex  47057  liminfltlimsupex  47064  dvnmul  47226  stoweidlem7  47290  stoweidlem36  47319  stoweidlem38  47321  stoweidlem42  47325  stoweidlem51  47334  stoweidlem59  47342  stirlinglem5  47361  stirlinglem7  47363  stirlinglem10  47366  stirlinglem11  47367  stirlinglem12  47368  stirlinglem15  47371  dirkeritg  47385  fourierdlem11  47401  fourierdlem30  47420  fourierdlem47  47436  fourierdlem79  47468  fourierdlem103  47492  fourierdlem104  47493  fouriersw  47514  etransclem4  47521  etransclem31  47548  etransclem32  47549  etransclem35  47552  etransclem41  47558  salexct2  47622  hoidmvlelem1  47878  cjnpoly  48212  m1mod0mod1  48703  m1modmmod  48707  muldvdsfacgt  48729  muldvdsfacm1  48730  nfermltl2rev  49114  regt1loggt0  49979  rege1logbrege0  50001  nnlog2ge0lt1  50009  eenglngeehlnmlem2  50182  amgmwlem  51415