Theorem 0lt1 11768

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 11244	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11207	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11766	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11196	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11248	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5150	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2107   ≠ wne 2931   class class class wbr 5125  (class class class)co 7414  ℝcr 11137  0cc0 11138  1c1 11139   · cmul 11143   < clt 11278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-po 5574  df-so 5575  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-er 8728  df-en 8969  df-dom 8970  df-sdom 8971  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11477  df-neg 11478

This theorem is referenced by:  0le1  11769  eqneg  11970  elimgt0  12088  ltp1  12090  ltm1  12092  recgt0  12096  mulgt1OLD  12109  mulgt1  12112  reclt1  12146  recgt1  12147  recgt1i  12148  recp1lt1  12149  recreclt  12150  recgt0ii  12157  inelr  12239  nnge1  12277  nngt0  12280  0nnnALT  12286  nnrecgt0  12292  2pos  12352  3pos  12354  4pos  12356  5pos  12358  6pos  12359  7pos  12360  8pos  12361  9pos  12362  neg1lt0  12366  halflt1  12467  nn0p1gt0  12539  elnnnn0c  12555  elnnz1  12627  nn0lt10b  12664  recnz  12677  1rp  13021  divlt1lt  13087  divle1le  13088  ledivge1le  13089  nnledivrp  13130  xmulrid  13304  0nelfz1  13566  fz10  13568  fzpreddisj  13596  elfznelfzob  13795  1mod  13926  expgt1  14124  ltexp2a  14189  expcan  14192  ltexp2  14193  leexp2  14194  leexp2a  14195  expnbnd  14254  expnlbnd  14255  expnlbnd2  14256  expmulnbnd  14257  discr1  14261  bcn1  14335  hashnn0n0nn  14413  s2fv0  14909  swrd2lsw  14974  2swrd2eqwrdeq  14975  sgn1  15114  resqrex  15272  mulcn2  15615  cvgrat  15902  bpoly4  16078  cos1bnd  16206  sin01gt0  16209  sincos1sgn  16212  ruclem8  16256  p1modz1  16280  nnoddm1d2  16406  sadcadd  16478  dvdsnprmd  16710  isprm7  16728  divdenle  16769  43prm  17142  plendxnocndx  17405  ipostr  18548  srgbinomlem4  20199  abvtrivd  20806  gzrngunit  21418  znidomb  21547  psgnodpmr  21575  thlleOLD  21684  leordtval2  23185  mopnex  24495  dscopn  24549  metnrmlem1a  24835  xrhmph  24933  evth  24946  xlebnum  24952  vitalilem5  25602  vitali  25603  ply1remlem  26159  plyremlem  26301  plyrem  26302  vieta1lem2  26308  reeff1olem  26445  sinhalfpilem  26460  rplogcl  26601  logtayllem  26656  cxplt  26691  cxple  26692  atanlogaddlem  26911  ressatans  26932  rlimcnp  26963  rlimcnp2  26964  cxp2limlem  26974  cxp2lim  26975  cxploglim2  26977  amgmlem  26988  emcllem2  26995  harmonicubnd  27008  fsumharmonic  27010  zetacvg  27013  ftalem1  27071  ftalem2  27072  chpchtsum  27218  chpub  27219  mersenne  27226  perfectlem2  27229  efexple  27280  chebbnd1  27471  dchrmusumlema  27492  dchrvmasumlem2  27497  dchrvmasumiflem1  27500  dchrisum0flblem2  27508  dchrisum0lema  27513  dchrisum0lem1  27515  dchrisum0lem2a  27516  mulog2sumlem1  27533  chpdifbndlem1  27552  chpdifbnd  27554  selberg3lem1  27556  pntrmax  27563  pntrsumo1  27564  pntpbnd1a  27584  pntpbnd2  27586  pntibndlem1  27588  pntlem3  27608  pnt  27613  ostth2lem1  27617  ostth2lem3  27634  ostth2lem4  27635  axcontlem2  28929  wwlksn0s  29828  clwwlkf1  30015  esumcst  34005  hasheuni  34027  ballotlemi1  34446  ballotlemic  34450  sgnnbi  34489  sgnpbi  34490  sgnmulsgp  34494  signsply0  34507  signswch  34517  hgt750lem  34607  unblimceq0  36449  knoppndvlem1  36454  knoppndvlem2  36455  knoppndvlem7  36460  knoppndvlem13  36466  knoppndvlem14  36467  knoppndvlem15  36468  knoppndvlem17  36470  knoppndvlem20  36473  irrdiff  37268  poimirlem22  37590  poimirlem31  37599  asindmre  37651  areacirclem4  37659  60gcd7e1  41947  3lexlogpow5ineq2  41997  aks4d1p1p2  42012  aks4d1p7  42025  aks4d1p8d2  42027  aks4d1p8d3  42028  aks4d1p8  42029  aks4d1p9  42030  aks6d1c5lem3  42079  sticksstones11  42098  aks6d1c6lem1  42112  aks6d1c6lem4  42115  aks6d1c7lem2  42123  2xp3dxp2ge1d  42183  explt1d  42303  3cubeslem1  42640  pellexlem2  42786  pellexlem6  42790  pell14qrgt0  42815  elpell1qr2  42828  pellfundex  42842  pellfundrp  42844  rmxypos  42904  relexp01min  43671  imo72b2  44130  radcnvrat  44278  reclt0d  45343  sqrlearg  45511  sumnnodd  45590  liminf10ex  45734  liminfltlimsupex  45741  dvnmul  45903  stoweidlem7  45967  stoweidlem36  45996  stoweidlem38  45998  stoweidlem42  46002  stoweidlem51  46011  stoweidlem59  46019  stirlinglem5  46038  stirlinglem7  46040  stirlinglem10  46043  stirlinglem11  46044  stirlinglem12  46045  stirlinglem15  46048  dirkeritg  46062  fourierdlem11  46078  fourierdlem30  46097  fourierdlem47  46113  fourierdlem79  46145  fourierdlem103  46169  fourierdlem104  46170  fouriersw  46191  etransclem4  46198  etransclem31  46225  etransclem32  46226  etransclem35  46229  etransclem41  46235  salexct2  46299  hoidmvlelem1  46555  tworepnotupword  46846  m1mod0mod1  47302  nfermltl2rev  47676  m1modmmod  48388  regt1loggt0  48403  rege1logbrege0  48425  nnlog2ge0lt1  48433  eenglngeehlnmlem2  48605  amgmwlem  49317