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  39117  factwoffsmonot  39118  sn-1ne2  39178  rtprmirr  39214  sn-00idlem2  39249  sn-0ne2  39256  fltnlta  39295  3cubeslem1  39301  3cubeslem3r  39304  3cubeslem4  39306  lzenom  39387  irrapxlem1  39439  irrapxlem2  39440  irrapxlem4  39442  irrapxlem5  39443  pellexlem2  39447  pell1qrge1  39487  pell1qr1  39488  elpell1qr2  39489  pell14qrgapw  39493  pellfundgt1  39500  pellfundglb  39502  pellfundex  39503  pellfundrp  39505  pellfundne1  39506  rmspecsqrtnq  39523  rmspecnonsq  39524  rmspecfund  39526  rmspecpos  39533  monotoddzzfi  39559  rmygeid  39581  areaquad  39843  imo72b2lem0  40536  imo72b2lem1  40541  imo72b2  40545  cvgdvgrat  40665  radcnvrat  40666  hashnzfzclim  40674  lhe4.4ex1a  40681  binomcxplemnn0  40701  binomcxplemdvbinom  40705  binomcxplemnotnn0  40708  oddfl  41563  abscosbd  41564  zltlesub  41571  abssinbd  41582  monoords  41584  fzisoeu  41587  fzdifsuc2  41597  suplesup  41627  xralrple2  41642  infxr  41655  infleinflem2  41659  reclt0d  41678  xrralrecnnge  41682  sqrlearg  41849  iooiinioc  41852  fmul01  41881  fmul01lt1lem1  41885  fmul01lt1lem2  41886  climsuselem1  41908  sumnnodd  41931  0ellimcdiv  41950  dvmptidg  42221  dvcosax  42231  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvxpaek  42245  dvnmul  42248  iblspltprt  42278  itgspltprt  42284  stoweidlem5  42310  stoweidlem7  42312  stoweidlem10  42315  stoweidlem11  42316  stoweidlem12  42317  stoweidlem13  42318  stoweidlem14  42319  stoweidlem16  42321  stoweidlem18  42323  stoweidlem20  42325  stoweidlem24  42329  stoweidlem25  42330  stoweidlem34  42339  stoweidlem36  42341  stoweidlem38  42343  stoweidlem40  42345  stoweidlem41  42346  stoweidlem42  42347  stoweidlem45  42350  stoweidlem51  42356  stoweidlem60  42365  wallispilem3  42372  wallispilem4  42373  wallispilem5  42374  wallispi  42375  wallispi2lem1  42376  wallispi2lem2  42377  wallispi2  42378  stirlinglem1  42379  stirlinglem3  42381  stirlinglem5  42383  stirlinglem6  42384  stirlinglem7  42385  stirlinglem8  42386  stirlinglem10  42388  stirlinglem11  42389  stirlinglem12  42390  stirlinglem13  42391  stirlinglem15  42393  dirker2re  42397  dirkerval2  42399  dirkerre  42400  dirkertrigeqlem1  42403  dirkertrigeqlem3  42405  dirkeritg  42407  dirkercncflem1  42408  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem5  42417  fourierdlem6  42418  fourierdlem11  42423  fourierdlem15  42427  fourierdlem19  42431  fourierdlem20  42432  fourierdlem24  42436  fourierdlem26  42438  fourierdlem28  42440  fourierdlem30  42442  fourierdlem39  42451  fourierdlem41  42453  fourierdlem43  42455  fourierdlem47  42458  fourierdlem48  42459  fourierdlem56  42467  fourierdlem60  42471  fourierdlem61  42472  fourierdlem62  42473  fourierdlem64  42475  fourierdlem65  42476  fourierdlem66  42477  fourierdlem68  42479  fourierdlem73  42484  fourierdlem78  42489  fourierdlem79  42490  fourierdlem87  42498  fourierdlem103  42514  fourierdlem104  42515  sqwvfoura  42533  fouriersw  42536  etransclem4  42543  etransclem23  42562  etransclem24  42563  etransclem31  42570  etransclem32  42571  etransclem35  42574  etransclem41  42580  etransclem46  42585  etransclem48  42587  etransc  42588  ioorrnopnxrlem  42611  nnfoctbdjlem  42757  iundjiun  42762  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem4  42900  ovnhoilem1  42903  vonioolem2  42983  vonicclem2  42986  pimrecltneg  43021  smfrec  43084  smfmullem1  43086  smfmullem2  43087  smfdiv  43092  sigaradd  43143  p1lep2  43520  zm1nn  43522  m1mod0mod1  43549  iccpartiltu  43602  iccpartlt  43604  iccpartgt  43607  fmtnoge3  43712  fmtnodvds  43726  fmtnoprmfac2lem1  43748  2pwp1prm  43771  flsqrt  43776  sfprmdvdsmersenne  43788  lighneallem2  43791  lighneallem4a  43793  proththdlem  43798  proththd  43799  nnoALTV  43880  bgoldbtbndlem4  43993  cznnring  44247  divge1b  44587  divgt1b  44588  m1modmmod  44601  difmodm1lt  44602  nn0eo  44608  regt1loggt0  44616  rege1logbrege0  44638  logblt1b  44644  fllog2  44648  nnolog2flm1  44670  dignn0flhalflem1  44695  rrxlinesc  44742  rrxlinec  44743  eenglngeehlnmlem1  44744  eenglngeehlnmlem2  44745  line2ylem  44758  line2  44759  line2xlem  44760  reseccl  44872  recsccl  44873  amgmwlem  44923  amgmlemALT  44924