Theorem 1red 11212

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11106  1c1 11108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-mulcl 11169  ax-mulrcl 11170  ax-i2m1 11175  ax-1ne0 11176  ax-rrecex 11179  ax-cnre 11180

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409

This theorem is referenced by:  recgt0  12057  ltrec  12093  nnne0  12243  nn0p1gt0  12498  nn0ge2m1nn  12538  nn0le2is012  12623  suprzcl  12639  ledivge1le  13042  qbtwnre  13175  lincmb01cmp  13469  iccf1o  13470  xov1plusxeqvd  13472  zltaddlt1le  13479  fznatpl1  13552  elfz1b  13567  fzonn0p1p1  13708  elfznelfzo  13734  elfznelfzob  13735  fladdz  13787  2tnp1ge0ge0  13791  flhalf  13792  ltdifltdiv  13796  fldiv4lem1div2uz2  13798  mulp1mod1  13874  m1modge3gt1  13880  modltm1p1mod  13885  addmodlteq  13908  ltexp2a  14128  expcan  14131  ltexp2  14132  leexp2  14133  leexp2a  14134  leexp2r  14136  nnlesq  14166  bernneq3  14191  expnbnd  14192  expnlbnd2  14194  expnngt1  14201  fzsdom2  14385  wrdlenge2n0  14499  swrd2lsw  14900  2swrd2eqwrdeq  14901  01sqrexlem7  15192  rddif  15284  reccn2  15538  rlimo1  15558  o1fsum  15756  abscvgcvg  15762  climcndslem1  15792  flo1  15797  harmonic  15802  geomulcvg  15819  fprodrecl  15894  fprodreclf  15900  fprodle  15937  bpoly4  16000  efcllem  16018  efgt1  16056  tanhlt1  16100  sinltx  16129  eirrlem  16144  p1modz1  16201  mod2eq1n2dvds  16287  oddge22np1  16289  ltoddhalfle  16301  nn0o1gt2  16321  nno  16322  nn0oddm1d2  16325  nnoddm1d2  16326  bitsfzolem  16372  bitsfzo  16373  bitsmod  16374  bitscmp  16376  bitsinv1lem  16379  smuval2  16420  coprmgcdb  16583  prmind2  16619  dvdsnprmd  16624  2mulprm  16627  isprm5  16641  isprm7  16642  divdenle  16682  zsqrtelqelz  16691  fermltl  16714  odzdvds  16725  modprm0  16735  iserodd  16765  difsqpwdvds  16817  pcfaclem  16828  prmreclem1  16846  4sqlem11  16885  4sqlem12  16886  ramub1lem1  16956  prmgaplem8  16988  2expltfac  17023  pgpfaclem2  19947  znidomb  21109  chfacfisf  22348  chfacfisfcpmat  22349  chfacfscmulgsum  22354  chfacfpmmulgsum  22358  nrginvrcnlem  24200  nmoid  24251  xrsmopn  24320  metnrmlem1a  24366  iccpnfhmeo  24453  lebnumii  24474  htpycc  24488  pcohtpylem  24527  pcoass  24532  pcorevlem  24534  nmhmcn  24628  cncmet  24831  ovoliunlem1  25011  dyadmaxlem  25106  vitalilem2  25118  mbfi1fseqlem6  25230  itg2mulc  25257  itg2monolem1  25260  itg2monolem3  25262  dveflem  25488  mvth  25501  dvlipcn  25503  lhop1lem  25522  dvfsumlem1  25535  dvfsumlem2  25536  dvfsumlem3  25537  dvfsumlem4  25538  dvfsum2  25543  fta1glem2  25676  plyeq0lem  25716  fta1lem  25812  vieta1lem2  25816  aalioulem3  25839  aalioulem4  25840  radcnvlem1  25917  radcnvlem2  25918  dvradcnv  25925  abelthlem2  25936  abelthlem5  25939  abelthlem7  25942  abelth2  25946  cos02pilt1  26027  cosne0  26030  rplogcl  26104  logdivlti  26120  logno1  26136  dvlog2lem  26152  advlog  26154  logtayllem  26159  cxplt  26194  cxple  26195  cxpaddlelem  26249  cxpaddle  26250  relogbf  26286  logbgt0b  26288  isosctrlem1  26313  isosctrlem2  26314  chordthmlem4  26330  heron  26333  atanlogaddlem  26408  bndatandm  26424  leibpi  26437  log2tlbnd  26440  birthdaylem3  26448  rlimcnp  26460  rlimcnp2  26461  efrlim  26464  cxp2limlem  26470  cxp2lim  26471  divsqrtsumo1  26478  jensenlem2  26482  logdiflbnd  26489  fsumharmonic  26506  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem4  26526  lgamgulmlem5  26527  lgamgulmlem6  26528  lgamcvg2  26549  regamcl  26555  wilthlem2  26563  ftalem2  26568  basellem9  26583  vma1  26660  ppieq0  26670  mumullem2  26674  fsumfldivdiaglem  26683  chpeq0  26701  chtub  26705  chpval2  26711  chpchtsum  26712  chpub  26713  logfacrlim  26717  logexprlim  26718  mersenne  26720  perfectlem2  26723  dchrelbas4  26736  bcmono  26770  bposlem1  26777  bposlem2  26778  zabsle1  26789  lgslem3  26792  lgsmod  26816  lgsdir2lem4  26821  lgsdirprm  26824  gausslemma2dlem1a  26858  gausslemma2d  26867  lgsquadlem2  26874  2sqlem8  26919  chebbnd1lem1  26962  chebbnd1lem2  26963  chtppilimlem1  26966  chebbnd2  26970  chto1lb  26971  chpchtlim  26972  chpo1ubb  26974  vmadivsum  26975  rplogsumlem1  26977  rpvmasumlem  26980  dchrisumlem3  26984  dchrmusumlema  26986  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumlem3  26992  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  dchrisum0flblem1  27001  dchrisum0flblem2  27002  dchrisum0fno1  27004  dchrisum0re  27006  dchrisum0lema  27007  dchrisum0lem1b  27008  dchrisum0lem2a  27010  dchrisum0lem2  27011  dchrisum0lem3  27012  rplogsum  27020  dirith2  27021  mudivsum  27023  mulogsumlem  27024  mulogsum  27025  mulog2sumlem1  27027  mulog2sumlem2  27028  vmalogdivsum2  27031  vmalogdivsum  27032  2vmadivsumlem  27033  log2sumbnd  27037  selberglem2  27039  selberg2lem  27043  chpdifbnd  27048  selberg3lem1  27050  selberg3  27052  selberg4lem1  27053  selberg4  27054  pntrmax  27057  pntrsumo1  27058  pntrsumbnd  27059  selberg3r  27062  selberg4r  27063  selberg34r  27064  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntrlog2bnd  27077  pntpbnd1a  27078  pntpbnd1  27079  pntibndlem2a  27083  pntibndlem2  27084  pntibnd  27086  pntlemc  27088  pntlemg  27091  pntlemr  27095  pntlemk  27099  pnt  27107  qabvle  27118  ostth2lem3  27128  ostth2  27130  trgcgrg  27756  tgcgr4  27772  ttgcontlem1  28132  axpaschlem  28188  axlowdimlem16  28205  axcontlem2  28213  axcontlem7  28218  nbusgrvtxm1  28626  upgrewlkle2  28853  pthdlem1  29013  crctcshwlkn0lem3  29056  crctcshwlkn0lem5  29058  wwlksm1edg  29125  wwlksnextproplem2  29154  clwlkclwwlklem2fv1  29238  clwlkclwwlklem2fv2  29239  clwlkclwwlklem2  29243  clwlkclwwlk2  29246  clwwisshclwwslem  29257  clwwlkf1  29292  clwwlkext2edg  29299  clwlknf1oclwwlknlem1  29324  clwwlknonex2lem2  29351  numclwwlk7  29634  frgrreggt1  29636  frgrogt3nreg  29640  smcnlem  29938  nmoub3i  30014  blocnilem  30045  ubthlem2  30112  minvecolem4  30121  htthlem  30158  nmcexi  31267  nmopcoi  31336  stadd3i  31489  cdj1i  31674  nnmulge  31951  nndiffz1  31985  fzsplit3  31993  wrdt2ind  32105  pmtrto1cl  32246  fzto1st1  32249  fzto1st  32250  psgnfzto1st  32252  cycpmco2lem6  32278  cycpmco2lem7  32279  cycpmrn  32290  qsidomlem1  32560  krull  32583  ply1degltel  32655  ply1degltlss  32656  1smat1  32773  submateqlem1  32776  madjusmdetlem2  32797  unitdivcld  32870  sqsscirc1  32877  nexple  32996  indf1o  33011  esumdivc  33070  dya2ub  33258  dya2iocress  33262  dya2iocbrsiga  33263  dya2icobrsiga  33264  dya2icoseg  33265  dya2iocucvr  33272  sxbrsigalem2  33274  fibp1  33389  probmeasb  33418  dstrvprob  33459  dstfrvunirn  33462  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemsgt1  33498  ballotlemsel1i  33500  ballotlemfrcn0  33517  signsply0  33551  itgexpif  33607  reprlt  33620  chtvalz  33630  breprexplemc  33633  breprexp  33634  circlemeth  33641  tgoldbachgnn  33660  acycgr1v  34129  subfaclim  34168  cvmliftlem2  34266  cvmliftlem13  34276  snmlff  34309  bccolsum  34698  faclim  34705  gg-dvfsumlem2  35172  nn0prpwlem  35196  dnibndlem10  35352  dnibndlem12  35354  knoppcnlem4  35361  unblimceq0  35372  knoppndvlem1  35377  knoppndvlem2  35378  knoppndvlem3  35379  knoppndvlem7  35383  knoppndvlem11  35387  knoppndvlem12  35388  knoppndvlem14  35390  knoppndvlem15  35391  knoppndvlem17  35393  knoppndvlem18  35394  knoppndvlem20  35396  irrdiff  36196  poimirlem6  36483  poimirlem7  36484  poimirlem15  36492  poimirlem19  36496  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimirlem32  36509  broucube  36511  itg2addnclem2  36529  itg2addnclem3  36530  areacirclem1  36565  areacirclem4  36568  incsequz  36605  totbndbnd  36646  bfplem2  36680  resdvopclptsd  40882  lcmineqlem2  40884  lcmineqlem3  40885  lcmineqlem10  40892  lcmineqlem12  40894  lcmineqlem15  40897  lcmineqlem18  40900  lcmineqlem19  40901  lcmineqlem20  40902  lcmineqlem22  40904  lcmineqlem23  40905  3lexlogpow5ineq2  40909  3lexlogpow5ineq4  40910  3lexlogpow5ineq3  40911  3lexlogpow2ineq1  40912  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1lem1  40916  dvrelog2  40918  dvrelog3  40919  dvrelog2b  40920  dvrelogpow2b  40922  aks4d1p1p3  40923  aks4d1p1p2  40924  aks4d1p1p4  40925  aks4d1p1p6  40927  aks4d1p1p7  40928  aks4d1p1p5  40929  aks4d1p1  40930  aks4d1p2  40931  aks4d1p3  40932  aks4d1p5  40934  aks4d1p6  40935  aks4d1p7d1  40936  aks4d1p7  40937  aks4d1p8d2  40939  aks4d1p8d3  40940  aks4d1p8  40941  aks4d1p9  40942  aks6d1c2p2  40946  2np3bcnp1  40949  2ap1caineq  40950  sticksstones6  40956  sticksstones7  40957  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  sticksstones22  40973  metakunt1  40974  metakunt2  40975  metakunt7  40980  metakunt15  40988  metakunt16  40989  metakunt24  40997  metakunt28  41001  metakunt29  41002  2xp3dxp2ge1d  41011  factwoffsmonot  41012  sn-1ne2  41177  rtprmirr  41234  sn-00idlem2  41269  sn-0ne2  41276  rei4  41293  sn-0tie0  41309  sn-nnne0  41318  mulgt0b2d  41330  sn-0lt1  41332  flt4lem7  41398  fltnlta  41402  3cubeslem1  41408  3cubeslem3r  41411  3cubeslem4  41413  lzenom  41494  irrapxlem1  41546  irrapxlem2  41547  irrapxlem4  41549  irrapxlem5  41550  pellexlem2  41554  pell1qrge1  41594  pell1qr1  41595  elpell1qr2  41596  pell14qrgapw  41600  pellfundgt1  41607  pellfundglb  41609  pellfundex  41610  pellfundrp  41612  pellfundne1  41613  rmspecsqrtnq  41630  rmspecnonsq  41631  rmspecfund  41633  rmspecpos  41641  monotoddzzfi  41667  rmygeid  41689  areaquad  41951  imo72b2lem0  42903  imo72b2lem1  42907  imo72b2  42910  cvgdvgrat  43058  radcnvrat  43059  hashnzfzclim  43067  lhe4.4ex1a  43074  binomcxplemnn0  43094  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  oddfl  43974  abscosbd  43975  zltlesub  43982  abssinbd  43992  monoords  43994  fzisoeu  43997  fzdifsuc2  44007  suplesup  44036  xralrple2  44051  infxr  44064  infleinflem2  44068  reclt0d  44084  xrralrecnnge  44087  sqrlearg  44253  iooiinioc  44256  fmul01  44283  fmul01lt1lem1  44287  fmul01lt1lem2  44288  climsuselem1  44310  sumnnodd  44333  0ellimcdiv  44352  dvmptidg  44620  dvcosax  44629  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvxpaek  44643  dvnmul  44646  iblspltprt  44676  itgspltprt  44682  stoweidlem5  44708  stoweidlem7  44710  stoweidlem10  44713  stoweidlem11  44714  stoweidlem12  44715  stoweidlem13  44716  stoweidlem14  44717  stoweidlem16  44719  stoweidlem18  44721  stoweidlem20  44723  stoweidlem24  44727  stoweidlem25  44728  stoweidlem34  44737  stoweidlem36  44739  stoweidlem38  44741  stoweidlem40  44743  stoweidlem41  44744  stoweidlem42  44745  stoweidlem45  44748  stoweidlem51  44754  stoweidlem60  44763  wallispilem3  44770  wallispilem4  44771  wallispilem5  44772  wallispi  44773  wallispi2lem1  44774  wallispi2lem2  44775  wallispi2  44776  stirlinglem1  44777  stirlinglem3  44779  stirlinglem5  44781  stirlinglem6  44782  stirlinglem7  44783  stirlinglem8  44784  stirlinglem10  44786  stirlinglem11  44787  stirlinglem12  44788  stirlinglem13  44789  stirlinglem15  44791  dirker2re  44795  dirkerval2  44797  dirkerre  44798  dirkertrigeqlem1  44801  dirkertrigeqlem3  44803  dirkeritg  44805  dirkercncflem1  44806  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem5  44815  fourierdlem6  44816  fourierdlem11  44821  fourierdlem15  44825  fourierdlem19  44829  fourierdlem20  44830  fourierdlem24  44834  fourierdlem26  44836  fourierdlem28  44838  fourierdlem30  44840  fourierdlem39  44849  fourierdlem41  44851  fourierdlem43  44853  fourierdlem47  44856  fourierdlem48  44857  fourierdlem56  44865  fourierdlem60  44869  fourierdlem61  44870  fourierdlem62  44871  fourierdlem64  44873  fourierdlem65  44874  fourierdlem66  44875  fourierdlem68  44877  fourierdlem73  44882  fourierdlem78  44887  fourierdlem79  44888  fourierdlem87  44896  fourierdlem103  44912  fourierdlem104  44913  sqwvfoura  44931  fouriersw  44934  etransclem4  44941  etransclem23  44960  etransclem24  44961  etransclem31  44968  etransclem32  44969  etransclem35  44972  etransclem41  44978  etransclem46  44983  etransclem48  44985  etransc  44986  ioorrnopnxrlem  45009  nnfoctbdjlem  45158  iundjiun  45163  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  ovnhoilem1  45304  vonioolem2  45384  vonicclem2  45387  pimrecltneg  45427  smfrec  45492  smfmullem1  45494  smfmullem2  45495  smfdiv  45500  sigaradd  45569  p1lep2  45995  zm1nn  45997  m1mod0mod1  46024  iccpartiltu  46077  iccpartlt  46079  iccpartgt  46082  fmtnoge3  46185  fmtnodvds  46199  fmtnoprmfac2lem1  46221  2pwp1prm  46244  flsqrt  46248  sfprmdvdsmersenne  46258  lighneallem2  46261  lighneallem4a  46263  proththdlem  46268  proththd  46269  nnoALTV  46350  bgoldbtbndlem4  46463  cznnring  46808  divge1b  47147  divgt1b  47148  m1modmmod  47161  difmodm1lt  47162  nn0eo  47168  regt1loggt0  47176  rege1logbrege0  47198  logblt1b  47204  fllog2  47208  nnolog2flm1  47230  dignn0flhalflem1  47255  rrxlinesc  47375  rrxlinec  47376  eenglngeehlnmlem1  47377  eenglngeehlnmlem2  47378  line2ylem  47391  line2  47392  line2xlem  47393  reseccl  47752  recsccl  47753  amgmwlem  47803  amgmlemALT  47804