Theorem 1red 11179

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 11069  1c1 11071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-mulcl 11132  ax-mulrcl 11133  ax-i2m1 11138  ax-1ne0 11139  ax-rrecex 11142  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395

This theorem is referenced by:  recgt0  12034  mulgt1  12050  ltrec  12071  nnne0  12244  nn0p1gt0  12507  nn0ge2m1nn  12548  nn0le2is012  12634  suprzcl  12650  ledivge1le  13063  ge2halflem1  13107  qbtwnre  13199  lincmb01cmp  13496  iccf1o  13497  xov1plusxeqvd  13499  zltaddlt1le  13506  nnge2recico01  13508  fznatpl1  13580  elfz1b  13595  elfzo0subge1  13708  fzonn0p1p1  13747  elfznelfzo  13776  elfznelfzob  13777  fladdz  13832  2tnp1ge0ge0  13836  flhalf  13837  ltdifltdiv  13841  fldiv4lem1div2uz2  13843  mulp1mod1  13921  m1modge3gt1  13928  modltm1p1mod  13933  addmodlteq  13956  ltexp2a  14176  expcan  14179  ltexp2  14180  leexp2  14181  leexp2a  14182  leexp2r  14184  nnlesq  14215  bernneq3  14241  expnbnd  14242  expnlbnd2  14244  expnngt1  14251  fzsdom2  14438  wrdlenge2n0  14562  swrd2lsw  14962  2swrd2eqwrdeq  14963  01sqrexlem7  15258  rddif  15351  reccn2  15607  rlimo1  15627  o1fsum  15824  abscvgcvg  15830  climcndslem1  15862  flo1  15867  harmonic  15872  geomulcvg  15889  fprodrecl  15966  fprodreclf  15972  fprodle  16009  bpoly4  16072  efcllem  16090  efgt1  16131  tanhlt1  16175  sinltx  16204  eirrlem  16219  p1modz1  16276  mod2eq1n2dvds  16364  oddge22np1  16366  ltoddhalfle  16378  nn0o1gt2  16398  nno  16399  nn0oddm1d2  16402  nnoddm1d2  16403  bitsfzolem  16451  bitsfzo  16452  bitsmod  16453  bitscmp  16455  bitsinv1lem  16458  smuval2  16499  coprmgcdb  16666  prmind2  16702  dvdsnprmd  16707  2mulprm  16710  isprm5  16725  isprm7  16726  divdenle  16767  zsqrtelqelz  16776  fermltl  16802  odzdvds  16814  modprm0  16824  iserodd  16854  difsqpwdvds  16906  pcfaclem  16917  prmreclem1  16935  4sqlem11  16974  4sqlem12  16975  ramub1lem1  17045  prmgaplem8  17077  2expltfac  17111  chnccat  18641  pgpfaclem2  20107  znidomb  21593  psdmvr  22214  chfacfisf  22894  chfacfisfcpmat  22895  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  nrginvrcnlem  24731  nmoid  24782  xrsmopn  24853  metnrmlem1a  24899  iihalf2cn  24976  iccpnfhmeo  24987  lebnumii  25008  htpycc  25022  pcohtpylem  25061  pcoass  25066  pcorevlem  25068  nmhmcn  25162  cncmet  25364  ovoliunlem1  25544  dyadmaxlem  25639  vitalilem2  25651  mbfi1fseqlem6  25762  itg2mulc  25789  itg2monolem1  25792  itg2monolem3  25794  dveflem  26021  mvth  26034  dvlipcn  26036  lhop1lem  26055  dvfsumlem1  26068  dvfsumlem2  26069  dvfsumlem3  26070  dvfsumlem4  26071  dvfsum2  26076  fta1glem2  26209  plyeq0lem  26250  fta1lem  26348  vieta1lem2  26352  aalioulem3  26375  aalioulem4  26376  radcnvlem1  26453  radcnvlem2  26454  dvradcnv  26461  abelthlem2  26472  abelthlem5  26475  abelthlem7  26478  abelth2  26482  cos02pilt1  26568  cosne0  26571  rplogcl  26646  logdivlti  26662  logno1  26678  dvlog2lem  26694  advlog  26696  logtayllem  26701  cxplt  26736  cxple  26737  cxpaddlelem  26793  cxpaddle  26794  rtprmirr  26802  relogbf  26833  logbgt0b  26835  isosctrlem1  26860  isosctrlem2  26861  chordthmlem4  26877  heron  26880  atanlogaddlem  26955  bndatandm  26971  leibpi  26984  log2tlbnd  26987  birthdaylem3  26995  rlimcnp  27007  rlimcnp2  27008  efrlim  27011  cxp2limlem  27017  cxp2lim  27018  divsqrtsumo1  27025  jensenlem2  27029  logdiflbnd  27036  fsumharmonic  27053  lgamgulmlem2  27071  lgamgulmlem3  27072  lgamgulmlem4  27073  lgamgulmlem5  27074  lgamgulmlem6  27075  lgamcvg2  27096  regamcl  27102  wilthlem2  27110  ftalem2  27115  basellem9  27130  vma1  27207  ppieq0  27217  mumullem2  27221  fsumfldivdiaglem  27230  chpeq0  27249  chtub  27253  chpval2  27259  chpchtsum  27260  chpub  27261  logfacrlim  27265  logexprlim  27266  mersenne  27268  perfectlem2  27271  dchrelbas4  27284  bcmono  27318  bposlem1  27325  bposlem2  27326  zabsle1  27337  lgslem3  27340  lgsmod  27364  lgsdir2lem4  27369  lgsdirprm  27372  gausslemma2dlem1a  27406  gausslemma2d  27415  lgsquadlem2  27422  2sqlem8  27467  chebbnd1lem1  27510  chebbnd1lem2  27511  chtppilimlem1  27514  chebbnd2  27518  chto1lb  27519  chpchtlim  27520  chpo1ubb  27522  vmadivsum  27523  rplogsumlem1  27525  rpvmasumlem  27528  dchrisumlem3  27532  dchrmusumlema  27534  dchrmusum2  27535  dchrvmasumlem2  27539  dchrvmasumlem3  27540  dchrvmasumiflem1  27542  dchrvmasumiflem2  27543  dchrisum0flblem1  27549  dchrisum0flblem2  27550  dchrisum0fno1  27552  dchrisum0re  27554  dchrisum0lema  27555  dchrisum0lem1b  27556  dchrisum0lem2a  27558  dchrisum0lem2  27559  dchrisum0lem3  27560  rplogsum  27568  dirith2  27569  mudivsum  27571  mulogsumlem  27572  mulogsum  27573  mulog2sumlem1  27575  mulog2sumlem2  27576  vmalogdivsum2  27579  vmalogdivsum  27580  2vmadivsumlem  27581  log2sumbnd  27585  selberglem2  27587  selberg2lem  27591  chpdifbnd  27596  selberg3lem1  27598  selberg3  27600  selberg4lem1  27601  selberg4  27602  pntrmax  27605  pntrsumo1  27606  pntrsumbnd  27607  selberg3r  27610  selberg4r  27611  selberg34r  27612  pntrlog2bndlem1  27618  pntrlog2bndlem2  27619  pntrlog2bndlem3  27620  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  pntrlog2bndlem6  27624  pntrlog2bnd  27625  pntpbnd1a  27626  pntpbnd1  27627  pntibndlem2a  27631  pntibndlem2  27632  pntibnd  27634  pntlemc  27636  pntlemg  27639  pntlemr  27643  pntlemk  27647  pnt  27655  qabvle  27666  ostth2lem3  27676  ostth2  27678  trgcgrg  28661  tgcgr4  28677  ttgcontlem1  29031  axpaschlem  29087  axlowdimlem16  29104  axcontlem2  29112  axcontlem7  29117  nbusgrvtxm1  29526  upgrewlkle2  29753  pthdlem1  29912  crctcshwlkn0lem3  29958  crctcshwlkn0lem5  29960  wwlksm1edg  30027  wwlksnextproplem2  30056  clwlkclwwlklem2fv1  30143  clwlkclwwlklem2fv2  30144  clwlkclwwlklem2  30148  clwlkclwwlk2  30151  clwwisshclwwslem  30162  clwwlkf1  30197  clwwlkext2edg  30204  clwlknf1oclwwlknlem1  30229  clwwlknonex2lem2  30256  numclwwlk7  30539  frgrreggt1  30541  frgrogt3nreg  30545  smcnlem  30846  nmoub3i  30922  blocnilem  30953  ubthlem2  31020  minvecolem4  31029  htthlem  31066  nmcexi  32175  nmopcoi  32244  stadd3i  32397  cdj1i  32582  nnmulge  32891  receqid  32896  nndiffz1  32938  fzsplit3  32945  nexple  32996  indf1o  33003  wrdt2ind  33092  pmtrto1cl  33240  fzto1st1  33243  fzto1st  33244  psgnfzto1st  33246  cycpmco2lem6  33272  cycpmco2lem7  33273  cycpmrn  33284  qsidomlem1  33600  krull  33628  ply1degltel  33751  ply1degltlss  33753  constrnegcl  34021  constrdircl  34023  iconstr  34024  constrrecl  34027  constrmulcl  34029  constrreinvcl  34030  constrresqrtcl  34035  cos9thpiminplylem1  34040  cos9thpiminply  34046  cos9thpinconstrlem1  34047  1smat1  34062  submateqlem1  34065  madjusmdetlem2  34086  unitdivcld  34159  sqsscirc1  34166  esumdivc  34341  dya2ub  34528  dya2iocress  34532  dya2iocbrsiga  34533  dya2icobrsiga  34534  dya2icoseg  34535  dya2iocucvr  34542  sxbrsigalem2  34544  fibp1  34659  probmeasb  34688  dstrvprob  34730  dstfrvunirn  34733  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemsgt1  34769  ballotlemsel1i  34771  ballotlemfrcn0  34788  signsply0  34809  itgexpif  34864  reprlt  34877  chtvalz  34887  breprexplemc  34890  breprexp  34891  circlemeth  34898  tgoldbachgnn  34917  acycgr1v  35463  subfaclim  35502  cvmliftlem2  35600  cvmliftlem13  35610  snmlff  35643  bccolsum  36053  faclim  36060  nn0prpwlem  36646  dnibndlem10  36889  dnibndlem12  36891  knoppcnlem4  36898  unblimceq0  36909  knoppndvlem1  36914  knoppndvlem2  36915  knoppndvlem3  36916  knoppndvlem7  36920  knoppndvlem11  36924  knoppndvlem12  36925  knoppndvlem14  36927  knoppndvlem15  36928  knoppndvlem17  36930  knoppndvlem18  36931  knoppndvlem20  36933  irrdiff  37782  poimirlem6  38089  poimirlem7  38090  poimirlem15  38098  poimirlem19  38102  poimirlem29  38112  poimirlem30  38113  poimirlem31  38114  poimirlem32  38115  broucube  38117  itg2addnclem2  38135  itg2addnclem3  38136  areacirclem1  38171  areacirclem4  38174  incsequz  38211  totbndbnd  38252  bfplem2  38286  resdvopclptsd  42609  lcmineqlem2  42611  lcmineqlem3  42612  lcmineqlem10  42619  lcmineqlem12  42621  lcmineqlem15  42624  lcmineqlem18  42627  lcmineqlem19  42628  lcmineqlem20  42629  lcmineqlem22  42631  lcmineqlem23  42632  3lexlogpow5ineq2  42636  3lexlogpow5ineq4  42637  3lexlogpow5ineq3  42638  3lexlogpow2ineq1  42639  3lexlogpow2ineq2  42640  3lexlogpow5ineq5  42641  aks4d1lem1  42643  dvrelog2  42645  dvrelog3  42646  dvrelog2b  42647  dvrelogpow2b  42649  aks4d1p1p3  42650  aks4d1p1p2  42651  aks4d1p1p4  42652  aks4d1p1p6  42654  aks4d1p1p7  42655  aks4d1p1p5  42656  aks4d1p1  42657  aks4d1p2  42658  aks4d1p3  42659  aks4d1p5  42661  aks4d1p6  42662  aks4d1p7d1  42663  aks4d1p7  42664  aks4d1p8d2  42666  aks4d1p8d3  42667  aks4d1p8  42668  aks4d1p9  42669  posbezout  42681  primrootlekpowne0  42686  primrootspoweq0  42687  aks6d1c1  42697  aks6d1c2p2  42700  hashscontpow1  42702  aks6d1c3  42704  aks6d1c2lem4  42708  aks6d1c2  42711  2np3bcnp1  42725  2ap1caineq  42726  sticksstones6  42732  sticksstones7  42733  sticksstones10  42736  sticksstones12a  42738  sticksstones12  42739  sticksstones22  42749  aks6d1c6lem3  42753  aks6d1c6lem4  42754  bcled  42759  bcle2d  42760  aks6d1c7lem1  42761  aks6d1c7lem2  42762  unitscyglem2  42777  unitscyglem4  42779  unitscyglem5  42780  aks5lem8  42782  sn-1ne2  42844  redvmptabs  42933  sn-00idlem2  42972  sn-0ne2  42979  rei4  42997  rediveq1d  43024  sn-rediv1d  43025  sn-rereccld  43028  rerecne0d  43029  rerecidd  43030  rerecrecd  43032  sn-0tie0  43037  sn-nnne0  43046  mulgt0b1d  43058  sn-ltmulgt11d  43060  sn-0lt1  43061  sn-mulgt1d  43065  fimgmcyc  43116  flt4lem7  43205  fltnlta  43209  3cubeslem1  43229  3cubeslem3r  43232  3cubeslem4  43234  lzenom  43315  irrapxlem1  43363  irrapxlem2  43364  irrapxlem4  43366  irrapxlem5  43367  pellexlem2  43371  pell1qrge1  43411  pell1qr1  43412  elpell1qr2  43413  pell14qrgapw  43417  pellfundgt1  43424  pellfundglb  43426  pellfundex  43427  pellfundrp  43429  pellfundne1  43430  rmspecsqrtnq  43447  rmspecnonsq  43448  rmspecfund  43450  rmspecpos  43457  monotoddzzfi  43483  rmygeid  43505  areaquad  43757  imo72b2lem0  44705  imo72b2lem1  44709  imo72b2  44712  cvgdvgrat  44853  radcnvrat  44854  hashnzfzclim  44862  lhe4.4ex1a  44869  binomcxplemnn0  44889  binomcxplemdvbinom  44893  binomcxplemnotnn0  44896  oddfl  45821  abscosbd  45822  zltlesub  45828  abssinbd  45838  monoords  45840  fzisoeu  45843  fzdifsuc2  45853  suplesup  45879  xralrple2  45894  infxr  45906  infleinflem2  45910  reclt0d  45926  xrralrecnnge  45929  sqrlearg  46093  iooiinioc  46096  fmul01  46120  fmul01lt1lem1  46124  fmul01lt1lem2  46125  climsuselem1  46147  sumnnodd  46170  0ellimcdiv  46187  dvmptidg  46455  dvcosax  46464  ioodvbdlimc1lem1  46469  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvxpaek  46478  dvnmul  46481  iblspltprt  46511  itgspltprt  46517  stoweidlem5  46543  stoweidlem7  46545  stoweidlem10  46548  stoweidlem11  46549  stoweidlem12  46550  stoweidlem13  46551  stoweidlem14  46552  stoweidlem16  46554  stoweidlem18  46556  stoweidlem20  46558  stoweidlem24  46562  stoweidlem25  46563  stoweidlem34  46572  stoweidlem36  46574  stoweidlem38  46576  stoweidlem40  46578  stoweidlem41  46579  stoweidlem42  46580  stoweidlem45  46583  stoweidlem51  46589  stoweidlem60  46598  wallispilem3  46605  wallispilem4  46606  wallispilem5  46607  wallispi  46608  wallispi2lem1  46609  wallispi2lem2  46610  wallispi2  46611  stirlinglem1  46612  stirlinglem3  46614  stirlinglem5  46616  stirlinglem6  46617  stirlinglem7  46618  stirlinglem8  46619  stirlinglem10  46621  stirlinglem11  46622  stirlinglem12  46623  stirlinglem13  46624  stirlinglem15  46626  dirker2re  46630  dirkerval2  46632  dirkerre  46633  dirkertrigeqlem1  46636  dirkertrigeqlem3  46638  dirkeritg  46640  dirkercncflem1  46641  dirkercncflem2  46642  dirkercncflem4  46644  fourierdlem5  46650  fourierdlem6  46651  fourierdlem11  46656  fourierdlem15  46660  fourierdlem19  46664  fourierdlem20  46665  fourierdlem24  46669  fourierdlem26  46671  fourierdlem28  46673  fourierdlem30  46675  fourierdlem39  46684  fourierdlem41  46686  fourierdlem43  46688  fourierdlem47  46691  fourierdlem48  46692  fourierdlem56  46700  fourierdlem60  46704  fourierdlem61  46705  fourierdlem62  46706  fourierdlem64  46708  fourierdlem65  46709  fourierdlem66  46710  fourierdlem68  46712  fourierdlem73  46717  fourierdlem78  46722  fourierdlem79  46723  fourierdlem87  46731  fourierdlem103  46747  fourierdlem104  46748  sqwvfoura  46766  fouriersw  46769  etransclem4  46776  etransclem23  46795  etransclem24  46796  etransclem31  46803  etransclem32  46804  etransclem35  46807  etransclem41  46813  etransclem46  46818  etransclem48  46820  etransc  46821  ioorrnopnxrlem  46844  nnfoctbdjlem  46993  iundjiun  46998  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  hoidmvlelem4  47136  ovnhoilem1  47139  vonioolem2  47219  vonicclem2  47222  pimrecltneg  47262  smfrec  47327  smfmullem1  47329  smfmullem2  47330  smfdiv  47335  sigaradd  47404  ormkglobd  47415  cjnpoly  47447  p1lep2  47858  zm1nn  47860  ceilhalfgt1  47891  2tceilhalfelfzo1  47894  ceilbi  47895  rehalfge1  47897  ceilhalfnn  47898  flmrecm1  47901  addmodne  47908  m1mod0mod1  47918  m1modmmod  47922  difmodm1lt  47923  modmknepk  47926  modp2nep1  47931  modm1nem2  47933  2timesltsqm1  47937  muldvdsfacm1  47945  iccpartiltu  47992  iccpartlt  47994  iccpartgt  47997  fmtnoge3  48103  fmtnodvds  48117  fmtnoprmfac2lem1  48139  2pwp1prm  48162  flsqrt  48166  sfprmdvdsmersenne  48176  lighneallem2  48179  lighneallem4a  48181  proththdlem  48186  proththd  48187  nprmdvdsfacm1lem4  48196  nnoALTV  48281  bgoldbtbndlem4  48394  gpgprismgrusgra  48644  gpgedgvtx0  48647  gpgvtxedg0  48649  gpg5nbgrvtx03starlem2  48655  gpg3kgrtriexlem4  48672  gpg3kgrtriexlem6  48674  cznnring  48848  divge1b  49098  divgt1b  49099  nn0eo  49114  regt1loggt0  49122  rege1logbrege0  49144  logblt1b  49150  fllog2  49154  nnolog2flm1  49176  dignn0flhalflem1  49201  rrxlinesc  49321  rrxlinec  49322  eenglngeehlnmlem1  49323  eenglngeehlnmlem2  49324  line2ylem  49337  line2  49338  line2xlem  49339  reseccl  50338  recsccl  50339  amgmwlem  50387  amgmlemALT  50388