Theorem 1red 11236

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11126  1c1 11128

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417

This theorem is used by:  recgt0  12088  mulgt1  12103  ltrec  12124  nnne0  12297  nn0p1gt0  12560  nn0ge2m1nn  12601  nn0le2is012  12688  suprzcl  12704  ledivge1le  13118  ge2halflem1  13162  qbtwnre  13254  lincmb01cmp  13551  iccf1o  13552  xov1plusxeqvd  13554  zltaddlt1le  13561  nnge2recico01  13563  fznatpl1  13636  elfz1b  13651  elfzo0subge1  13764  fzonn0p1p1  13803  elfznelfzo  13832  elfznelfzob  13833  fladdz  13889  2tnp1ge0ge0  13893  flhalf  13894  ltdifltdiv  13898  fldiv4lem1div2uz2  13900  mulp1mod1  13978  m1modge3gt1  13985  modltm1p1mod  13990  addmodlteq  14013  ltexp2a  14233  expcan  14236  ltexp2  14237  leexp2  14238  leexp2a  14239  leexp2r  14241  nnlesq  14272  bernneq3  14298  expnbnd  14299  expnlbnd2  14301  expnngt1  14308  fzsdom2  14496  wrdlenge2n0  14620  swrd2lsw  15028  2swrd2eqwrdeq  15029  01sqrexlem7  15338  rddif  15431  reccn2  15687  rlimo1  15707  o1fsum  15903  abscvgcvg  15909  climcndslem1  15941  flo1  15946  harmonic  15951  geomulcvg  15968  fprodrecl  16043  fprodreclf  16049  fprodle  16086  bpoly4  16148  efcllem  16166  efgt1  16207  tanhlt1  16251  sinltx  16280  eirrlem  16295  p1modz1  16352  mod2eq1n2dvds  16440  oddge22np1  16442  ltoddhalfle  16454  nn0o1gt2  16474  nno  16475  nn0oddm1d2  16478  nnoddm1d2  16479  bitsfzolem  16527  bitsfzo  16528  bitsmod  16529  bitscmp  16531  bitsinv1lem  16534  smuval2  16575  coprmgcdb  16742  prmind2  16778  dvdsnprmd  16783  2mulprm  16786  isprm5  16801  isprm7  16802  divdenle  16843  zsqrtelqelz  16852  fermltl  16878  odzdvds  16890  modprm0  16900  iserodd  16930  difsqpwdvds  16982  pcfaclem  16993  prmreclem1  17011  4sqlem11  17050  4sqlem12  17051  ramub1lem1  17121  prmgaplem8  17153  2expltfac  17187  chnccat  18717  pgpfaclem2  20214  qsidomlem1  21546  znidomb  21777  psdmvr  22400  chfacfisf  23082  chfacfisfcpmat  23083  chfacfscmulgsum  23088  chfacfpmmulgsum  23092  nrginvrcnlem  24920  nmoid  24971  xrsmopn  25042  metnrmlem1a  25088  iihalf2cn  25165  iccpnfhmeo  25176  lebnumii  25197  htpycc  25211  pcohtpylem  25250  pcoass  25255  pcorevlem  25257  nmhmcn  25351  cncmet  25553  ovoliunlem1  25733  dyadmaxlem  25828  vitalilem2  25840  mbfi1fseqlem6  25951  itg2mulc  25978  itg2monolem1  25981  itg2monolem3  25983  dveflem  26209  mvth  26222  dvlipcn  26224  lhop1lem  26243  dvfsumlem1  26256  dvfsumlem2  26257  dvfsumlem3  26258  dvfsumlem4  26259  dvfsum2  26264  fta1glem2  26397  plyeq0lem  26439  fta1lem  26540  vieta1lem2  26546  aalioulem3  26573  aalioulem4  26574  radcnvlem1  26652  radcnvlem2  26653  dvradcnv  26660  abelthlem2  26671  abelthlem5  26674  abelthlem7  26677  abelth2  26681  cos02pilt1  26766  cosne0  26769  rplogcl  26844  logdivlti  26860  logno1  26876  dvlog2lem  26892  advlog  26894  logtayllem  26899  cxplt  26934  cxple  26935  cxpaddlelem  26991  cxpaddle  26992  rtprmirr  27000  relogbf  27031  logbgt0b  27033  isosctrlem1  27058  isosctrlem2  27059  chordthmlem4  27075  heron  27078  atanlogaddlem  27153  bndatandm  27169  leibpi  27182  log2tlbnd  27185  birthdaylem3  27193  rlimcnp  27205  rlimcnp2  27206  efrlim  27209  cxp2limlem  27215  cxp2lim  27216  divsqrtsumo1  27223  jensenlem2  27227  logdiflbnd  27234  fsumharmonic  27251  lgamgulmlem2  27269  lgamgulmlem3  27270  lgamgulmlem4  27271  lgamgulmlem5  27272  lgamgulmlem6  27273  lgamcvg2  27294  regamcl  27300  wilthlem2  27308  ftalem2  27313  basellem9  27328  vma1  27405  ppieq0  27415  mumullem2  27419  fsumfldivdiaglem  27428  ppiub  27443  chpeq0  27447  chtub  27451  chpval2  27457  chpchtsum  27458  chpub  27459  logfacrlim  27463  logexprlim  27464  mersenne  27466  perfectlem2  27469  dchrelbas4  27482  bcmono  27516  bposlem1  27523  bposlem2  27524  zabsle1  27535  lgslem3  27538  lgsmod  27562  lgsdir2lem4  27567  lgsdirprm  27570  gausslemma2dlem1a  27604  gausslemma2d  27613  lgsquadlem2  27620  2sqlem8  27665  chebbnd1lem1  27708  chebbnd1lem2  27709  chtppilimlem1  27712  chebbnd2  27716  chto1lb  27717  chpchtlim  27718  chpo1ubb  27720  vmadivsum  27721  rplogsumlem1  27723  rpvmasumlem  27726  dchrisumlem3  27730  dchrmusumlema  27732  dchrmusum2  27733  dchrvmasumlem2  27737  dchrvmasumlem3  27738  dchrvmasumiflem1  27740  dchrvmasumiflem2  27741  dchrisum0flblem1  27747  dchrisum0flblem2  27748  dchrisum0fno1  27750  dchrisum0re  27752  dchrisum0lema  27753  dchrisum0lem1b  27754  dchrisum0lem2a  27756  dchrisum0lem2  27757  dchrisum0lem3  27758  rplogsum  27766  dirith2  27767  mudivsum  27769  mulogsumlem  27770  mulogsum  27771  mulog2sumlem1  27773  mulog2sumlem2  27774  vmalogdivsum2  27777  vmalogdivsum  27778  2vmadivsumlem  27779  log2sumbnd  27783  selberglem2  27785  selberg2lem  27789  chpdifbnd  27794  selberg3lem1  27796  selberg3  27798  selberg4lem1  27799  selberg4  27800  pntrmax  27803  pntrsumo1  27804  pntrsumbnd  27805  selberg3r  27808  selberg4r  27809  selberg34r  27810  pntrlog2bndlem1  27816  pntrlog2bndlem2  27817  pntrlog2bndlem3  27818  pntrlog2bndlem4  27819  pntrlog2bndlem5  27820  pntrlog2bndlem6  27822  pntrlog2bnd  27823  pntpbnd1a  27824  pntpbnd1  27825  pntibndlem2a  27829  pntibndlem2  27830  pntibnd  27832  pntlemc  27834  pntlemg  27837  pntlemr  27841  pntlemk  27845  pnt  27853  qabvle  27864  ostth2lem3  27874  ostth2  27876  trgcgrg  28860  tgcgr4  28876  ttgcontlem1  29344  axpaschlem  29400  axlowdimlem16  29417  axcontlem2  29425  axcontlem7  29430  nbusgrvtxm1  29842  upgrewlkle2  30069  pthdlem1  30234  crctcshwlkn0lem3  30283  crctcshwlkn0lem5  30285  wwlksm1edg  30352  wwlksnextproplem2  30381  clwlkclwwlklem2fv1  30468  clwlkclwwlklem2fv2  30469  clwlkclwwlklem2  30473  clwlkclwwlk2  30476  clwwisshclwwslem  30487  clwwlkf1  30522  clwwlkext2edg  30529  clwlknf1oclwwlknlem1  30554  clwwlknonex2lem2  30581  numclwwlk7  30874  frgrreggt1  30876  frgrogt3nreg  30880  smcnlem  31181  nmoub3i  31257  blocnilem  31288  ubthlem2  31355  minvecolem4  31364  htthlem  31401  nmcexi  32510  nmopcoi  32579  stadd3i  32732  cdj1i  32917  nnmulge  33213  receqid  33218  nndiffz1  33260  fzsplit3  33267  nexple  33306  indf1o  33313  wrdt2ind  33398  pmtrto1cl  33542  fzto1st1  33545  fzto1st  33546  psgnfzto1st  33548  cycpmco2lem6  33574  cycpmco2lem7  33575  cycpmrn  33586  krull  33884  ply1degltel  34007  ply1degltlss  34009  constrnegcl  34276  constrdircl  34278  iconstr  34279  constrrecl  34282  constrmulcl  34284  constrreinvcl  34285  constrresqrtcl  34290  cos9thpiminplylem1  34295  cos9thpiminply  34301  cos9thpinconstrlem1  34302  1smat1  34317  submateqlem1  34320  madjusmdetlem2  34341  unitdivcld  34414  sqsscirc1  34421  esumdivc  34596  dya2ub  34784  dya2iocress  34788  dya2iocbrsiga  34789  dya2icobrsiga  34790  dya2icoseg  34791  dya2iocucvr  34798  sxbrsigalem2  34800  fibp1  34915  probmeasb  34944  dstrvprob  34986  dstfrvunirn  34989  ballotlemfc0  35007  ballotlemfcc  35008  ballotlemsgt1  35025  ballotlemsel1i  35027  ballotlemfrcn0  35044  signsply0  35062  itgexpif  35117  reprlt  35130  chtvalz  35140  breprexplemc  35143  breprexp  35144  circlemeth  35151  tgoldbachgnn  35170  acycgr1v  35731  subfaclim  35770  cvmliftlem2  35868  cvmliftlem13  35878  snmlff  35911  bccolsum  36321  faclim  36328  nn0prpwlem  36944  dnibndlem10  37187  dnibndlem12  37189  knoppcnlem4  37196  unblimceq0  37207  knoppndvlem1  37212  knoppndvlem2  37213  knoppndvlem3  37214  knoppndvlem7  37218  knoppndvlem11  37222  knoppndvlem12  37223  knoppndvlem14  37225  knoppndvlem15  37226  knoppndvlem17  37228  knoppndvlem18  37229  knoppndvlem20  37231  irrdiff  38081  poimirlem6  38378  poimirlem7  38379  poimirlem15  38387  poimirlem19  38391  poimirlem29  38401  poimirlem30  38402  poimirlem31  38403  poimirlem32  38404  broucube  38406  itg2addnclem2  38424  itg2addnclem3  38425  areacirclem1  38460  areacirclem4  38463  incsequz  38501  totbndbnd  38542  bfplem2  38576  resdvopclptsd  42897  lcmineqlem2  42899  lcmineqlem3  42900  lcmineqlem10  42907  lcmineqlem12  42909  lcmineqlem15  42912  lcmineqlem18  42915  lcmineqlem19  42916  lcmineqlem20  42917  lcmineqlem22  42919  lcmineqlem23  42920  3lexlogpow5ineq2  42924  3lexlogpow5ineq4  42925  3lexlogpow5ineq3  42926  3lexlogpow2ineq1  42927  3lexlogpow2ineq2  42928  3lexlogpow5ineq5  42929  aks4d1lem1  42931  dvrelog2  42933  dvrelog3  42934  dvrelog2b  42935  dvrelogpow2b  42937  aks4d1p1p3  42938  aks4d1p1p2  42939  aks4d1p1p4  42940  aks4d1p1p6  42942  aks4d1p1p7  42943  aks4d1p1p5  42944  aks4d1p1  42945  aks4d1p2  42946  aks4d1p3  42947  aks4d1p5  42949  aks4d1p6  42950  aks4d1p7d1  42951  aks4d1p7  42952  aks4d1p8d2  42954  aks4d1p8d3  42955  aks4d1p8  42956  aks4d1p9  42957  posbezout  42969  primrootlekpowne0  42974  primrootspoweq0  42975  aks6d1c1  42985  aks6d1c2p2  42988  hashscontpow1  42990  aks6d1c3  42992  aks6d1c2lem4  42996  aks6d1c2  42999  2np3bcnp1  43013  2ap1caineq  43014  sticksstones6  43020  sticksstones7  43021  sticksstones10  43024  sticksstones12a  43026  sticksstones12  43027  sticksstones22  43037  aks6d1c6lem3  43041  aks6d1c6lem4  43042  bcled  43047  bcle2d  43048  aks6d1c7lem1  43049  aks6d1c7lem2  43050  unitscyglem2  43065  unitscyglem4  43067  unitscyglem5  43068  aks5lem8  43070  sn-1ne2  43149  redvmptabs  43238  sn-00idlem2  43277  sn-0ne2  43284  rei4  43302  rediveq1d  43329  sn-rediv1d  43330  sn-rereccld  43333  rerecne0d  43334  rerecidd  43335  rerecrecd  43337  sn-0tie0  43342  sn-nnne0  43351  mulgt0b1d  43363  sn-ltmulgt11d  43365  sn-0lt1  43366  sn-mulgt1d  43370  fimgmcyc  43419  flt4lem7  43508  fltnlta  43512  3cubeslem1  43532  3cubeslem3r  43535  3cubeslem4  43537  lzenom  43618  irrapxlem1  43666  irrapxlem2  43667  irrapxlem4  43669  irrapxlem5  43670  pellexlem2  43674  pell1qrge1  43714  pell1qr1  43715  elpell1qr2  43716  pell14qrgapw  43720  pellfundgt1  43727  pellfundglb  43729  pellfundex  43730  pellfundrp  43732  pellfundne1  43733  rmspecsqrtnq  43750  rmspecnonsq  43751  rmspecfund  43753  rmspecpos  43760  monotoddzzfi  43786  rmygeid  43808  areaquad  44060  imo72b2lem0  45008  imo72b2lem1  45012  imo72b2  45015  cvgdvgrat  45140  radcnvrat  45141  hashnzfzclim  45149  lhe4.4ex1a  45156  binomcxplemnn0  45176  binomcxplemdvbinom  45180  binomcxplemnotnn0  45183  oddfl  46114  abscosbd  46115  zltlesub  46121  abssinbd  46131  monoords  46133  fzisoeu  46136  fzdifsuc2  46146  suplesup  46172  xralrple2  46187  infxr  46199  infleinflem2  46203  reclt0d  46219  xrralrecnnge  46222  sqrlearg  46386  iooiinioc  46389  fmul01  46413  fmul01lt1lem1  46417  fmul01lt1lem2  46418  climsuselem1  46440  sumnnodd  46463  0ellimcdiv  46480  dvmptidg  46748  dvcosax  46757  ioodvbdlimc1lem1  46762  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  dvxpaek  46771  dvnmul  46774  iblspltprt  46804  itgspltprt  46810  stoweidlem5  46836  stoweidlem7  46838  stoweidlem10  46841  stoweidlem11  46842  stoweidlem12  46843  stoweidlem13  46844  stoweidlem14  46845  stoweidlem16  46847  stoweidlem18  46849  stoweidlem20  46851  stoweidlem24  46855  stoweidlem25  46856  stoweidlem34  46865  stoweidlem36  46867  stoweidlem38  46869  stoweidlem40  46871  stoweidlem41  46872  stoweidlem42  46873  stoweidlem45  46876  stoweidlem51  46882  stoweidlem60  46891  wallispilem3  46898  wallispilem4  46899  wallispilem5  46900  wallispi  46901  wallispi2lem1  46902  wallispi2lem2  46903  wallispi2  46904  stirlinglem1  46905  stirlinglem3  46907  stirlinglem5  46909  stirlinglem6  46910  stirlinglem7  46911  stirlinglem8  46912  stirlinglem10  46914  stirlinglem11  46915  stirlinglem12  46916  stirlinglem13  46917  stirlinglem15  46919  dirker2re  46923  dirkerval2  46925  dirkerre  46926  dirkertrigeqlem1  46929  dirkertrigeqlem3  46931  dirkeritg  46933  dirkercncflem1  46934  dirkercncflem2  46935  dirkercncflem4  46937  fourierdlem5  46943  fourierdlem6  46944  fourierdlem11  46949  fourierdlem15  46953  fourierdlem19  46957  fourierdlem20  46958  fourierdlem24  46962  fourierdlem26  46964  fourierdlem28  46966  fourierdlem30  46968  fourierdlem39  46977  fourierdlem41  46979  fourierdlem43  46981  fourierdlem47  46984  fourierdlem48  46985  fourierdlem56  46993  fourierdlem60  46997  fourierdlem61  46998  fourierdlem62  46999  fourierdlem64  47001  fourierdlem65  47002  fourierdlem66  47003  fourierdlem68  47005  fourierdlem73  47010  fourierdlem78  47015  fourierdlem79  47016  fourierdlem87  47024  fourierdlem103  47040  fourierdlem104  47041  sqwvfoura  47059  fouriersw  47062  etransclem4  47069  etransclem23  47088  etransclem24  47089  etransclem31  47096  etransclem32  47097  etransclem35  47100  etransclem41  47106  etransclem46  47111  etransclem48  47113  etransc  47114  ioorrnopnxrlem  47137  nnfoctbdjlem  47286  iundjiun  47291  hoidmvlelem1  47426  hoidmvlelem2  47427  hoidmvlelem3  47428  hoidmvlelem4  47429  ovnhoilem1  47432  vonioolem2  47512  vonicclem2  47515  pimrecltneg  47555  smfrec  47620  smfmullem1  47622  smfmullem2  47623  smfdiv  47628  sigaradd  47697  ormkglobd  47708  cjnpoly  47760  p1lep2  48191  zm1nn  48193  ceilhalfgt1  48224  2tceilhalfelfzo1  48227  ceilbi  48228  rehalfge1  48230  ceilhalfnn  48231  flmrecm1  48234  addmodne  48241  m1mod0mod1  48251  m1modmmod  48255  difmodm1lt  48256  modmknepk  48259  modp2nep1  48264  modm1nem2  48266  2timesltsqm1  48270  muldvdsfacm1  48278  iccpartiltu  48325  iccpartlt  48327  iccpartgt  48330  fmtnoge3  48436  fmtnodvds  48450  fmtnoprmfac2lem1  48472  2pwp1prm  48495  flsqrt  48499  sfprmdvdsmersenne  48509  lighneallem2  48512  lighneallem4a  48514  proththdlem  48519  proththd  48520  nprmdvdsfacm1lem4  48529  nnoALTV  48614  bgoldbtbndlem4  48727  gpgprismgrusgra  48977  gpgedgvtx0  48980  gpgvtxedg0  48982  gpg5nbgrvtx03starlem2  48988  gpg3kgrtriexlem4  49005  gpg3kgrtriexlem6  49007  cznnring  49180  divge1b  49445  divgt1b  49446  nn0eo  49461  regt1loggt0  49469  rege1logbrege0  49491  logblt1b  49497  fllog2  49501  nnolog2flm1  49523  dignn0flhalflem1  49548  rrxlinesc  49668  rrxlinec  49669  eenglngeehlnmlem1  49670  eenglngeehlnmlem2  49671  line2ylem  49684  line2  49685  line2xlem  49686  reseccl  50682  recsccl  50683  amgmwlem  50823  amgmlemALT  50824