Theorem 1red 11120

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 11119	. 2 ⊢ 1 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11012  1c1 11014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-mulcl 11075  ax-mulrcl 11076  ax-i2m1 11081  ax-1ne0 11082  ax-rrecex 11085  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355

This theorem is referenced by:  recgt0  11974  mulgt1  11990  ltrec  12011  nnne0  12166  nn0p1gt0  12417  nn0ge2m1nn  12458  nn0le2is012  12543  suprzcl  12559  ledivge1le  12965  ge2halflem1  13009  qbtwnre  13100  lincmb01cmp  13397  iccf1o  13398  xov1plusxeqvd  13400  zltaddlt1le  13407  fznatpl1  13480  elfz1b  13495  elfzo0subge1  13607  fzonn0p1p1  13646  elfznelfzo  13675  elfznelfzob  13676  fladdz  13731  2tnp1ge0ge0  13735  flhalf  13736  ltdifltdiv  13740  fldiv4lem1div2uz2  13742  mulp1mod1  13820  m1modge3gt1  13827  modltm1p1mod  13832  addmodlteq  13855  ltexp2a  14075  expcan  14078  ltexp2  14079  leexp2  14080  leexp2a  14081  leexp2r  14083  nnlesq  14114  bernneq3  14140  expnbnd  14141  expnlbnd2  14143  expnngt1  14150  fzsdom2  14337  wrdlenge2n0  14461  swrd2lsw  14861  2swrd2eqwrdeq  14862  01sqrexlem7  15157  rddif  15250  reccn2  15506  rlimo1  15526  o1fsum  15722  abscvgcvg  15728  climcndslem1  15758  flo1  15763  harmonic  15768  geomulcvg  15785  fprodrecl  15862  fprodreclf  15868  fprodle  15905  bpoly4  15968  efcllem  15986  efgt1  16027  tanhlt1  16071  sinltx  16100  eirrlem  16115  p1modz1  16172  mod2eq1n2dvds  16260  oddge22np1  16262  ltoddhalfle  16274  nn0o1gt2  16294  nno  16295  nn0oddm1d2  16298  nnoddm1d2  16299  bitsfzolem  16347  bitsfzo  16348  bitsmod  16349  bitscmp  16351  bitsinv1lem  16354  smuval2  16395  coprmgcdb  16562  prmind2  16598  dvdsnprmd  16603  2mulprm  16606  isprm5  16620  isprm7  16621  divdenle  16662  zsqrtelqelz  16671  fermltl  16697  odzdvds  16709  modprm0  16719  iserodd  16749  difsqpwdvds  16801  pcfaclem  16812  prmreclem1  16830  4sqlem11  16869  4sqlem12  16870  ramub1lem1  16940  prmgaplem8  16972  2expltfac  17006  chnccat  18534  pgpfaclem2  19998  znidomb  21500  psdmvr  22085  chfacfisf  22770  chfacfisfcpmat  22771  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  nrginvrcnlem  24607  nmoid  24658  xrsmopn  24729  metnrmlem1a  24775  iihalf2cn  24857  iccpnfhmeo  24871  lebnumii  24893  htpycc  24907  pcohtpylem  24947  pcoass  24952  pcorevlem  24954  nmhmcn  25048  cncmet  25250  ovoliunlem1  25431  dyadmaxlem  25526  vitalilem2  25538  mbfi1fseqlem6  25649  itg2mulc  25676  itg2monolem1  25679  itg2monolem3  25681  dveflem  25911  mvth  25925  dvlipcn  25927  lhop1lem  25946  dvfsumlem1  25960  dvfsumlem2  25961  dvfsumlem2OLD  25962  dvfsumlem3  25963  dvfsumlem4  25964  dvfsum2  25969  fta1glem2  26102  plyeq0lem  26143  fta1lem  26243  vieta1lem2  26247  aalioulem3  26270  aalioulem4  26271  radcnvlem1  26350  radcnvlem2  26351  dvradcnv  26358  abelthlem2  26370  abelthlem5  26373  abelthlem7  26376  abelth2  26380  cos02pilt1  26463  cosne0  26466  rplogcl  26541  logdivlti  26557  logno1  26573  dvlog2lem  26589  advlog  26591  logtayllem  26596  cxplt  26631  cxple  26632  cxpaddlelem  26689  cxpaddle  26690  rtprmirr  26698  relogbf  26729  logbgt0b  26731  isosctrlem1  26756  isosctrlem2  26757  chordthmlem4  26773  heron  26776  atanlogaddlem  26851  bndatandm  26867  leibpi  26880  log2tlbnd  26883  birthdaylem3  26891  rlimcnp  26903  rlimcnp2  26904  efrlim  26907  efrlimOLD  26908  cxp2limlem  26914  cxp2lim  26915  divsqrtsumo1  26922  jensenlem2  26926  logdiflbnd  26933  fsumharmonic  26950  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamcvg2  26993  regamcl  26999  wilthlem2  27007  ftalem2  27012  basellem9  27027  vma1  27104  ppieq0  27114  mumullem2  27118  fsumfldivdiaglem  27127  chpeq0  27147  chtub  27151  chpval2  27157  chpchtsum  27158  chpub  27159  logfacrlim  27163  logexprlim  27164  mersenne  27166  perfectlem2  27169  dchrelbas4  27182  bcmono  27216  bposlem1  27223  bposlem2  27224  zabsle1  27235  lgslem3  27238  lgsmod  27262  lgsdir2lem4  27267  lgsdirprm  27270  gausslemma2dlem1a  27304  gausslemma2d  27313  lgsquadlem2  27320  2sqlem8  27365  chebbnd1lem1  27408  chebbnd1lem2  27409  chtppilimlem1  27412  chebbnd2  27416  chto1lb  27417  chpchtlim  27418  chpo1ubb  27420  vmadivsum  27421  rplogsumlem1  27423  rpvmasumlem  27426  dchrisumlem3  27430  dchrmusumlema  27432  dchrmusum2  27433  dchrvmasumlem2  27437  dchrvmasumlem3  27438  dchrvmasumiflem1  27440  dchrvmasumiflem2  27441  dchrisum0flblem1  27447  dchrisum0flblem2  27448  dchrisum0fno1  27450  dchrisum0re  27452  dchrisum0lema  27453  dchrisum0lem1b  27454  dchrisum0lem2a  27456  dchrisum0lem2  27457  dchrisum0lem3  27458  rplogsum  27466  dirith2  27467  mudivsum  27469  mulogsumlem  27470  mulogsum  27471  mulog2sumlem1  27473  mulog2sumlem2  27474  vmalogdivsum2  27477  vmalogdivsum  27478  2vmadivsumlem  27479  log2sumbnd  27483  selberglem2  27485  selberg2lem  27489  chpdifbnd  27494  selberg3lem1  27496  selberg3  27498  selberg4lem1  27499  selberg4  27500  pntrmax  27503  pntrsumo1  27504  pntrsumbnd  27505  selberg3r  27508  selberg4r  27509  selberg34r  27510  pntrlog2bndlem1  27516  pntrlog2bndlem2  27517  pntrlog2bndlem3  27518  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntrlog2bndlem6  27522  pntrlog2bnd  27523  pntpbnd1a  27524  pntpbnd1  27525  pntibndlem2a  27529  pntibndlem2  27530  pntibnd  27532  pntlemc  27534  pntlemg  27537  pntlemr  27541  pntlemk  27545  pnt  27553  qabvle  27564  ostth2lem3  27574  ostth2  27576  trgcgrg  28494  tgcgr4  28510  ttgcontlem1  28864  axpaschlem  28920  axlowdimlem16  28937  axcontlem2  28945  axcontlem7  28950  nbusgrvtxm1  29359  upgrewlkle2  29587  pthdlem1  29746  crctcshwlkn0lem3  29792  crctcshwlkn0lem5  29794  wwlksm1edg  29861  wwlksnextproplem2  29890  clwlkclwwlklem2fv1  29977  clwlkclwwlklem2fv2  29978  clwlkclwwlklem2  29982  clwlkclwwlk2  29985  clwwisshclwwslem  29996  clwwlkf1  30031  clwwlkext2edg  30038  clwlknf1oclwwlknlem1  30063  clwwlknonex2lem2  30090  numclwwlk7  30373  frgrreggt1  30375  frgrogt3nreg  30379  smcnlem  30679  nmoub3i  30755  blocnilem  30786  ubthlem2  30853  minvecolem4  30862  htthlem  30899  nmcexi  32008  nmopcoi  32077  stadd3i  32230  cdj1i  32415  nnmulge  32726  receqid  32732  nndiffz1  32773  fzsplit3  32780  nexple  32832  indf1o  32852  wrdt2ind  32941  pmtrto1cl  33075  fzto1st1  33078  fzto1st  33079  psgnfzto1st  33081  cycpmco2lem6  33107  cycpmco2lem7  33108  cycpmrn  33119  qsidomlem1  33424  krull  33451  ply1degltel  33562  ply1degltlss  33564  constrnegcl  33797  constrdircl  33799  iconstr  33800  constrrecl  33803  constrmulcl  33805  constrreinvcl  33806  constrresqrtcl  33811  cos9thpiminplylem1  33816  cos9thpiminply  33822  cos9thpinconstrlem1  33823  1smat1  33838  submateqlem1  33841  madjusmdetlem2  33862  unitdivcld  33935  sqsscirc1  33942  esumdivc  34117  dya2ub  34304  dya2iocress  34308  dya2iocbrsiga  34309  dya2icobrsiga  34310  dya2icoseg  34311  dya2iocucvr  34318  sxbrsigalem2  34320  fibp1  34435  probmeasb  34464  dstrvprob  34506  dstfrvunirn  34509  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemsgt1  34545  ballotlemsel1i  34547  ballotlemfrcn0  34564  signsply0  34585  itgexpif  34640  reprlt  34653  chtvalz  34663  breprexplemc  34666  breprexp  34667  circlemeth  34674  tgoldbachgnn  34693  acycgr1v  35214  subfaclim  35253  cvmliftlem2  35351  cvmliftlem13  35361  snmlff  35394  bccolsum  35804  faclim  35811  nn0prpwlem  36387  dnibndlem10  36552  dnibndlem12  36554  knoppcnlem4  36561  unblimceq0  36572  knoppndvlem1  36577  knoppndvlem2  36578  knoppndvlem3  36579  knoppndvlem7  36583  knoppndvlem11  36587  knoppndvlem12  36588  knoppndvlem14  36590  knoppndvlem15  36591  knoppndvlem17  36593  knoppndvlem18  36594  knoppndvlem20  36596  irrdiff  37391  poimirlem6  37687  poimirlem7  37688  poimirlem15  37696  poimirlem19  37700  poimirlem29  37710  poimirlem30  37711  poimirlem31  37712  poimirlem32  37713  broucube  37715  itg2addnclem2  37733  itg2addnclem3  37734  areacirclem1  37769  areacirclem4  37772  incsequz  37809  totbndbnd  37850  bfplem2  37884  resdvopclptsd  42142  lcmineqlem2  42144  lcmineqlem3  42145  lcmineqlem10  42152  lcmineqlem12  42154  lcmineqlem15  42157  lcmineqlem18  42160  lcmineqlem19  42161  lcmineqlem20  42162  lcmineqlem22  42164  lcmineqlem23  42165  3lexlogpow5ineq2  42169  3lexlogpow5ineq4  42170  3lexlogpow5ineq3  42171  3lexlogpow2ineq1  42172  3lexlogpow2ineq2  42173  3lexlogpow5ineq5  42174  aks4d1lem1  42176  dvrelog2  42178  dvrelog3  42179  dvrelog2b  42180  dvrelogpow2b  42182  aks4d1p1p3  42183  aks4d1p1p2  42184  aks4d1p1p4  42185  aks4d1p1p6  42187  aks4d1p1p7  42188  aks4d1p1p5  42189  aks4d1p1  42190  aks4d1p2  42191  aks4d1p3  42192  aks4d1p5  42194  aks4d1p6  42195  aks4d1p7d1  42196  aks4d1p7  42197  aks4d1p8d2  42199  aks4d1p8d3  42200  aks4d1p8  42201  aks4d1p9  42202  posbezout  42214  primrootlekpowne0  42219  primrootspoweq0  42220  aks6d1c1  42230  aks6d1c2p2  42233  hashscontpow1  42235  aks6d1c3  42237  aks6d1c2lem4  42241  aks6d1c2  42244  2np3bcnp1  42258  2ap1caineq  42259  sticksstones6  42265  sticksstones7  42266  sticksstones10  42269  sticksstones12a  42271  sticksstones12  42272  sticksstones22  42282  aks6d1c6lem3  42286  aks6d1c6lem4  42287  bcled  42292  bcle2d  42293  aks6d1c7lem1  42294  aks6d1c7lem2  42295  unitscyglem2  42310  unitscyglem4  42312  unitscyglem5  42313  aks5lem8  42315  sn-1ne2  42384  redvmptabs  42479  sn-00idlem2  42518  sn-0ne2  42525  rei4  42543  sn-rereccld  42567  rerecid  42568  sn-0tie0  42570  sn-nnne0  42579  mulgt0b1d  42591  sn-ltmulgt11d  42593  sn-0lt1  42594  sn-mulgt1d  42598  fimgmcyc  42653  flt4lem7  42778  fltnlta  42782  3cubeslem1  42802  3cubeslem3r  42805  3cubeslem4  42807  lzenom  42888  irrapxlem1  42940  irrapxlem2  42941  irrapxlem4  42943  irrapxlem5  42944  pellexlem2  42948  pell1qrge1  42988  pell1qr1  42989  elpell1qr2  42990  pell14qrgapw  42994  pellfundgt1  43001  pellfundglb  43003  pellfundex  43004  pellfundrp  43006  pellfundne1  43007  rmspecsqrtnq  43024  rmspecnonsq  43025  rmspecfund  43027  rmspecpos  43034  monotoddzzfi  43060  rmygeid  43082  areaquad  43334  imo72b2lem0  44283  imo72b2lem1  44287  imo72b2  44290  cvgdvgrat  44431  radcnvrat  44432  hashnzfzclim  44440  lhe4.4ex1a  44447  binomcxplemnn0  44467  binomcxplemdvbinom  44471  binomcxplemnotnn0  44474  oddfl  45404  abscosbd  45405  zltlesub  45411  abssinbd  45421  monoords  45423  fzisoeu  45426  fzdifsuc2  45436  suplesup  45463  xralrple2  45478  infxr  45490  infleinflem2  45494  reclt0d  45510  xrralrecnnge  45513  sqrlearg  45678  iooiinioc  45681  fmul01  45705  fmul01lt1lem1  45709  fmul01lt1lem2  45710  climsuselem1  45732  sumnnodd  45755  0ellimcdiv  45772  dvmptidg  46040  dvcosax  46049  ioodvbdlimc1lem1  46054  ioodvbdlimc1lem2  46055  ioodvbdlimc2lem  46057  dvxpaek  46063  dvnmul  46066  iblspltprt  46096  itgspltprt  46102  stoweidlem5  46128  stoweidlem7  46130  stoweidlem10  46133  stoweidlem11  46134  stoweidlem12  46135  stoweidlem13  46136  stoweidlem14  46137  stoweidlem16  46139  stoweidlem18  46141  stoweidlem20  46143  stoweidlem24  46147  stoweidlem25  46148  stoweidlem34  46157  stoweidlem36  46159  stoweidlem38  46161  stoweidlem40  46163  stoweidlem41  46164  stoweidlem42  46165  stoweidlem45  46168  stoweidlem51  46174  stoweidlem60  46183  wallispilem3  46190  wallispilem4  46191  wallispilem5  46192  wallispi  46193  wallispi2lem1  46194  wallispi2lem2  46195  wallispi2  46196  stirlinglem1  46197  stirlinglem3  46199  stirlinglem5  46201  stirlinglem6  46202  stirlinglem7  46203  stirlinglem8  46204  stirlinglem10  46206  stirlinglem11  46207  stirlinglem12  46208  stirlinglem13  46209  stirlinglem15  46211  dirker2re  46215  dirkerval2  46217  dirkerre  46218  dirkertrigeqlem1  46221  dirkertrigeqlem3  46223  dirkeritg  46225  dirkercncflem1  46226  dirkercncflem2  46227  dirkercncflem4  46229  fourierdlem5  46235  fourierdlem6  46236  fourierdlem11  46241  fourierdlem15  46245  fourierdlem19  46249  fourierdlem20  46250  fourierdlem24  46254  fourierdlem26  46256  fourierdlem28  46258  fourierdlem30  46260  fourierdlem39  46269  fourierdlem41  46271  fourierdlem43  46273  fourierdlem47  46276  fourierdlem48  46277  fourierdlem56  46285  fourierdlem60  46289  fourierdlem61  46290  fourierdlem62  46291  fourierdlem64  46293  fourierdlem65  46294  fourierdlem66  46295  fourierdlem68  46297  fourierdlem73  46302  fourierdlem78  46307  fourierdlem79  46308  fourierdlem87  46316  fourierdlem103  46332  fourierdlem104  46333  sqwvfoura  46351  fouriersw  46354  etransclem4  46361  etransclem23  46380  etransclem24  46381  etransclem31  46388  etransclem32  46389  etransclem35  46392  etransclem41  46398  etransclem46  46403  etransclem48  46405  etransc  46406  ioorrnopnxrlem  46429  nnfoctbdjlem  46578  iundjiun  46583  hoidmvlelem1  46718  hoidmvlelem2  46719  hoidmvlelem3  46720  hoidmvlelem4  46721  ovnhoilem1  46724  vonioolem2  46804  vonicclem2  46807  pimrecltneg  46847  smfrec  46912  smfmullem1  46914  smfmullem2  46915  smfdiv  46920  sigaradd  46989  ormkglobd  46998  cjnpoly  47014  p1lep2  47425  zm1nn  47427  ceilhalfgt1  47454  2tceilhalfelfzo1  47457  ceilbi  47458  rehalfge1  47460  ceilhalfnn  47461  addmodne  47469  m1mod0mod1  47479  m1modmmod  47483  difmodm1lt  47484  modmknepk  47487  modp2nep1  47492  modm1nem2  47494  iccpartiltu  47547  iccpartlt  47549  iccpartgt  47552  fmtnoge3  47655  fmtnodvds  47669  fmtnoprmfac2lem1  47691  2pwp1prm  47714  flsqrt  47718  sfprmdvdsmersenne  47728  lighneallem2  47731  lighneallem4a  47733  proththdlem  47738  proththd  47739  nnoALTV  47820  bgoldbtbndlem4  47933  gpgprismgrusgra  48183  gpgedgvtx0  48186  gpgvtxedg0  48188  gpg5nbgrvtx03starlem2  48194  gpg3kgrtriexlem4  48211  gpg3kgrtriexlem6  48213  cznnring  48387  divge1b  48638  divgt1b  48639  nn0eo  48654  regt1loggt0  48662  rege1logbrege0  48684  logblt1b  48690  fllog2  48694  nnolog2flm1  48716  dignn0flhalflem1  48741  rrxlinesc  48861  rrxlinec  48862  eenglngeehlnmlem1  48863  eenglngeehlnmlem2  48864  line2ylem  48877  line2  48878  line2xlem  48879  reseccl  49879  recsccl  49880  amgmwlem  49928  amgmlemALT  49929