Theorem 1red 11136

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11028  1c1 11030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  recgt0  11992  mulgt1  12008  ltrec  12029  nnne0  12202  nn0p1gt0  12457  nn0ge2m1nn  12498  nn0le2is012  12584  suprzcl  12600  ledivge1le  13006  ge2halflem1  13050  qbtwnre  13142  lincmb01cmp  13439  iccf1o  13440  xov1plusxeqvd  13442  zltaddlt1le  13449  nnge2recico01  13451  fznatpl1  13523  elfz1b  13538  elfzo0subge1  13651  fzonn0p1p1  13690  elfznelfzo  13719  elfznelfzob  13720  fladdz  13775  2tnp1ge0ge0  13779  flhalf  13780  ltdifltdiv  13784  fldiv4lem1div2uz2  13786  mulp1mod1  13864  m1modge3gt1  13871  modltm1p1mod  13876  addmodlteq  13899  ltexp2a  14119  expcan  14122  ltexp2  14123  leexp2  14124  leexp2a  14125  leexp2r  14127  nnlesq  14158  bernneq3  14184  expnbnd  14185  expnlbnd2  14187  expnngt1  14194  fzsdom2  14381  wrdlenge2n0  14505  swrd2lsw  14905  2swrd2eqwrdeq  14906  01sqrexlem7  15201  rddif  15294  reccn2  15550  rlimo1  15570  o1fsum  15767  abscvgcvg  15773  climcndslem1  15805  flo1  15810  harmonic  15815  geomulcvg  15832  fprodrecl  15909  fprodreclf  15915  fprodle  15952  bpoly4  16015  efcllem  16033  efgt1  16074  tanhlt1  16118  sinltx  16147  eirrlem  16162  p1modz1  16219  mod2eq1n2dvds  16307  oddge22np1  16309  ltoddhalfle  16321  nn0o1gt2  16341  nno  16342  nn0oddm1d2  16345  nnoddm1d2  16346  bitsfzolem  16394  bitsfzo  16395  bitsmod  16396  bitscmp  16398  bitsinv1lem  16401  smuval2  16442  coprmgcdb  16609  prmind2  16645  dvdsnprmd  16650  2mulprm  16653  isprm5  16668  isprm7  16669  divdenle  16710  zsqrtelqelz  16719  fermltl  16745  odzdvds  16757  modprm0  16767  iserodd  16797  difsqpwdvds  16849  pcfaclem  16860  prmreclem1  16878  4sqlem11  16917  4sqlem12  16918  ramub1lem1  16988  prmgaplem8  17020  2expltfac  17054  chnccat  18583  pgpfaclem2  20050  znidomb  21551  psdmvr  22145  chfacfisf  22829  chfacfisfcpmat  22830  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  nrginvrcnlem  24666  nmoid  24717  xrsmopn  24788  metnrmlem1a  24834  iihalf2cn  24911  iccpnfhmeo  24922  lebnumii  24943  htpycc  24957  pcohtpylem  24996  pcoass  25001  pcorevlem  25003  nmhmcn  25097  cncmet  25299  ovoliunlem1  25479  dyadmaxlem  25574  vitalilem2  25586  mbfi1fseqlem6  25697  itg2mulc  25724  itg2monolem1  25727  itg2monolem3  25729  dveflem  25956  mvth  25969  dvlipcn  25971  lhop1lem  25990  dvfsumlem1  26003  dvfsumlem2  26004  dvfsumlem3  26005  dvfsumlem4  26006  dvfsum2  26011  fta1glem2  26144  plyeq0lem  26185  fta1lem  26284  vieta1lem2  26288  aalioulem3  26311  aalioulem4  26312  radcnvlem1  26391  radcnvlem2  26392  dvradcnv  26399  abelthlem2  26410  abelthlem5  26413  abelthlem7  26416  abelth2  26420  cos02pilt1  26503  cosne0  26506  rplogcl  26581  logdivlti  26597  logno1  26613  dvlog2lem  26629  advlog  26631  logtayllem  26636  cxplt  26671  cxple  26672  cxpaddlelem  26728  cxpaddle  26729  rtprmirr  26737  relogbf  26768  logbgt0b  26770  isosctrlem1  26795  isosctrlem2  26796  chordthmlem4  26812  heron  26815  atanlogaddlem  26890  bndatandm  26906  leibpi  26919  log2tlbnd  26922  birthdaylem3  26930  rlimcnp  26942  rlimcnp2  26943  efrlim  26946  efrlimOLD  26947  cxp2limlem  26953  cxp2lim  26954  divsqrtsumo1  26961  jensenlem2  26965  logdiflbnd  26972  fsumharmonic  26989  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem4  27009  lgamgulmlem5  27010  lgamgulmlem6  27011  lgamcvg2  27032  regamcl  27038  wilthlem2  27046  ftalem2  27051  basellem9  27066  vma1  27143  ppieq0  27153  mumullem2  27157  fsumfldivdiaglem  27166  chpeq0  27185  chtub  27189  chpval2  27195  chpchtsum  27196  chpub  27197  logfacrlim  27201  logexprlim  27202  mersenne  27204  perfectlem2  27207  dchrelbas4  27220  bcmono  27254  bposlem1  27261  bposlem2  27262  zabsle1  27273  lgslem3  27276  lgsmod  27300  lgsdir2lem4  27305  lgsdirprm  27308  gausslemma2dlem1a  27342  gausslemma2d  27351  lgsquadlem2  27358  2sqlem8  27403  chebbnd1lem1  27446  chebbnd1lem2  27447  chtppilimlem1  27450  chebbnd2  27454  chto1lb  27455  chpchtlim  27456  chpo1ubb  27458  vmadivsum  27459  rplogsumlem1  27461  rpvmasumlem  27464  dchrisumlem3  27468  dchrmusumlema  27470  dchrmusum2  27471  dchrvmasumlem2  27475  dchrvmasumlem3  27476  dchrvmasumiflem1  27478  dchrvmasumiflem2  27479  dchrisum0flblem1  27485  dchrisum0flblem2  27486  dchrisum0fno1  27488  dchrisum0re  27490  dchrisum0lema  27491  dchrisum0lem1b  27492  dchrisum0lem2a  27494  dchrisum0lem2  27495  dchrisum0lem3  27496  rplogsum  27504  dirith2  27505  mudivsum  27507  mulogsumlem  27508  mulogsum  27509  mulog2sumlem1  27511  mulog2sumlem2  27512  vmalogdivsum2  27515  vmalogdivsum  27516  2vmadivsumlem  27517  log2sumbnd  27521  selberglem2  27523  selberg2lem  27527  chpdifbnd  27532  selberg3lem1  27534  selberg3  27536  selberg4lem1  27537  selberg4  27538  pntrmax  27541  pntrsumo1  27542  pntrsumbnd  27543  selberg3r  27546  selberg4r  27547  selberg34r  27548  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntrlog2bnd  27561  pntpbnd1a  27562  pntpbnd1  27563  pntibndlem2a  27567  pntibndlem2  27568  pntibnd  27570  pntlemc  27572  pntlemg  27575  pntlemr  27579  pntlemk  27583  pnt  27591  qabvle  27602  ostth2lem3  27612  ostth2  27614  trgcgrg  28597  tgcgr4  28613  ttgcontlem1  28967  axpaschlem  29023  axlowdimlem16  29040  axcontlem2  29048  axcontlem7  29053  nbusgrvtxm1  29462  upgrewlkle2  29690  pthdlem1  29849  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  wwlksm1edg  29964  wwlksnextproplem2  29993  clwlkclwwlklem2fv1  30080  clwlkclwwlklem2fv2  30081  clwlkclwwlklem2  30085  clwlkclwwlk2  30088  clwwisshclwwslem  30099  clwwlkf1  30134  clwwlkext2edg  30141  clwlknf1oclwwlknlem1  30166  clwwlknonex2lem2  30193  numclwwlk7  30476  frgrreggt1  30478  frgrogt3nreg  30482  smcnlem  30783  nmoub3i  30859  blocnilem  30890  ubthlem2  30957  minvecolem4  30966  htthlem  31003  nmcexi  32112  nmopcoi  32181  stadd3i  32334  cdj1i  32519  nnmulge  32827  receqid  32832  nndiffz1  32874  fzsplit3  32881  nexple  32932  indf1o  32939  wrdt2ind  33028  pmtrto1cl  33175  fzto1st1  33178  fzto1st  33179  psgnfzto1st  33181  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmrn  33219  qsidomlem1  33527  krull  33554  ply1degltel  33669  ply1degltlss  33671  constrnegcl  33923  constrdircl  33925  iconstr  33926  constrrecl  33929  constrmulcl  33931  constrreinvcl  33932  constrresqrtcl  33937  cos9thpiminplylem1  33942  cos9thpiminply  33948  cos9thpinconstrlem1  33949  1smat1  33964  submateqlem1  33967  madjusmdetlem2  33988  unitdivcld  34061  sqsscirc1  34068  esumdivc  34243  dya2ub  34430  dya2iocress  34434  dya2iocbrsiga  34435  dya2icobrsiga  34436  dya2icoseg  34437  dya2iocucvr  34444  sxbrsigalem2  34446  fibp1  34561  probmeasb  34590  dstrvprob  34632  dstfrvunirn  34635  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemsgt1  34671  ballotlemsel1i  34673  ballotlemfrcn0  34690  signsply0  34711  itgexpif  34766  reprlt  34779  chtvalz  34789  breprexplemc  34792  breprexp  34793  circlemeth  34800  tgoldbachgnn  34819  acycgr1v  35347  subfaclim  35386  cvmliftlem2  35484  cvmliftlem13  35494  snmlff  35527  bccolsum  35937  faclim  35944  nn0prpwlem  36520  dnibndlem10  36763  dnibndlem12  36765  knoppcnlem4  36772  unblimceq0  36783  knoppndvlem1  36788  knoppndvlem2  36789  knoppndvlem3  36790  knoppndvlem7  36794  knoppndvlem11  36798  knoppndvlem12  36799  knoppndvlem14  36801  knoppndvlem15  36802  knoppndvlem17  36804  knoppndvlem18  36805  knoppndvlem20  36807  irrdiff  37656  poimirlem6  37961  poimirlem7  37962  poimirlem15  37970  poimirlem19  37974  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  broucube  37989  itg2addnclem2  38007  itg2addnclem3  38008  areacirclem1  38043  areacirclem4  38046  incsequz  38083  totbndbnd  38124  bfplem2  38158  resdvopclptsd  42481  lcmineqlem2  42483  lcmineqlem3  42484  lcmineqlem10  42491  lcmineqlem12  42493  lcmineqlem15  42496  lcmineqlem18  42499  lcmineqlem19  42500  lcmineqlem20  42501  lcmineqlem22  42503  lcmineqlem23  42504  3lexlogpow5ineq2  42508  3lexlogpow5ineq4  42509  3lexlogpow5ineq3  42510  3lexlogpow2ineq1  42511  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1lem1  42515  dvrelog2  42517  dvrelog3  42518  dvrelog2b  42519  dvrelogpow2b  42521  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8d2  42538  aks4d1p8d3  42539  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  primrootlekpowne0  42558  primrootspoweq0  42559  aks6d1c1  42569  aks6d1c2p2  42572  hashscontpow1  42574  aks6d1c3  42576  aks6d1c2lem4  42580  aks6d1c2  42583  2np3bcnp1  42597  2ap1caineq  42598  sticksstones6  42604  sticksstones7  42605  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones22  42621  aks6d1c6lem3  42625  aks6d1c6lem4  42626  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  aks6d1c7lem2  42634  unitscyglem2  42649  unitscyglem4  42651  unitscyglem5  42652  aks5lem8  42654  sn-1ne2  42717  redvmptabs  42806  sn-00idlem2  42845  sn-0ne2  42852  rei4  42870  rediveq1d  42897  sn-rediv1d  42898  sn-rereccld  42901  rerecne0d  42902  rerecidd  42903  rerecrecd  42905  sn-0tie0  42910  sn-nnne0  42919  mulgt0b1d  42931  sn-ltmulgt11d  42933  sn-0lt1  42934  sn-mulgt1d  42938  fimgmcyc  42993  flt4lem7  43106  fltnlta  43110  3cubeslem1  43130  3cubeslem3r  43133  3cubeslem4  43135  lzenom  43216  irrapxlem1  43268  irrapxlem2  43269  irrapxlem4  43271  irrapxlem5  43272  pellexlem2  43276  pell1qrge1  43316  pell1qr1  43317  elpell1qr2  43318  pell14qrgapw  43322  pellfundgt1  43329  pellfundglb  43331  pellfundex  43332  pellfundrp  43334  pellfundne1  43335  rmspecsqrtnq  43352  rmspecnonsq  43353  rmspecfund  43355  rmspecpos  43362  monotoddzzfi  43388  rmygeid  43410  areaquad  43662  imo72b2lem0  44610  imo72b2lem1  44614  imo72b2  44617  cvgdvgrat  44758  radcnvrat  44759  hashnzfzclim  44767  lhe4.4ex1a  44774  binomcxplemnn0  44794  binomcxplemdvbinom  44798  binomcxplemnotnn0  44801  oddfl  45729  abscosbd  45730  zltlesub  45736  abssinbd  45746  monoords  45748  fzisoeu  45751  fzdifsuc2  45761  suplesup  45787  xralrple2  45802  infxr  45814  infleinflem2  45818  reclt0d  45834  xrralrecnnge  45837  sqrlearg  46001  iooiinioc  46004  fmul01  46028  fmul01lt1lem1  46032  fmul01lt1lem2  46033  climsuselem1  46055  sumnnodd  46078  0ellimcdiv  46095  dvmptidg  46363  dvcosax  46372  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvxpaek  46386  dvnmul  46389  iblspltprt  46419  itgspltprt  46425  stoweidlem5  46451  stoweidlem7  46453  stoweidlem10  46456  stoweidlem11  46457  stoweidlem12  46458  stoweidlem13  46459  stoweidlem14  46460  stoweidlem16  46462  stoweidlem18  46464  stoweidlem20  46466  stoweidlem24  46470  stoweidlem25  46471  stoweidlem34  46480  stoweidlem36  46482  stoweidlem38  46484  stoweidlem40  46486  stoweidlem41  46487  stoweidlem42  46488  stoweidlem45  46491  stoweidlem51  46497  stoweidlem60  46506  wallispilem3  46513  wallispilem4  46514  wallispilem5  46515  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  wallispi2  46519  stirlinglem1  46520  stirlinglem3  46522  stirlinglem5  46524  stirlinglem6  46525  stirlinglem7  46526  stirlinglem8  46527  stirlinglem10  46529  stirlinglem11  46530  stirlinglem12  46531  stirlinglem13  46532  stirlinglem15  46534  dirker2re  46538  dirkerval2  46540  dirkerre  46541  dirkertrigeqlem1  46544  dirkertrigeqlem3  46546  dirkeritg  46548  dirkercncflem1  46549  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem5  46558  fourierdlem6  46559  fourierdlem11  46564  fourierdlem15  46568  fourierdlem19  46572  fourierdlem20  46573  fourierdlem24  46577  fourierdlem26  46579  fourierdlem28  46581  fourierdlem30  46583  fourierdlem39  46592  fourierdlem41  46594  fourierdlem43  46596  fourierdlem47  46599  fourierdlem48  46600  fourierdlem56  46608  fourierdlem60  46612  fourierdlem61  46613  fourierdlem62  46614  fourierdlem64  46616  fourierdlem65  46617  fourierdlem66  46618  fourierdlem68  46620  fourierdlem73  46625  fourierdlem78  46630  fourierdlem79  46631  fourierdlem87  46639  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  fouriersw  46677  etransclem4  46684  etransclem23  46703  etransclem24  46704  etransclem31  46711  etransclem32  46712  etransclem35  46715  etransclem41  46721  etransclem46  46726  etransclem48  46728  etransc  46729  ioorrnopnxrlem  46752  nnfoctbdjlem  46901  iundjiun  46906  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  ovnhoilem1  47047  vonioolem2  47127  vonicclem2  47130  pimrecltneg  47170  smfrec  47235  smfmullem1  47237  smfmullem2  47238  smfdiv  47243  sigaradd  47312  ormkglobd  47321  cjnpoly  47349  p1lep2  47760  zm1nn  47762  ceilhalfgt1  47793  2tceilhalfelfzo1  47796  ceilbi  47797  rehalfge1  47799  ceilhalfnn  47800  flmrecm1  47803  addmodne  47810  m1mod0mod1  47820  m1modmmod  47824  difmodm1lt  47825  modmknepk  47828  modp2nep1  47833  modm1nem2  47835  2timesltsqm1  47839  muldvdsfacm1  47847  iccpartiltu  47894  iccpartlt  47896  iccpartgt  47899  fmtnoge3  48005  fmtnodvds  48019  fmtnoprmfac2lem1  48041  2pwp1prm  48064  flsqrt  48068  sfprmdvdsmersenne  48078  lighneallem2  48081  lighneallem4a  48083  proththdlem  48088  proththd  48089  nprmdvdsfacm1lem4  48098  nnoALTV  48183  bgoldbtbndlem4  48296  gpgprismgrusgra  48546  gpgedgvtx0  48549  gpgvtxedg0  48551  gpg5nbgrvtx03starlem2  48557  gpg3kgrtriexlem4  48574  gpg3kgrtriexlem6  48576  cznnring  48750  divge1b  49000  divgt1b  49001  nn0eo  49016  regt1loggt0  49024  rege1logbrege0  49046  logblt1b  49052  fllog2  49056  nnolog2flm1  49078  dignn0flhalflem1  49103  rrxlinesc  49223  rrxlinec  49224  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  line2ylem  49239  line2  49240  line2xlem  49241  reseccl  50240  recsccl  50241  amgmwlem  50289  amgmlemALT  50290