Theorem 1red 10642

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10536  1c1 10538

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  recgt0  11486  ltrec  11522  nnne0  11672  nn0p1gt0  11927  nn0ge2m1nn  11965  nn0le2is012  12047  suprzcl  12063  ledivge1le  12461  qbtwnre  12593  lincmb01cmp  12882  iccf1o  12883  xov1plusxeqvd  12885  zltaddlt1le  12891  fznatpl1  12962  elfz1b  12977  fzonn0p1p1  13117  elfznelfzo  13143  elfznelfzob  13144  fladdz  13196  2tnp1ge0ge0  13200  flhalf  13201  ltdifltdiv  13205  fldiv4lem1div2uz2  13207  mulp1mod1  13281  m1modge3gt1  13287  modltm1p1mod  13292  addmodlteq  13315  ltexp2a  13531  expcan  13534  ltexp2  13535  leexp2  13536  leexp2a  13537  leexp2r  13539  nnlesq  13569  bernneq3  13593  expnbnd  13594  expnlbnd2  13596  expnngt1  13603  fzsdom2  13790  wrdlenge2n0  13904  swrd2lsw  14314  2swrd2eqwrdeq  14315  sqrlem7  14608  rddif  14700  reccn2  14953  rlimo1  14973  o1fsum  15168  abscvgcvg  15174  climcndslem1  15204  flo1  15209  harmonic  15214  geomulcvg  15232  fprodrecl  15307  fprodreclf  15313  fprodle  15350  bpoly4  15413  efcllem  15431  efgt1  15469  tanhlt1  15513  sinltx  15542  eirrlem  15557  p1modz1  15614  mod2eq1n2dvds  15696  oddge22np1  15698  ltoddhalfle  15710  nn0o1gt2  15732  nno  15733  nn0oddm1d2  15736  nnoddm1d2  15737  bitsfzolem  15783  bitsfzo  15784  bitsmod  15785  bitscmp  15787  bitsinv1lem  15790  smuval2  15831  coprmgcdb  15993  prmind2  16029  dvdsnprmd  16034  2mulprm  16037  isprm5  16051  isprm7  16052  divdenle  16089  zsqrtelqelz  16098  fermltl  16121  odzdvds  16132  modprm0  16142  iserodd  16172  difsqpwdvds  16223  pcfaclem  16234  prmreclem1  16252  4sqlem11  16291  4sqlem12  16292  ramub1lem1  16362  prmgaplem8  16394  2expltfac  16426  pgpfaclem2  19204  znidomb  20708  chfacfisf  21462  chfacfisfcpmat  21463  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  nrginvrcnlem  23300  nmoid  23351  xrsmopn  23420  metnrmlem1a  23466  iccpnfhmeo  23549  lebnumii  23570  htpycc  23584  pcohtpylem  23623  pcoass  23628  pcorevlem  23630  nmhmcn  23724  cncmet  23925  ovoliunlem1  24103  dyadmaxlem  24198  vitalilem2  24210  mbfi1fseqlem6  24321  itg2mulc  24348  itg2monolem1  24351  itg2monolem3  24353  dveflem  24576  mvth  24589  dvlipcn  24591  lhop1lem  24610  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsum2  24631  fta1glem2  24760  plyeq0lem  24800  fta1lem  24896  vieta1lem2  24900  aalioulem3  24923  aalioulem4  24924  radcnvlem1  25001  radcnvlem2  25002  dvradcnv  25009  abelthlem2  25020  abelthlem5  25023  abelthlem7  25026  abelth2  25030  cos02pilt1  25111  cosne0  25114  rplogcl  25187  logdivlti  25203  logno1  25219  dvlog2lem  25235  advlog  25237  logtayllem  25242  cxplt  25277  cxple  25278  cxpaddlelem  25332  cxpaddle  25333  relogbf  25369  logbgt0b  25371  isosctrlem1  25396  isosctrlem2  25397  chordthmlem4  25413  heron  25416  atanlogaddlem  25491  bndatandm  25507  leibpi  25520  log2tlbnd  25523  birthdaylem3  25531  rlimcnp  25543  rlimcnp2  25544  efrlim  25547  cxp2limlem  25553  cxp2lim  25554  divsqrtsumo1  25561  jensenlem2  25565  logdiflbnd  25572  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  lgamgulmlem6  25611  lgamcvg2  25632  regamcl  25638  wilthlem2  25646  ftalem2  25651  basellem9  25666  vma1  25743  ppieq0  25753  mumullem2  25757  fsumfldivdiaglem  25766  chpeq0  25784  chtub  25788  chpval2  25794  chpchtsum  25795  chpub  25796  logfacrlim  25800  logexprlim  25801  mersenne  25803  perfectlem2  25806  dchrelbas4  25819  bcmono  25853  bposlem1  25860  bposlem2  25861  zabsle1  25872  lgslem3  25875  lgsmod  25899  lgsdir2lem4  25904  lgsdirprm  25907  gausslemma2dlem1a  25941  gausslemma2d  25950  lgsquadlem2  25957  2sqlem8  26002  chebbnd1lem1  26045  chebbnd1lem2  26046  chtppilimlem1  26049  chebbnd2  26053  chto1lb  26054  chpchtlim  26055  chpo1ubb  26057  vmadivsum  26058  rplogsumlem1  26060  rpvmasumlem  26063  dchrisumlem3  26067  dchrmusumlema  26069  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  dchrvmasumiflem2  26078  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dchrisum0fno1  26087  dchrisum0re  26089  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0lem3  26095  rplogsum  26103  dirith2  26104  mudivsum  26106  mulogsumlem  26107  mulogsum  26108  mulog2sumlem1  26110  mulog2sumlem2  26111  vmalogdivsum2  26114  vmalogdivsum  26115  2vmadivsumlem  26116  log2sumbnd  26120  selberglem2  26122  selberg2lem  26126  chpdifbnd  26131  selberg3lem1  26133  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrmax  26140  pntrsumo1  26141  pntrsumbnd  26142  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd1  26162  pntibndlem2a  26166  pntibndlem2  26167  pntibnd  26169  pntlemc  26171  pntlemg  26174  pntlemr  26178  pntlemk  26182  pnt  26190  qabvle  26201  ostth2lem3  26211  ostth2  26213  trgcgrg  26301  tgcgr4  26317  ttgcontlem1  26671  axpaschlem  26726  axlowdimlem16  26743  axcontlem2  26751  axcontlem7  26756  nbusgrvtxm1  27161  upgrewlkle2  27388  pthdlem1  27547  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  wwlksm1edg  27659  wwlksnextproplem2  27689  clwlkclwwlklem2fv1  27773  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2  27778  clwlkclwwlk2  27781  clwwisshclwwslem  27792  clwwlkf1  27828  clwwlkext2edg  27835  clwlknf1oclwwlknlem1  27860  clwwlknonex2lem2  27887  numclwwlk7  28170  frgrreggt1  28172  frgrogt3nreg  28176  smcnlem  28474  nmoub3i  28550  blocnilem  28581  ubthlem2  28648  minvecolem4  28657  htthlem  28694  nmcexi  29803  nmopcoi  29872  stadd3i  30025  cdj1i  30210  nnmulge  30474  nndiffz1  30509  fzsplit3  30517  wrdt2ind  30627  pmtrto1cl  30741  fzto1st1  30744  fzto1st  30745  psgnfzto1st  30747  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmrn  30785  qsidomlem1  30965  krull  30980  1smat1  31069  submateqlem1  31072  madjusmdetlem2  31093  unitdivcld  31144  sqsscirc1  31151  nexple  31268  indf1o  31283  esumdivc  31342  dya2ub  31528  dya2iocress  31532  dya2iocbrsiga  31533  dya2icobrsiga  31534  dya2icoseg  31535  dya2iocucvr  31542  sxbrsigalem2  31544  fibp1  31659  probmeasb  31688  dstrvprob  31729  dstfrvunirn  31732  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemsgt1  31768  ballotlemsel1i  31770  ballotlemfrcn0  31787  signsply0  31821  itgexpif  31877  reprlt  31890  chtvalz  31900  breprexplemc  31903  breprexp  31904  circlemeth  31911  tgoldbachgnn  31930  acycgr1v  32396  subfaclim  32435  cvmliftlem2  32533  cvmliftlem13  32543  snmlff  32576  bccolsum  32971  faclim  32978  nn0prpwlem  33670  dnibndlem10  33826  dnibndlem12  33828  knoppcnlem4  33835  unblimceq0  33846  knoppndvlem1  33851  knoppndvlem2  33852  knoppndvlem3  33853  knoppndvlem7  33857  knoppndvlem11  33861  knoppndvlem12  33862  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem18  33868  knoppndvlem20  33870  poimirlem6  34913  poimirlem7  34914  poimirlem15  34922  poimirlem19  34926  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  broucube  34941  itg2addnclem2  34959  itg2addnclem3  34960  areacirclem1  34997  areacirclem4  35000  incsequz  35038  totbndbnd  35082  bfplem2  35116  2xp3dxp2ge1d  39146  factwoffsmonot  39147  sn-1ne2  39207  rtprmirr  39243  sn-00idlem2  39278  sn-0ne2  39285  fltnlta  39324  3cubeslem1  39330  3cubeslem3r  39333  3cubeslem4  39335  lzenom  39416  irrapxlem1  39468  irrapxlem2  39469  irrapxlem4  39471  irrapxlem5  39472  pellexlem2  39476  pell1qrge1  39516  pell1qr1  39517  elpell1qr2  39518  pell14qrgapw  39522  pellfundgt1  39529  pellfundglb  39531  pellfundex  39532  pellfundrp  39534  pellfundne1  39535  rmspecsqrtnq  39552  rmspecnonsq  39553  rmspecfund  39555  rmspecpos  39562  monotoddzzfi  39588  rmygeid  39610  areaquad  39872  imo72b2lem0  40565  imo72b2lem1  40570  imo72b2  40574  cvgdvgrat  40694  radcnvrat  40695  hashnzfzclim  40703  lhe4.4ex1a  40710  binomcxplemnn0  40730  binomcxplemdvbinom  40734  binomcxplemnotnn0  40737  oddfl  41592  abscosbd  41593  zltlesub  41600  abssinbd  41611  monoords  41613  fzisoeu  41616  fzdifsuc2  41626  suplesup  41656  xralrple2  41671  infxr  41684  infleinflem2  41688  reclt0d  41707  xrralrecnnge  41711  sqrlearg  41878  iooiinioc  41881  fmul01  41910  fmul01lt1lem1  41914  fmul01lt1lem2  41915  climsuselem1  41937  sumnnodd  41960  0ellimcdiv  41979  dvmptidg  42250  dvcosax  42260  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvxpaek  42274  dvnmul  42277  iblspltprt  42307  itgspltprt  42313  stoweidlem5  42339  stoweidlem7  42341  stoweidlem10  42344  stoweidlem11  42345  stoweidlem12  42346  stoweidlem13  42347  stoweidlem14  42348  stoweidlem16  42350  stoweidlem18  42352  stoweidlem20  42354  stoweidlem24  42358  stoweidlem25  42359  stoweidlem34  42368  stoweidlem36  42370  stoweidlem38  42372  stoweidlem40  42374  stoweidlem41  42375  stoweidlem42  42376  stoweidlem45  42379  stoweidlem51  42385  stoweidlem60  42394  wallispilem3  42401  wallispilem4  42402  wallispilem5  42403  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  wallispi2  42407  stirlinglem1  42408  stirlinglem3  42410  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem8  42415  stirlinglem10  42417  stirlinglem11  42418  stirlinglem12  42419  stirlinglem13  42420  stirlinglem15  42422  dirker2re  42426  dirkerval2  42428  dirkerre  42429  dirkertrigeqlem1  42432  dirkertrigeqlem3  42434  dirkeritg  42436  dirkercncflem1  42437  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem5  42446  fourierdlem6  42447  fourierdlem11  42452  fourierdlem15  42456  fourierdlem19  42460  fourierdlem20  42461  fourierdlem24  42465  fourierdlem26  42467  fourierdlem28  42469  fourierdlem30  42471  fourierdlem39  42480  fourierdlem41  42482  fourierdlem43  42484  fourierdlem47  42487  fourierdlem48  42488  fourierdlem56  42496  fourierdlem60  42500  fourierdlem61  42501  fourierdlem62  42502  fourierdlem64  42504  fourierdlem65  42505  fourierdlem66  42506  fourierdlem68  42508  fourierdlem73  42513  fourierdlem78  42518  fourierdlem79  42519  fourierdlem87  42527  fourierdlem103  42543  fourierdlem104  42544  sqwvfoura  42562  fouriersw  42565  etransclem4  42572  etransclem23  42591  etransclem24  42592  etransclem31  42599  etransclem32  42600  etransclem35  42603  etransclem41  42609  etransclem46  42614  etransclem48  42616  etransc  42617  ioorrnopnxrlem  42640  nnfoctbdjlem  42786  iundjiun  42791  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  ovnhoilem1  42932  vonioolem2  43012  vonicclem2  43015  pimrecltneg  43050  smfrec  43113  smfmullem1  43115  smfmullem2  43116  smfdiv  43121  sigaradd  43172  p1lep2  43549  zm1nn  43551  m1mod0mod1  43578  iccpartiltu  43631  iccpartlt  43633  iccpartgt  43636  fmtnoge3  43741  fmtnodvds  43755  fmtnoprmfac2lem1  43777  2pwp1prm  43800  flsqrt  43805  sfprmdvdsmersenne  43817  lighneallem2  43820  lighneallem4a  43822  proththdlem  43827  proththd  43828  nnoALTV  43909  bgoldbtbndlem4  44022  cznnring  44276  divge1b  44616  divgt1b  44617  m1modmmod  44630  difmodm1lt  44631  nn0eo  44637  regt1loggt0  44645  rege1logbrege0  44667  logblt1b  44673  fllog2  44677  nnolog2flm1  44699  dignn0flhalflem1  44724  rrxlinesc  44771  rrxlinec  44772  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  line2ylem  44787  line2  44788  line2xlem  44789  reseccl  44901  recsccl  44902  amgmwlem  44952  amgmlemALT  44953