Theorem 0lt1 11525

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 11003	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 10968	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11523	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 688	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 10957	. . 3 ⊢ 1 ∈ ℂ
6	5	mulid1i 11007	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5102	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2101   ≠ wne 2938   class class class wbr 5077  (class class class)co 7295  ℝcr 10898  0cc0 10899  1c1 10900   · cmul 10904   < clt 11037

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 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7608  ax-resscn 10956  ax-1cn 10957  ax-icn 10958  ax-addcl 10959  ax-addrcl 10960  ax-mulcl 10961  ax-mulrcl 10962  ax-mulcom 10963  ax-addass 10964  ax-mulass 10965  ax-distr 10966  ax-i2m1 10967  ax-1ne0 10968  ax-1rid 10969  ax-rnegex 10970  ax-rrecex 10971  ax-cnre 10972  ax-pre-lttri 10973  ax-pre-lttrn 10974  ax-pre-ltadd 10975  ax-pre-mulgt0 10976

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3223  df-rab 3224  df-v 3436  df-sbc 3719  df-csb 3835  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-br 5078  df-opab 5140  df-mpt 5161  df-id 5491  df-po 5505  df-so 5506  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-f1 6452  df-fo 6453  df-f1o 6454  df-fv 6455  df-riota 7252  df-ov 7298  df-oprab 7299  df-mpo 7300  df-er 8518  df-en 8754  df-dom 8755  df-sdom 8756  df-pnf 11039  df-mnf 11040  df-xr 11041  df-ltxr 11042  df-le 11043  df-sub 11235  df-neg 11236

This theorem is referenced by:  0le1  11526  eqneg  11723  elimgt0  11841  ltp1  11843  ltm1  11845  recgt0  11849  mulgt1  11862  reclt1  11898  recgt1  11899  recgt1i  11900  recp1lt1  11901  recreclt  11902  recgt0ii  11909  inelr  11991  nnge1  12029  nngt0  12032  0nnnALT  12038  nnrecgt0  12044  2pos  12104  3pos  12106  4pos  12108  5pos  12110  6pos  12111  7pos  12112  8pos  12113  9pos  12114  neg1lt0  12118  halflt1  12219  nn0p1gt0  12290  elnnnn0c  12306  elnnz1  12374  nn0lt10b  12410  recnz  12423  1rp  12762  divlt1lt  12827  divle1le  12828  ledivge1le  12829  nnledivrp  12870  xmulid1  13041  0nelfz1  13303  fz10  13305  fzpreddisj  13333  elfznelfzob  13521  1mod  13651  expgt1  13849  ltexp2a  13912  expcan  13915  ltexp2  13916  leexp2  13917  leexp2a  13918  expnbnd  13975  expnlbnd  13976  expnlbnd2  13977  expmulnbnd  13978  discr1  13982  bcn1  14055  hashnn0n0nn  14134  s2fv0  14628  swrd2lsw  14693  2swrd2eqwrdeq  14694  sgn1  14831  resqrex  14990  mulcn2  15333  cvgrat  15623  bpoly4  15797  cos1bnd  15924  sin01gt0  15927  sincos1sgn  15930  ruclem8  15974  p1modz1  15998  nnoddm1d2  16123  sadcadd  16193  dvdsnprmd  16423  isprm7  16441  divdenle  16481  43prm  16851  plendxnocndx  17122  ipostr  18275  srgbinomlem4  19807  abvtrivd  20128  gzrngunit  20692  znidomb  20797  psgnodpmr  20823  thlleOLD  20932  leordtval2  22391  mopnex  23703  dscopn  23757  metnrmlem1a  24049  xrhmph  24138  evth  24150  xlebnum  24156  vitalilem5  24804  vitali  24805  ply1remlem  25355  plyremlem  25492  plyrem  25493  vieta1lem2  25499  reeff1olem  25633  sinhalfpilem  25648  rplogcl  25787  logtayllem  25842  cxplt  25877  cxple  25878  atanlogaddlem  26091  ressatans  26112  rlimcnp  26143  rlimcnp2  26144  cxp2limlem  26153  cxp2lim  26154  cxploglim2  26156  amgmlem  26167  emcllem2  26174  harmonicubnd  26187  fsumharmonic  26189  zetacvg  26192  ftalem1  26250  ftalem2  26251  chpchtsum  26395  chpub  26396  mersenne  26403  perfectlem2  26406  efexple  26457  chebbnd1  26648  dchrmusumlema  26669  dchrvmasumlem2  26674  dchrvmasumiflem1  26677  dchrisum0flblem2  26685  dchrisum0lema  26690  dchrisum0lem1  26692  dchrisum0lem2a  26693  mulog2sumlem1  26710  chpdifbndlem1  26729  chpdifbnd  26731  selberg3lem1  26733  pntrmax  26740  pntrsumo1  26741  pntpbnd1a  26761  pntpbnd2  26763  pntibndlem1  26765  pntlem3  26785  pnt  26790  ostth2lem1  26794  ostth2lem3  26811  ostth2lem4  26812  axcontlem2  27361  wwlksn0s  28254  clwwlkf1  28441  esumcst  32059  hasheuni  32081  ballotlemi1  32497  ballotlemic  32501  sgnnbi  32540  sgnpbi  32541  sgnmulsgp  32545  signsply0  32558  signswch  32568  hgt750lem  32659  unblimceq0  34715  knoppndvlem1  34720  knoppndvlem2  34721  knoppndvlem7  34726  knoppndvlem13  34732  knoppndvlem14  34733  knoppndvlem15  34734  knoppndvlem17  34736  knoppndvlem20  34739  irrdiff  35525  poimirlem22  35827  poimirlem31  35836  asindmre  35888  areacirclem4  35896  60gcd7e1  40039  3lexlogpow5ineq2  40089  aks4d1p1p2  40104  aks4d1p7  40117  aks4d1p8d2  40119  aks4d1p8d3  40120  aks4d1p8  40121  aks4d1p9  40122  sticksstones11  40138  2xp3dxp2ge1d  40188  3cubeslem1  40529  pellexlem2  40675  pellexlem6  40679  pell14qrgt0  40704  elpell1qr2  40717  pellfundex  40731  pellfundrp  40733  rmxypos  40793  relexp01min  41345  imo72b2  41807  radcnvrat  41956  reclt0d  42960  sqrlearg  43126  sumnnodd  43206  liminf10ex  43350  liminfltlimsupex  43357  dvnmul  43519  stoweidlem7  43583  stoweidlem36  43612  stoweidlem38  43614  stoweidlem42  43618  stoweidlem51  43627  stoweidlem59  43635  stirlinglem5  43654  stirlinglem7  43656  stirlinglem10  43659  stirlinglem11  43660  stirlinglem12  43661  stirlinglem15  43664  dirkeritg  43678  fourierdlem11  43694  fourierdlem30  43713  fourierdlem47  43729  fourierdlem79  43761  fourierdlem103  43785  fourierdlem104  43786  fouriersw  43807  etransclem4  43814  etransclem31  43841  etransclem32  43842  etransclem35  43845  etransclem41  43851  salexct2  43913  hoidmvlelem1  44169  m1mod0mod1  44861  nfermltl2rev  45235  m1modmmod  45907  regt1loggt0  45922  rege1logbrege0  45944  nnlog2ge0lt1  45952  eenglngeehlnmlem2  46124  amgmwlem  46546  tworepnotupword  46561