Theorem 1red 11143

Description: The number 1 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1red	⊢ (𝜑 → 1 ∈ ℝ)

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 11142	. 2 ⊢ 1 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11035  1c1 11037

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-ext 2712  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-mulrcl 11099  ax-i2m1 11104  ax-1ne0 11105  ax-rrecex 11108  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366

This theorem is referenced by:  recgt0  11999  mulgt1  12015  ltrec  12036  nnne0  12209  nn0p1gt0  12464  nn0ge2m1nn  12505  nn0le2is012  12591  suprzcl  12607  ledivge1le  13013  ge2halflem1  13057  qbtwnre  13149  lincmb01cmp  13446  iccf1o  13447  xov1plusxeqvd  13449  zltaddlt1le  13456  nnge2recico01  13458  fznatpl1  13530  elfz1b  13545  elfzo0subge1  13658  fzonn0p1p1  13697  elfznelfzo  13726  elfznelfzob  13727  fladdz  13782  2tnp1ge0ge0  13786  flhalf  13787  ltdifltdiv  13791  fldiv4lem1div2uz2  13793  mulp1mod1  13871  m1modge3gt1  13878  modltm1p1mod  13883  addmodlteq  13906  ltexp2a  14126  expcan  14129  ltexp2  14130  leexp2  14131  leexp2a  14132  leexp2r  14134  nnlesq  14165  bernneq3  14191  expnbnd  14192  expnlbnd2  14194  expnngt1  14201  fzsdom2  14388  wrdlenge2n0  14512  swrd2lsw  14912  2swrd2eqwrdeq  14913  01sqrexlem7  15208  rddif  15301  reccn2  15557  rlimo1  15577  o1fsum  15774  abscvgcvg  15780  climcndslem1  15812  flo1  15817  harmonic  15822  geomulcvg  15839  fprodrecl  15916  fprodreclf  15922  fprodle  15959  bpoly4  16022  efcllem  16040  efgt1  16081  tanhlt1  16125  sinltx  16154  eirrlem  16169  p1modz1  16226  mod2eq1n2dvds  16314  oddge22np1  16316  ltoddhalfle  16328  nn0o1gt2  16348  nno  16349  nn0oddm1d2  16352  nnoddm1d2  16353  bitsfzolem  16401  bitsfzo  16402  bitsmod  16403  bitscmp  16405  bitsinv1lem  16408  smuval2  16449  coprmgcdb  16616  prmind2  16652  dvdsnprmd  16657  2mulprm  16660  isprm5  16675  isprm7  16676  divdenle  16717  zsqrtelqelz  16726  fermltl  16752  odzdvds  16764  modprm0  16774  iserodd  16804  difsqpwdvds  16856  pcfaclem  16867  prmreclem1  16885  4sqlem11  16924  4sqlem12  16925  ramub1lem1  16995  prmgaplem8  17027  2expltfac  17061  chnccat  18590  pgpfaclem2  20057  znidomb  21543  psdmvr  22164  chfacfisf  22844  chfacfisfcpmat  22845  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  nrginvrcnlem  24681  nmoid  24732  xrsmopn  24803  metnrmlem1a  24849  iihalf2cn  24926  iccpnfhmeo  24937  lebnumii  24958  htpycc  24972  pcohtpylem  25011  pcoass  25016  pcorevlem  25018  nmhmcn  25112  cncmet  25314  ovoliunlem1  25494  dyadmaxlem  25589  vitalilem2  25601  mbfi1fseqlem6  25712  itg2mulc  25739  itg2monolem1  25742  itg2monolem3  25744  dveflem  25971  mvth  25984  dvlipcn  25986  lhop1lem  26005  dvfsumlem1  26018  dvfsumlem2  26019  dvfsumlem3  26020  dvfsumlem4  26021  dvfsum2  26026  fta1glem2  26159  plyeq0lem  26200  fta1lem  26298  vieta1lem2  26302  aalioulem3  26325  aalioulem4  26326  radcnvlem1  26403  radcnvlem2  26404  dvradcnv  26411  abelthlem2  26422  abelthlem5  26425  abelthlem7  26428  abelth2  26432  cos02pilt1  26515  cosne0  26518  rplogcl  26593  logdivlti  26609  logno1  26625  dvlog2lem  26641  advlog  26643  logtayllem  26648  cxplt  26683  cxple  26684  cxpaddlelem  26740  cxpaddle  26741  rtprmirr  26749  relogbf  26780  logbgt0b  26782  isosctrlem1  26807  isosctrlem2  26808  chordthmlem4  26824  heron  26827  atanlogaddlem  26902  bndatandm  26918  leibpi  26931  log2tlbnd  26934  birthdaylem3  26942  rlimcnp  26954  rlimcnp2  26955  efrlim  26958  cxp2limlem  26964  cxp2lim  26965  divsqrtsumo1  26972  jensenlem2  26976  logdiflbnd  26983  fsumharmonic  27000  lgamgulmlem2  27018  lgamgulmlem3  27019  lgamgulmlem4  27020  lgamgulmlem5  27021  lgamgulmlem6  27022  lgamcvg2  27043  regamcl  27049  wilthlem2  27057  ftalem2  27062  basellem9  27077  vma1  27154  ppieq0  27164  mumullem2  27168  fsumfldivdiaglem  27177  chpeq0  27196  chtub  27200  chpval2  27206  chpchtsum  27207  chpub  27208  logfacrlim  27212  logexprlim  27213  mersenne  27215  perfectlem2  27218  dchrelbas4  27231  bcmono  27265  bposlem1  27272  bposlem2  27273  zabsle1  27284  lgslem3  27287  lgsmod  27311  lgsdir2lem4  27316  lgsdirprm  27319  gausslemma2dlem1a  27353  gausslemma2d  27362  lgsquadlem2  27369  2sqlem8  27414  chebbnd1lem1  27457  chebbnd1lem2  27458  chtppilimlem1  27461  chebbnd2  27465  chto1lb  27466  chpchtlim  27467  chpo1ubb  27469  vmadivsum  27470  rplogsumlem1  27472  rpvmasumlem  27475  dchrisumlem3  27479  dchrmusumlema  27481  dchrmusum2  27482  dchrvmasumlem2  27486  dchrvmasumlem3  27487  dchrvmasumiflem1  27489  dchrvmasumiflem2  27490  dchrisum0flblem1  27496  dchrisum0flblem2  27497  dchrisum0fno1  27499  dchrisum0re  27501  dchrisum0lema  27502  dchrisum0lem1b  27503  dchrisum0lem2a  27505  dchrisum0lem2  27506  dchrisum0lem3  27507  rplogsum  27515  dirith2  27516  mudivsum  27518  mulogsumlem  27519  mulogsum  27520  mulog2sumlem1  27522  mulog2sumlem2  27523  vmalogdivsum2  27526  vmalogdivsum  27527  2vmadivsumlem  27528  log2sumbnd  27532  selberglem2  27534  selberg2lem  27538  chpdifbnd  27543  selberg3lem1  27545  selberg3  27547  selberg4lem1  27548  selberg4  27549  pntrmax  27552  pntrsumo1  27553  pntrsumbnd  27554  selberg3r  27557  selberg4r  27558  selberg34r  27559  pntrlog2bndlem1  27565  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntrlog2bndlem6  27571  pntrlog2bnd  27572  pntpbnd1a  27573  pntpbnd1  27574  pntibndlem2a  27578  pntibndlem2  27579  pntibnd  27581  pntlemc  27583  pntlemg  27586  pntlemr  27590  pntlemk  27594  pnt  27602  qabvle  27613  ostth2lem3  27623  ostth2  27625  trgcgrg  28608  tgcgr4  28624  ttgcontlem1  28978  axpaschlem  29034  axlowdimlem16  29051  axcontlem2  29059  axcontlem7  29064  nbusgrvtxm1  29473  upgrewlkle2  29700  pthdlem1  29859  crctcshwlkn0lem3  29905  crctcshwlkn0lem5  29907  wwlksm1edg  29974  wwlksnextproplem2  30003  clwlkclwwlklem2fv1  30090  clwlkclwwlklem2fv2  30091  clwlkclwwlklem2  30095  clwlkclwwlk2  30098  clwwisshclwwslem  30109  clwwlkf1  30144  clwwlkext2edg  30151  clwlknf1oclwwlknlem1  30176  clwwlknonex2lem2  30203  numclwwlk7  30486  frgrreggt1  30488  frgrogt3nreg  30492  smcnlem  30793  nmoub3i  30869  blocnilem  30900  ubthlem2  30967  minvecolem4  30976  htthlem  31013  nmcexi  32122  nmopcoi  32191  stadd3i  32344  cdj1i  32529  nnmulge  32838  receqid  32843  nndiffz1  32885  fzsplit3  32892  nexple  32943  indf1o  32950  wrdt2ind  33039  pmtrto1cl  33187  fzto1st1  33190  fzto1st  33191  psgnfzto1st  33193  cycpmco2lem6  33219  cycpmco2lem7  33220  cycpmrn  33231  qsidomlem1  33542  krull  33569  ply1degltel  33684  ply1degltlss  33686  constrnegcl  33954  constrdircl  33956  iconstr  33957  constrrecl  33960  constrmulcl  33962  constrreinvcl  33963  constrresqrtcl  33968  cos9thpiminplylem1  33973  cos9thpiminply  33979  cos9thpinconstrlem1  33980  1smat1  33995  submateqlem1  33998  madjusmdetlem2  34019  unitdivcld  34092  sqsscirc1  34099  esumdivc  34274  dya2ub  34461  dya2iocress  34465  dya2iocbrsiga  34466  dya2icobrsiga  34467  dya2icoseg  34468  dya2iocucvr  34475  sxbrsigalem2  34477  fibp1  34592  probmeasb  34621  dstrvprob  34663  dstfrvunirn  34666  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemsgt1  34702  ballotlemsel1i  34704  ballotlemfrcn0  34721  signsply0  34742  itgexpif  34797  reprlt  34810  chtvalz  34820  breprexplemc  34823  breprexp  34824  circlemeth  34831  tgoldbachgnn  34850  acycgr1v  35384  subfaclim  35423  cvmliftlem2  35521  cvmliftlem13  35531  snmlff  35564  bccolsum  35974  faclim  35981  nn0prpwlem  36557  dnibndlem10  36800  dnibndlem12  36802  knoppcnlem4  36809  unblimceq0  36820  knoppndvlem1  36825  knoppndvlem2  36826  knoppndvlem3  36827  knoppndvlem7  36831  knoppndvlem11  36835  knoppndvlem12  36836  knoppndvlem14  36838  knoppndvlem15  36839  knoppndvlem17  36841  knoppndvlem18  36842  knoppndvlem20  36844  irrdiff  37693  poimirlem6  38000  poimirlem7  38001  poimirlem15  38009  poimirlem19  38013  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  broucube  38028  itg2addnclem2  38046  itg2addnclem3  38047  areacirclem1  38082  areacirclem4  38085  incsequz  38122  totbndbnd  38163  bfplem2  38197  resdvopclptsd  42520  lcmineqlem2  42522  lcmineqlem3  42523  lcmineqlem10  42530  lcmineqlem12  42532  lcmineqlem15  42535  lcmineqlem18  42538  lcmineqlem19  42539  lcmineqlem20  42540  lcmineqlem22  42542  lcmineqlem23  42543  3lexlogpow5ineq2  42547  3lexlogpow5ineq4  42548  3lexlogpow5ineq3  42549  3lexlogpow2ineq1  42550  3lexlogpow2ineq2  42551  3lexlogpow5ineq5  42552  aks4d1lem1  42554  dvrelog2  42556  dvrelog3  42557  dvrelog2b  42558  dvrelogpow2b  42560  aks4d1p1p3  42561  aks4d1p1p2  42562  aks4d1p1p4  42563  aks4d1p1p6  42565  aks4d1p1p7  42566  aks4d1p1p5  42567  aks4d1p1  42568  aks4d1p2  42569  aks4d1p3  42570  aks4d1p5  42572  aks4d1p6  42573  aks4d1p7d1  42574  aks4d1p7  42575  aks4d1p8d2  42577  aks4d1p8d3  42578  aks4d1p8  42579  aks4d1p9  42580  posbezout  42592  primrootlekpowne0  42597  primrootspoweq0  42598  aks6d1c1  42608  aks6d1c2p2  42611  hashscontpow1  42613  aks6d1c3  42615  aks6d1c2lem4  42619  aks6d1c2  42622  2np3bcnp1  42636  2ap1caineq  42637  sticksstones6  42643  sticksstones7  42644  sticksstones10  42647  sticksstones12a  42649  sticksstones12  42650  sticksstones22  42660  aks6d1c6lem3  42664  aks6d1c6lem4  42665  bcled  42670  bcle2d  42671  aks6d1c7lem1  42672  aks6d1c7lem2  42673  unitscyglem2  42688  unitscyglem4  42690  unitscyglem5  42691  aks5lem8  42693  sn-1ne2  42755  redvmptabs  42844  sn-00idlem2  42883  sn-0ne2  42890  rei4  42908  rediveq1d  42935  sn-rediv1d  42936  sn-rereccld  42939  rerecne0d  42940  rerecidd  42941  rerecrecd  42943  sn-0tie0  42948  sn-nnne0  42957  mulgt0b1d  42969  sn-ltmulgt11d  42971  sn-0lt1  42972  sn-mulgt1d  42976  fimgmcyc  43027  flt4lem7  43116  fltnlta  43120  3cubeslem1  43140  3cubeslem3r  43143  3cubeslem4  43145  lzenom  43226  irrapxlem1  43274  irrapxlem2  43275  irrapxlem4  43277  irrapxlem5  43278  pellexlem2  43282  pell1qrge1  43322  pell1qr1  43323  elpell1qr2  43324  pell14qrgapw  43328  pellfundgt1  43335  pellfundglb  43337  pellfundex  43338  pellfundrp  43340  pellfundne1  43341  rmspecsqrtnq  43358  rmspecnonsq  43359  rmspecfund  43361  rmspecpos  43368  monotoddzzfi  43394  rmygeid  43416  areaquad  43668  imo72b2lem0  44616  imo72b2lem1  44620  imo72b2  44623  cvgdvgrat  44764  radcnvrat  44765  hashnzfzclim  44773  lhe4.4ex1a  44780  binomcxplemnn0  44800  binomcxplemdvbinom  44804  binomcxplemnotnn0  44807  oddfl  45733  abscosbd  45734  zltlesub  45740  abssinbd  45750  monoords  45752  fzisoeu  45755  fzdifsuc2  45765  suplesup  45791  xralrple2  45806  infxr  45818  infleinflem2  45822  reclt0d  45838  xrralrecnnge  45841  sqrlearg  46005  iooiinioc  46008  fmul01  46032  fmul01lt1lem1  46036  fmul01lt1lem2  46037  climsuselem1  46059  sumnnodd  46082  0ellimcdiv  46099  dvmptidg  46367  dvcosax  46376  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvxpaek  46390  dvnmul  46393  iblspltprt  46423  itgspltprt  46429  stoweidlem5  46455  stoweidlem7  46457  stoweidlem10  46460  stoweidlem11  46461  stoweidlem12  46462  stoweidlem13  46463  stoweidlem14  46464  stoweidlem16  46466  stoweidlem18  46468  stoweidlem20  46470  stoweidlem24  46474  stoweidlem25  46475  stoweidlem34  46484  stoweidlem36  46486  stoweidlem38  46488  stoweidlem40  46490  stoweidlem41  46491  stoweidlem42  46492  stoweidlem45  46495  stoweidlem51  46501  stoweidlem60  46510  wallispilem3  46517  wallispilem4  46518  wallispilem5  46519  wallispi  46520  wallispi2lem1  46521  wallispi2lem2  46522  wallispi2  46523  stirlinglem1  46524  stirlinglem3  46526  stirlinglem5  46528  stirlinglem6  46529  stirlinglem7  46530  stirlinglem8  46531  stirlinglem10  46533  stirlinglem11  46534  stirlinglem12  46535  stirlinglem13  46536  stirlinglem15  46538  dirker2re  46542  dirkerval2  46544  dirkerre  46545  dirkertrigeqlem1  46548  dirkertrigeqlem3  46550  dirkeritg  46552  dirkercncflem1  46553  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem5  46562  fourierdlem6  46563  fourierdlem11  46568  fourierdlem15  46572  fourierdlem19  46576  fourierdlem20  46577  fourierdlem24  46581  fourierdlem26  46583  fourierdlem28  46585  fourierdlem30  46587  fourierdlem39  46596  fourierdlem41  46598  fourierdlem43  46600  fourierdlem47  46603  fourierdlem48  46604  fourierdlem56  46612  fourierdlem60  46616  fourierdlem61  46617  fourierdlem62  46618  fourierdlem64  46620  fourierdlem65  46621  fourierdlem66  46622  fourierdlem68  46624  fourierdlem73  46629  fourierdlem78  46634  fourierdlem79  46635  fourierdlem87  46643  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  fouriersw  46681  etransclem4  46688  etransclem23  46707  etransclem24  46708  etransclem31  46715  etransclem32  46716  etransclem35  46719  etransclem41  46725  etransclem46  46730  etransclem48  46732  etransc  46733  ioorrnopnxrlem  46756  nnfoctbdjlem  46905  iundjiun  46910  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  ovnhoilem1  47051  vonioolem2  47131  vonicclem2  47134  pimrecltneg  47174  smfrec  47239  smfmullem1  47241  smfmullem2  47242  smfdiv  47247  sigaradd  47316  ormkglobd  47327  cjnpoly  47359  p1lep2  47770  zm1nn  47772  ceilhalfgt1  47803  2tceilhalfelfzo1  47806  ceilbi  47807  rehalfge1  47809  ceilhalfnn  47810  flmrecm1  47813  addmodne  47820  m1mod0mod1  47830  m1modmmod  47834  difmodm1lt  47835  modmknepk  47838  modp2nep1  47843  modm1nem2  47845  2timesltsqm1  47849  muldvdsfacm1  47857  iccpartiltu  47904  iccpartlt  47906  iccpartgt  47909  fmtnoge3  48015  fmtnodvds  48029  fmtnoprmfac2lem1  48051  2pwp1prm  48074  flsqrt  48078  sfprmdvdsmersenne  48088  lighneallem2  48091  lighneallem4a  48093  proththdlem  48098  proththd  48099  nprmdvdsfacm1lem4  48108  nnoALTV  48193  bgoldbtbndlem4  48306  gpgprismgrusgra  48556  gpgedgvtx0  48559  gpgvtxedg0  48561  gpg5nbgrvtx03starlem2  48567  gpg3kgrtriexlem4  48584  gpg3kgrtriexlem6  48586  cznnring  48760  divge1b  49010  divgt1b  49011  nn0eo  49026  regt1loggt0  49034  rege1logbrege0  49056  logblt1b  49062  fllog2  49066  nnolog2flm1  49088  dignn0flhalflem1  49113  rrxlinesc  49233  rrxlinec  49234  eenglngeehlnmlem1  49235  eenglngeehlnmlem2  49236  line2ylem  49249  line2  49250  line2xlem  49251  reseccl  50250  recsccl  50251  amgmwlem  50299  amgmlemALT  50300