Theorem 1red 11234

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11126  1c1 11128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  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 theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  recgt0  12085  mulgt1  12101  ltrec  12122  nnne0  12272  nn0p1gt0  12528  nn0ge2m1nn  12569  nn0le2is012  12655  suprzcl  12671  ledivge1le  13078  ge2halflem1  13122  qbtwnre  13213  lincmb01cmp  13510  iccf1o  13511  xov1plusxeqvd  13513  zltaddlt1le  13520  fznatpl1  13593  elfz1b  13608  elfzo0subge1  13720  fzonn0p1p1  13758  elfznelfzo  13786  elfznelfzob  13787  fladdz  13840  2tnp1ge0ge0  13844  flhalf  13845  ltdifltdiv  13849  fldiv4lem1div2uz2  13851  mulp1mod1  13927  m1modge3gt1  13934  modltm1p1mod  13939  addmodlteq  13962  ltexp2a  14182  expcan  14185  ltexp2  14186  leexp2  14187  leexp2a  14188  leexp2r  14190  nnlesq  14221  bernneq3  14247  expnbnd  14248  expnlbnd2  14250  expnngt1  14257  fzsdom2  14444  wrdlenge2n0  14568  swrd2lsw  14969  2swrd2eqwrdeq  14970  01sqrexlem7  15265  rddif  15357  reccn2  15611  rlimo1  15631  o1fsum  15827  abscvgcvg  15833  climcndslem1  15863  flo1  15868  harmonic  15873  geomulcvg  15890  fprodrecl  15967  fprodreclf  15973  fprodle  16010  bpoly4  16073  efcllem  16091  efgt1  16132  tanhlt1  16176  sinltx  16205  eirrlem  16220  p1modz1  16277  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  16724  isprm7  16725  divdenle  16766  zsqrtelqelz  16775  fermltl  16801  odzdvds  16813  modprm0  16823  iserodd  16853  difsqpwdvds  16905  pcfaclem  16916  prmreclem1  16934  4sqlem11  16973  4sqlem12  16974  ramub1lem1  17044  prmgaplem8  17076  2expltfac  17110  pgpfaclem2  20063  znidomb  21520  psdmvr  22105  chfacfisf  22790  chfacfisfcpmat  22791  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  nrginvrcnlem  24628  nmoid  24679  xrsmopn  24750  metnrmlem1a  24796  iihalf2cn  24878  iccpnfhmeo  24892  lebnumii  24914  htpycc  24928  pcohtpylem  24968  pcoass  24973  pcorevlem  24975  nmhmcn  25069  cncmet  25272  ovoliunlem1  25453  dyadmaxlem  25548  vitalilem2  25560  mbfi1fseqlem6  25671  itg2mulc  25698  itg2monolem1  25701  itg2monolem3  25703  dveflem  25933  mvth  25947  dvlipcn  25949  lhop1lem  25968  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsum2  25991  fta1glem2  26124  plyeq0lem  26165  fta1lem  26265  vieta1lem2  26269  aalioulem3  26292  aalioulem4  26293  radcnvlem1  26372  radcnvlem2  26373  dvradcnv  26380  abelthlem2  26392  abelthlem5  26395  abelthlem7  26398  abelth2  26402  cos02pilt1  26485  cosne0  26488  rplogcl  26563  logdivlti  26579  logno1  26595  dvlog2lem  26611  advlog  26613  logtayllem  26618  cxplt  26653  cxple  26654  cxpaddlelem  26711  cxpaddle  26712  rtprmirr  26720  relogbf  26751  logbgt0b  26753  isosctrlem1  26778  isosctrlem2  26779  chordthmlem4  26795  heron  26798  atanlogaddlem  26873  bndatandm  26889  leibpi  26902  log2tlbnd  26905  birthdaylem3  26913  rlimcnp  26925  rlimcnp2  26926  efrlim  26929  efrlimOLD  26930  cxp2limlem  26936  cxp2lim  26937  divsqrtsumo1  26944  jensenlem2  26948  logdiflbnd  26955  fsumharmonic  26972  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulmlem6  26994  lgamcvg2  27015  regamcl  27021  wilthlem2  27029  ftalem2  27034  basellem9  27049  vma1  27126  ppieq0  27136  mumullem2  27140  fsumfldivdiaglem  27149  chpeq0  27169  chtub  27173  chpval2  27179  chpchtsum  27180  chpub  27181  logfacrlim  27185  logexprlim  27186  mersenne  27188  perfectlem2  27191  dchrelbas4  27204  bcmono  27238  bposlem1  27245  bposlem2  27246  zabsle1  27257  lgslem3  27260  lgsmod  27284  lgsdir2lem4  27289  lgsdirprm  27292  gausslemma2dlem1a  27326  gausslemma2d  27335  lgsquadlem2  27342  2sqlem8  27387  chebbnd1lem1  27430  chebbnd1lem2  27431  chtppilimlem1  27434  chebbnd2  27438  chto1lb  27439  chpchtlim  27440  chpo1ubb  27442  vmadivsum  27443  rplogsumlem1  27445  rpvmasumlem  27448  dchrisumlem3  27452  dchrmusumlema  27454  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  dchrisum0flblem1  27469  dchrisum0flblem2  27470  dchrisum0fno1  27472  dchrisum0re  27474  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  rplogsum  27488  dirith2  27489  mudivsum  27491  mulogsumlem  27492  mulogsum  27493  mulog2sumlem1  27495  mulog2sumlem2  27496  vmalogdivsum2  27499  vmalogdivsum  27500  2vmadivsumlem  27501  log2sumbnd  27505  selberglem2  27507  selberg2lem  27511  chpdifbnd  27516  selberg3lem1  27518  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrmax  27525  pntrsumo1  27526  pntrsumbnd  27527  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd1  27547  pntibndlem2a  27551  pntibndlem2  27552  pntibnd  27554  pntlemc  27556  pntlemg  27559  pntlemr  27563  pntlemk  27567  pnt  27575  qabvle  27586  ostth2lem3  27596  ostth2  27598  trgcgrg  28440  tgcgr4  28456  ttgcontlem1  28810  axpaschlem  28865  axlowdimlem16  28882  axcontlem2  28890  axcontlem7  28895  nbusgrvtxm1  29304  upgrewlkle2  29532  pthdlem1  29694  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  wwlksm1edg  29809  wwlksnextproplem2  29838  clwlkclwwlklem2fv1  29922  clwlkclwwlklem2fv2  29923  clwlkclwwlklem2  29927  clwlkclwwlk2  29930  clwwisshclwwslem  29941  clwwlkf1  29976  clwwlkext2edg  29983  clwlknf1oclwwlknlem1  30008  clwwlknonex2lem2  30035  numclwwlk7  30318  frgrreggt1  30320  frgrogt3nreg  30324  smcnlem  30624  nmoub3i  30700  blocnilem  30731  ubthlem2  30798  minvecolem4  30807  htthlem  30844  nmcexi  31953  nmopcoi  32022  stadd3i  32175  cdj1i  32360  nnmulge  32662  receqid  32668  nndiffz1  32709  fzsplit3  32716  nexple  32769  indf1o  32787  wrdt2ind  32875  pmtrto1cl  33056  fzto1st1  33059  fzto1st  33060  psgnfzto1st  33062  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmrn  33100  qsidomlem1  33413  krull  33440  ply1degltel  33550  ply1degltlss  33552  constrnegcl  33743  constrdircl  33745  iconstr  33746  constrrecl  33749  constrmulcl  33751  constrreinvcl  33752  constrresqrtcl  33757  cos9thpiminplylem1  33762  cos9thpiminply  33768  cos9thpinconstrlem1  33769  1smat1  33781  submateqlem1  33784  madjusmdetlem2  33805  unitdivcld  33878  sqsscirc1  33885  esumdivc  34060  dya2ub  34248  dya2iocress  34252  dya2iocbrsiga  34253  dya2icobrsiga  34254  dya2icoseg  34255  dya2iocucvr  34262  sxbrsigalem2  34264  fibp1  34379  probmeasb  34408  dstrvprob  34450  dstfrvunirn  34453  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemsgt1  34489  ballotlemsel1i  34491  ballotlemfrcn0  34508  signsply0  34529  itgexpif  34584  reprlt  34597  chtvalz  34607  breprexplemc  34610  breprexp  34611  circlemeth  34618  tgoldbachgnn  34637  acycgr1v  35117  subfaclim  35156  cvmliftlem2  35254  cvmliftlem13  35264  snmlff  35297  bccolsum  35702  faclim  35709  nn0prpwlem  36286  dnibndlem10  36451  dnibndlem12  36453  knoppcnlem4  36460  unblimceq0  36471  knoppndvlem1  36476  knoppndvlem2  36477  knoppndvlem3  36478  knoppndvlem7  36482  knoppndvlem11  36486  knoppndvlem12  36487  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem18  36493  knoppndvlem20  36495  irrdiff  37290  poimirlem6  37596  poimirlem7  37597  poimirlem15  37605  poimirlem19  37609  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  broucube  37624  itg2addnclem2  37642  itg2addnclem3  37643  areacirclem1  37678  areacirclem4  37681  incsequz  37718  totbndbnd  37759  bfplem2  37793  resdvopclptsd  41987  lcmineqlem2  41989  lcmineqlem3  41990  lcmineqlem10  41997  lcmineqlem12  41999  lcmineqlem15  42002  lcmineqlem18  42005  lcmineqlem19  42006  lcmineqlem20  42007  lcmineqlem22  42009  lcmineqlem23  42010  3lexlogpow5ineq2  42014  3lexlogpow5ineq4  42015  3lexlogpow5ineq3  42016  3lexlogpow2ineq1  42017  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1lem1  42021  dvrelog2  42023  dvrelog3  42024  dvrelog2b  42025  dvrelogpow2b  42027  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p2  42036  aks4d1p3  42037  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8d2  42044  aks4d1p8d3  42045  aks4d1p8  42046  aks4d1p9  42047  posbezout  42059  primrootlekpowne0  42064  primrootspoweq0  42065  aks6d1c1  42075  aks6d1c2p2  42078  hashscontpow1  42080  aks6d1c3  42082  aks6d1c2lem4  42086  aks6d1c2  42089  2np3bcnp1  42103  2ap1caineq  42104  sticksstones6  42110  sticksstones7  42111  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones22  42127  aks6d1c6lem3  42131  aks6d1c6lem4  42132  bcled  42137  bcle2d  42138  aks6d1c7lem1  42139  aks6d1c7lem2  42140  unitscyglem2  42155  unitscyglem4  42157  unitscyglem5  42158  aks5lem8  42160  metakunt1  42164  metakunt2  42165  metakunt7  42170  metakunt15  42178  metakunt16  42179  metakunt24  42187  metakunt28  42191  metakunt29  42192  2xp3dxp2ge1d  42200  factwoffsmonot  42201  sn-1ne2  42262  redvmptabs  42350  sn-00idlem2  42389  sn-0ne2  42396  rei4  42413  sn-0tie0  42429  sn-nnne0  42438  mulgt0b2d  42450  sn-ltmulgt11d  42452  sn-0lt1  42453  sn-mulgt1d  42455  fimgmcyc  42504  flt4lem7  42629  fltnlta  42633  3cubeslem1  42654  3cubeslem3r  42657  3cubeslem4  42659  lzenom  42740  irrapxlem1  42792  irrapxlem2  42793  irrapxlem4  42795  irrapxlem5  42796  pellexlem2  42800  pell1qrge1  42840  pell1qr1  42841  elpell1qr2  42842  pell14qrgapw  42846  pellfundgt1  42853  pellfundglb  42855  pellfundex  42856  pellfundrp  42858  pellfundne1  42859  rmspecsqrtnq  42876  rmspecnonsq  42877  rmspecfund  42879  rmspecpos  42887  monotoddzzfi  42913  rmygeid  42935  areaquad  43187  imo72b2lem0  44136  imo72b2lem1  44140  imo72b2  44143  cvgdvgrat  44285  radcnvrat  44286  hashnzfzclim  44294  lhe4.4ex1a  44301  binomcxplemnn0  44321  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  oddfl  45254  abscosbd  45255  zltlesub  45262  abssinbd  45272  monoords  45274  fzisoeu  45277  fzdifsuc2  45287  suplesup  45314  xralrple2  45329  infxr  45342  infleinflem2  45346  reclt0d  45362  xrralrecnnge  45365  sqrlearg  45530  iooiinioc  45533  fmul01  45557  fmul01lt1lem1  45561  fmul01lt1lem2  45562  climsuselem1  45584  sumnnodd  45607  0ellimcdiv  45626  dvmptidg  45894  dvcosax  45903  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvxpaek  45917  dvnmul  45920  iblspltprt  45950  itgspltprt  45956  stoweidlem5  45982  stoweidlem7  45984  stoweidlem10  45987  stoweidlem11  45988  stoweidlem12  45989  stoweidlem13  45990  stoweidlem14  45991  stoweidlem16  45993  stoweidlem18  45995  stoweidlem20  45997  stoweidlem24  46001  stoweidlem25  46002  stoweidlem34  46011  stoweidlem36  46013  stoweidlem38  46015  stoweidlem40  46017  stoweidlem41  46018  stoweidlem42  46019  stoweidlem45  46022  stoweidlem51  46028  stoweidlem60  46037  wallispilem3  46044  wallispilem4  46045  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  stirlinglem3  46053  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem8  46058  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlinglem15  46065  dirker2re  46069  dirkerval2  46071  dirkerre  46072  dirkertrigeqlem1  46075  dirkertrigeqlem3  46077  dirkeritg  46079  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem5  46089  fourierdlem6  46090  fourierdlem11  46095  fourierdlem15  46099  fourierdlem19  46103  fourierdlem20  46104  fourierdlem24  46108  fourierdlem26  46110  fourierdlem28  46112  fourierdlem30  46114  fourierdlem39  46123  fourierdlem41  46125  fourierdlem43  46127  fourierdlem47  46130  fourierdlem48  46131  fourierdlem56  46139  fourierdlem60  46143  fourierdlem61  46144  fourierdlem62  46145  fourierdlem64  46147  fourierdlem65  46148  fourierdlem66  46149  fourierdlem68  46151  fourierdlem73  46156  fourierdlem78  46161  fourierdlem79  46162  fourierdlem87  46170  fourierdlem103  46186  fourierdlem104  46187  sqwvfoura  46205  fouriersw  46208  etransclem4  46215  etransclem23  46234  etransclem24  46235  etransclem31  46242  etransclem32  46243  etransclem35  46246  etransclem41  46252  etransclem46  46257  etransclem48  46259  etransc  46260  ioorrnopnxrlem  46283  nnfoctbdjlem  46432  iundjiun  46437  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  ovnhoilem1  46578  vonioolem2  46658  vonicclem2  46661  pimrecltneg  46701  smfrec  46766  smfmullem1  46768  smfmullem2  46769  smfdiv  46774  sigaradd  46843  ormkglobd  46852  p1lep2  47277  zm1nn  47279  ceilhalfgt1  47306  2tceilhalfelfzo1  47309  ceilbi  47310  rehalfge1  47312  ceilhalfnn  47313  addmodne  47321  m1mod0mod1  47331  iccpartiltu  47384  iccpartlt  47386  iccpartgt  47389  fmtnoge3  47492  fmtnodvds  47506  fmtnoprmfac2lem1  47528  2pwp1prm  47551  flsqrt  47555  sfprmdvdsmersenne  47565  lighneallem2  47568  lighneallem4a  47570  proththdlem  47575  proththd  47576  nnoALTV  47657  bgoldbtbndlem4  47770  gpgprismgrusgra  48010  gpgedgvtx0  48013  gpgvtxedg0  48015  gpg3nbgrvtxlem  48017  gpg5nbgrvtx03starlem2  48019  gpg3kgrtriexlem4  48036  gpg3kgrtriexlem6  48038  cznnring  48185  divge1b  48436  divgt1b  48437  m1modmmod  48449  difmodm1lt  48450  nn0eo  48456  regt1loggt0  48464  rege1logbrege0  48486  logblt1b  48492  fllog2  48496  nnolog2flm1  48518  dignn0flhalflem1  48543  rrxlinesc  48663  rrxlinec  48664  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  line2ylem  48679  line2  48680  line2xlem  48681  reseccl  49565  recsccl  49566  amgmwlem  49614  amgmlemALT  49615