Theorem 1red 11290

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

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

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 2733  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-mulrcl 11244  ax-i2m1 11249  ax-1ne0 11250  ax-rrecex 11253  ax-cnre 11254

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 6487  df-fv 6539  df-ov 7415

This theorem is used by:  recgt0  12144  mulgt1  12159  ltrec  12180  nnne0  12353  nn0p1gt0  12616  nn0ge2m1nn  12657  nn0le2is012  12744  suprzcl  12760  ledivge1le  13174  ge2halflem1  13218  qbtwnre  13310  lincmb01cmp  13607  iccf1o  13608  xov1plusxeqvd  13610  zltaddlt1le  13617  nnge2recico01  13619  fznatpl1  13692  elfz1b  13707  elfzo0subge1  13820  fzonn0p1p1  13859  elfznelfzo  13888  elfznelfzob  13889  fladdz  13945  2tnp1ge0ge0  13949  flhalf  13950  ltdifltdiv  13954  fldiv4lem1div2uz2  13956  mulp1mod1  14034  m1modge3gt1  14041  modltm1p1mod  14046  addmodlteq  14069  ltexp2a  14289  expcan  14292  ltexp2  14293  leexp2  14294  leexp2a  14295  leexp2r  14297  nnlesq  14329  bernneq3  14355  expnbnd  14356  expnlbnd2  14358  expnngt1  14365  fzsdom2  14553  wrdlenge2n0  14677  swrd2lsw  15085  2swrd2eqwrdeq  15086  01sqrexlem7  15395  rddif  15488  reccn2  15744  rlimo1  15764  o1fsum  15960  abscvgcvg  15966  climcndslem1  15998  flo1  16003  harmonic  16008  geomulcvg  16025  fprodrecl  16100  fprodreclf  16106  fprodle  16143  bpoly4  16205  efcllem  16223  efgt1  16264  tanhlt1  16308  sinltx  16337  eirrlem  16352  p1modz1  16409  mod2eq1n2dvds  16497  oddge22np1  16499  ltoddhalfle  16511  nn0o1gt2  16531  nno  16532  nn0oddm1d2  16535  nnoddm1d2  16536  bitsfzolem  16584  bitsfzo  16585  bitsmod  16586  bitscmp  16588  bitsinv1lem  16591  smuval2  16632  coprmgcdb  16804  prmind2  16840  dvdsnprmd  16845  2mulprm  16848  isprm5  16863  isprm7  16864  divdenle  16905  zsqrtelqelz  16914  fermltl  16941  odzdvds  16953  modprm0  16963  iserodd  16993  difsqpwdvds  17045  pcfaclem  17056  prmreclem1  17074  4sqlem11  17113  4sqlem12  17114  ramub1lem1  17184  prmgaplem8  17216  2expltfac  17250  chnccat  18780  pgpfaclem2  20278  qsidomlem1  21616  znidomb  21847  psdmvr  22470  chfacfisf  23152  chfacfisfcpmat  23153  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  nrginvrcnlem  24990  nmoid  25041  xrsmopn  25112  metnrmlem1a  25158  iihalf2cn  25235  iccpnfhmeo  25246  lebnumii  25267  htpycc  25281  pcohtpylem  25320  pcoass  25325  pcorevlem  25327  nmhmcn  25421  cncmet  25623  ovoliunlem1  25803  dyadmaxlem  25898  vitalilem2  25910  mbfi1fseqlem6  26021  itg2mulc  26048  itg2monolem1  26051  itg2monolem3  26053  dveflem  26279  mvth  26292  dvlipcn  26294  lhop1lem  26313  dvfsumlem1  26326  dvfsumlem2  26327  dvfsumlem3  26328  dvfsumlem4  26329  dvfsum2  26334  fta1glem2  26467  plyeq0lem  26509  fta1lem  26610  vieta1lem2  26616  aalioulem3  26643  aalioulem4  26644  radcnvlem1  26722  radcnvlem2  26723  dvradcnv  26730  abelthlem2  26741  abelthlem5  26744  abelthlem7  26747  abelth2  26751  cos02pilt1  26836  cosne0  26839  rplogcl  26914  logdivlti  26930  logno1  26946  dvlog2lem  26962  advlog  26964  logtayllem  26969  cxplt  27004  cxple  27005  cxpaddlelem  27061  cxpaddle  27062  rtprmirr  27070  relogbf  27101  logbgt0b  27103  isosctrlem1  27128  isosctrlem2  27129  chordthmlem4  27145  heron  27148  atanlogaddlem  27223  bndatandm  27239  leibpi  27252  log2tlbnd  27255  birthdaylem3  27263  rlimcnp  27275  rlimcnp2  27276  efrlim  27279  cxp2limlem  27285  cxp2lim  27286  divsqrtsumo1  27293  jensenlem2  27297  logdiflbnd  27304  fsumharmonic  27321  lgamgulmlem2  27339  lgamgulmlem3  27340  lgamgulmlem4  27341  lgamgulmlem5  27342  lgamgulmlem6  27343  lgamcvg2  27364  regamcl  27370  wilthlem2  27378  ftalem2  27383  basellem9  27398  vma1  27475  ppieq0  27485  mumullem2  27489  fsumfldivdiaglem  27498  ppiub  27513  chpeq0  27517  chtub  27521  chpval2  27527  chpchtsum  27528  chpub  27529  logfacrlim  27533  logexprlim  27534  mersenne  27536  perfectlem2  27539  dchrelbas4  27552  bcmono  27586  bposlem1  27593  bposlem2  27594  zabsle1  27605  lgslem3  27608  lgsmod  27632  lgsdir2lem4  27637  lgsdirprm  27640  gausslemma2dlem1a  27674  gausslemma2d  27683  lgsquadlem2  27690  2sqlem8  27735  chebbnd1lem1  27778  chebbnd1lem2  27779  chtppilimlem1  27782  chebbnd2  27786  chto1lb  27787  chpchtlim  27788  chpo1ubb  27790  vmadivsum  27791  rplogsumlem1  27793  rpvmasumlem  27796  dchrisumlem3  27800  dchrmusumlema  27802  dchrmusum2  27803  dchrvmasumlem2  27807  dchrvmasumlem3  27808  dchrvmasumiflem1  27810  dchrvmasumiflem2  27811  dchrisum0flblem1  27817  dchrisum0flblem2  27818  dchrisum0fno1  27820  dchrisum0re  27822  dchrisum0lema  27823  dchrisum0lem1b  27824  dchrisum0lem2a  27826  dchrisum0lem2  27827  dchrisum0lem3  27828  rplogsum  27836  dirith2  27837  mudivsum  27839  mulogsumlem  27840  mulogsum  27841  mulog2sumlem1  27843  mulog2sumlem2  27844  vmalogdivsum2  27847  vmalogdivsum  27848  2vmadivsumlem  27849  log2sumbnd  27853  selberglem2  27855  selberg2lem  27859  chpdifbnd  27864  selberg3lem1  27866  selberg3  27868  selberg4lem1  27869  selberg4  27870  pntrmax  27873  pntrsumo1  27874  pntrsumbnd  27875  selberg3r  27878  selberg4r  27879  selberg34r  27880  pntrlog2bndlem1  27886  pntrlog2bndlem2  27887  pntrlog2bndlem3  27888  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  pntrlog2bndlem6  27892  pntrlog2bnd  27893  pntpbnd1a  27894  pntpbnd1  27895  pntibndlem2a  27899  pntibndlem2  27900  pntibnd  27902  pntlemc  27904  pntlemg  27907  pntlemr  27911  pntlemk  27915  pnt  27923  qabvle  27934  ostth2lem3  27944  ostth2  27946  flt4lem7  27971  trgcgrg  28960  tgcgr4  28976  ttgcontlem1  29444  axpaschlem  29500  axlowdimlem16  29517  axcontlem2  29525  axcontlem7  29530  nbusgrvtxm1  29942  upgrewlkle2  30169  pthdlem1  30334  crctcshwlkn0lem3  30383  crctcshwlkn0lem5  30385  wwlksm1edg  30452  wwlksnextproplem2  30481  clwlkclwwlklem2fv1  30568  clwlkclwwlklem2fv2  30569  clwlkclwwlklem2  30573  clwlkclwwlk2  30576  clwwisshclwwslem  30587  clwwlkf1  30622  clwwlkext2edg  30629  clwlknf1oclwwlknlem1  30654  clwwlknonex2lem2  30681  numclwwlk7  30974  frgrreggt1  30976  frgrogt3nreg  30980  smcnlem  31281  nmoub3i  31357  blocnilem  31388  ubthlem2  31455  minvecolem4  31464  htthlem  31501  nmcexi  32610  nmopcoi  32679  stadd3i  32832  cdj1i  33017  nnmulge  33313  receqid  33318  nndiffz1  33360  fzsplit3  33367  nexple  33406  indf1o  33413  wrdt2ind  33498  pmtrto1cl  33642  fzto1st1  33645  fzto1st  33646  psgnfzto1st  33648  cycpmco2lem6  33674  cycpmco2lem7  33675  cycpmrn  33686  krull  33985  ply1degltel  34108  ply1degltlss  34110  constrnegcl  34377  constrdircl  34379  iconstr  34380  constrrecl  34383  constrmulcl  34385  constrreinvcl  34386  constrresqrtcl  34391  cos9thpiminplylem1  34396  cos9thpiminply  34402  cos9thpinconstrlem1  34403  1smat1  34418  submateqlem1  34421  madjusmdetlem2  34442  unitdivcld  34515  sqsscirc1  34522  esumdivc  34697  dya2ub  34885  dya2iocress  34889  dya2iocbrsiga  34890  dya2icobrsiga  34891  dya2icoseg  34892  dya2iocucvr  34899  sxbrsigalem2  34901  fibp1  35016  probmeasb  35045  dstrvprob  35087  dstfrvunirn  35090  ballotlemfc0  35108  ballotlemfcc  35109  ballotlemsgt1  35126  ballotlemsel1i  35128  ballotlemfrcn0  35145  signsply0  35163  itgexpif  35218  reprlt  35231  chtvalz  35241  breprexplemc  35244  breprexp  35245  circlemeth  35252  tgoldbachgnn  35271  acycgr1v  35883  subfaclim  35922  cvmliftlem2  36020  cvmliftlem13  36030  snmlff  36063  bccolsum  36473  faclim  36480  nn0prpwlem  37080  dnibndlem10  37323  dnibndlem12  37325  knoppcnlem4  37332  unblimceq0  37343  knoppndvlem1  37348  knoppndvlem2  37349  knoppndvlem3  37350  knoppndvlem7  37354  knoppndvlem11  37358  knoppndvlem12  37359  knoppndvlem14  37361  knoppndvlem15  37362  knoppndvlem17  37364  knoppndvlem18  37365  knoppndvlem20  37367  irrdiff  38215  poimirlem6  38512  poimirlem7  38513  poimirlem15  38521  poimirlem19  38525  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  poimirlem32  38538  broucube  38540  itg2addnclem2  38558  itg2addnclem3  38559  areacirclem1  38594  areacirclem4  38597  incsequz  38650  totbndbnd  38691  bfplem2  38725  resdvopclptsd  43046  lcmineqlem2  43048  lcmineqlem3  43049  lcmineqlem10  43056  lcmineqlem12  43058  lcmineqlem15  43061  lcmineqlem18  43064  lcmineqlem19  43065  lcmineqlem20  43066  lcmineqlem22  43068  lcmineqlem23  43069  3lexlogpow5ineq2  43073  3lexlogpow5ineq4  43074  3lexlogpow5ineq3  43075  3lexlogpow2ineq1  43076  3lexlogpow2ineq2  43077  3lexlogpow5ineq5  43078  aks4d1lem1  43080  dvrelog2  43082  dvrelog3  43083  dvrelog2b  43084  dvrelogpow2b  43086  aks4d1p1p3  43087  aks4d1p1p2  43088  aks4d1p1p4  43089  aks4d1p1p6  43091  aks4d1p1p7  43092  aks4d1p1p5  43093  aks4d1p1  43094  aks4d1p2  43095  aks4d1p3  43096  aks4d1p5  43098  aks4d1p6  43099  aks4d1p7d1  43100  aks4d1p7  43101  aks4d1p8d2  43103  aks4d1p8d3  43104  aks4d1p8  43105  aks4d1p9  43106  posbezout  43118  primrootlekpowne0  43123  primrootspoweq0  43124  aks6d1c1  43134  aks6d1c2p2  43137  hashscontpow1  43139  aks6d1c3  43141  aks6d1c2lem4  43145  aks6d1c2  43148  2np3bcnp1  43162  2ap1caineq  43163  sticksstones6  43169  sticksstones7  43170  sticksstones10  43173  sticksstones12a  43175  sticksstones12  43176  sticksstones22  43186  aks6d1c6lem3  43190  aks6d1c6lem4  43191  bcled  43196  bcle2d  43197  aks6d1c7lem1  43198  aks6d1c7lem2  43199  unitscyglem2  43214  unitscyglem4  43216  unitscyglem5  43217  aks5lem8  43219  sn-1ne2  43298  redvmptabs  43379  sn-00idlem2  43418  sn-0ne2  43425  rei4  43443  rediveq1d  43470  sn-rediv1d  43471  sn-rereccld  43474  rerecne0d  43475  rerecidd  43476  rerecrecd  43478  sn-0tie0  43483  sn-nnne0  43492  mulgt0b1d  43504  sn-ltmulgt11d  43506  sn-0lt1  43507  sn-mulgt1d  43511  fimgmcyc  43560  fltnlta  43628  3cubeslem1  43648  3cubeslem3r  43651  3cubeslem4  43653  lzenom  43734  irrapxlem1  43782  irrapxlem2  43783  irrapxlem4  43785  irrapxlem5  43786  pellexlem2  43790  pell1qrge1  43830  pell1qr1  43831  elpell1qr2  43832  pell14qrgapw  43836  pellfundgt1  43843  pellfundglb  43845  pellfundex  43846  pellfundrp  43848  pellfundne1  43849  rmspecsqrtnq  43866  rmspecnonsq  43867  rmspecfund  43869  rmspecpos  43876  monotoddzzfi  43902  rmygeid  43924  areaquad  44176  imo72b2lem0  45124  imo72b2lem1  45128  imo72b2  45131  cvgdvgrat  45256  radcnvrat  45257  hashnzfzclim  45265  lhe4.4ex1a  45272  binomcxplemnn0  45292  binomcxplemdvbinom  45296  binomcxplemnotnn0  45299  oddfl  46237  abscosbd  46238  zltlesub  46244  abssinbd  46254  monoords  46256  fzisoeu  46259  fzdifsuc2  46269  suplesup  46295  xralrple2  46310  infxr  46322  infleinflem2  46326  reclt0d  46342  xrralrecnnge  46345  sqrlearg  46509  iooiinioc  46512  fmul01  46536  fmul01lt1lem1  46540  fmul01lt1lem2  46541  climsuselem1  46563  sumnnodd  46586  0ellimcdiv  46603  dvmptidg  46871  dvcosax  46880  ioodvbdlimc1lem1  46885  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvxpaek  46894  dvnmul  46897  iblspltprt  46927  itgspltprt  46933  stoweidlem5  46959  stoweidlem7  46961  stoweidlem10  46964  stoweidlem11  46965  stoweidlem12  46966  stoweidlem13  46967  stoweidlem14  46968  stoweidlem16  46970  stoweidlem18  46972  stoweidlem20  46974  stoweidlem24  46978  stoweidlem25  46979  stoweidlem34  46988  stoweidlem36  46990  stoweidlem38  46992  stoweidlem40  46994  stoweidlem41  46995  stoweidlem42  46996  stoweidlem45  46999  stoweidlem51  47005  stoweidlem60  47014  wallispilem3  47021  wallispilem4  47022  wallispilem5  47023  wallispi  47024  wallispi2lem1  47025  wallispi2lem2  47026  wallispi2  47027  stirlinglem1  47028  stirlinglem3  47030  stirlinglem5  47032  stirlinglem6  47033  stirlinglem7  47034  stirlinglem8  47035  stirlinglem10  47037  stirlinglem11  47038  stirlinglem12  47039  stirlinglem13  47040  stirlinglem15  47042  dirker2re  47046  dirkerval2  47048  dirkerre  47049  dirkertrigeqlem1  47052  dirkertrigeqlem3  47054  dirkeritg  47056  dirkercncflem1  47057  dirkercncflem2  47058  dirkercncflem4  47060  fourierdlem5  47066  fourierdlem6  47067  fourierdlem11  47072  fourierdlem15  47076  fourierdlem19  47080  fourierdlem20  47081  fourierdlem24  47085  fourierdlem26  47087  fourierdlem28  47089  fourierdlem30  47091  fourierdlem39  47100  fourierdlem41  47102  fourierdlem43  47104  fourierdlem47  47107  fourierdlem48  47108  fourierdlem56  47116  fourierdlem60  47120  fourierdlem61  47121  fourierdlem62  47122  fourierdlem64  47124  fourierdlem65  47125  fourierdlem66  47126  fourierdlem68  47128  fourierdlem73  47133  fourierdlem78  47138  fourierdlem79  47139  fourierdlem87  47147  fourierdlem103  47163  fourierdlem104  47164  sqwvfoura  47182  fouriersw  47185  etransclem4  47192  etransclem23  47211  etransclem24  47212  etransclem31  47219  etransclem32  47220  etransclem35  47223  etransclem41  47229  etransclem46  47234  etransclem48  47236  etransc  47237  ioorrnopnxrlem  47260  nnfoctbdjlem  47409  iundjiun  47414  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  hoidmvlelem4  47552  ovnhoilem1  47555  vonioolem2  47635  vonicclem2  47638  pimrecltneg  47678  smfrec  47743  smfmullem1  47745  smfmullem2  47746  smfdiv  47751  sigaradd  47820  ormkglobd  47831  cjnpoly  47883  p1lep2  48314  zm1nn  48316  ceilhalfgt1  48347  2tceilhalfelfzo1  48350  ceilbi  48351  rehalfge1  48353  ceilhalfnn  48354  flmrecm1  48357  addmodne  48364  m1mod0mod1  48374  m1modmmod  48378  difmodm1lt  48379  modmknepk  48382  modp2nep1  48387  modm1nem2  48389  2timesltsqm1  48393  muldvdsfacm1  48401  iccpartiltu  48448  iccpartlt  48450  iccpartgt  48453  fmtnoge3  48559  fmtnodvds  48573  fmtnoprmfac2lem1  48595  2pwp1prm  48618  flsqrt  48622  sfprmdvdsmersenne  48632  lighneallem2  48635  lighneallem4a  48637  proththdlem  48642  proththd  48643  nprmdvdsfacm1lem4  48652  nnoALTV  48737  bgoldbtbndlem4  48850  gpgprismgrusgra  49100  gpgedgvtx0  49103  gpgvtxedg0  49105  gpg5nbgrvtx03starlem2  49111  gpg3kgrtriexlem4  49128  gpg3kgrtriexlem6  49130  cznnring  49303  divge1b  49568  divgt1b  49569  nn0eo  49584  regt1loggt0  49592  rege1logbrege0  49614  logblt1b  49620  fllog2  49624  nnolog2flm1  49646  dignn0flhalflem1  49671  rrxlinesc  49791  rrxlinec  49792  eenglngeehlnmlem1  49793  eenglngeehlnmlem2  49794  line2ylem  49807  line2  49808  line2xlem  49809  reseccl  50790  recsccl  50791  amgmwlem  50931  amgmlemALT  50932