Theorem 1red 8347

Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1red	|- ( ph -> 1 e. RR )

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 8331	. 2 |- 1 e. RR
2	1	a1i 9	1 |- ( ph -> 1 e. RR )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8184   1c1 8186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-1re 8279

This theorem is used by:  recgt0  9188  ltrec  9221  recp1lt1  9237  indfdc  9307  peano5nni  9316  peano2nn  9325  nn0p1gt0  9603  nn0ge2m1nn  9636  peano2z  9689  suprzclex  9754  ledivge1le  10143  lincmble  10422  iccf1o  10423  zltaddlt1le  10426  fznatpl1  10499  elfz1b  10513  fzonn0p1p1  10647  elfzom1p1elfzo  10648  zssinfcl  10681  exbtwnzlemstep  10698  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2z  10705  qfraclt1  10733  flqaddz  10752  btwnzge0  10755  2tnp1ge0ge0  10756  flhalf  10757  fldiv4lem1div2uz2  10761  modqid  10806  m1modge3gt1  10828  modqltm1p1mod  10833  addmodlteq  10855  seq3f1olemqsumkj  10968  ltexp2a  11048  leexp2a  11049  leexp2r  11050  nnlesq  11100  resq01  11115  bernneq3  11120  expnbnd  11121  expnlbnd2  11123  nn0ltexp2  11168  expcanlem  11174  expcan  11175  bcval5  11222  ssenneg  11301  wrdlenge2n0  11361  sq01  11681  cvg1nlemcau  11771  resqrexlem1arp  11792  resqrexlemf1  11795  resqrexlemover  11797  resqrexlemdecn  11799  resqrexlemlo  11800  resqrexlemcalc2  11802  resqrexlemnm  11805  resqrexlemga  11810  reccn2ap  12103  sumsnf  12200  expcnvre  12294  geolim  12302  geolim2  12303  georeclim  12304  geoisumr  12309  geoisum1c  12311  cvgratnnlembern  12314  cvgratnnlemsumlt  12319  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratnn  12322  cvgratz  12323  prodsnf  12383  fprodrecl  12399  fprodreclf  12405  efcllemp  12449  efgt1  12488  eflegeo  12492  sinltxirr  12552  eirraplem  12568  p1modz1  12585  oddge22np1  12672  ltoddhalfle  12684  nno  12697  nn0oddm1d2  12700  nnoddm1d2  12701  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  bitscmp  12749  bitsinv1lem  12752  uzwodc  12838  coprmgcdb  12890  prmind2  12922  dvdsnprmd  12927  prmdc  12932  isprm5lem  12944  znege1  12982  sqrt2irrap  12984  divdenle  13001  nn0sqrtelqelz  13010  difsqpwdvds  13145  fldivp1  13155  pcfaclem  13156  4sqlem11  13208  4sqlem12  13209  2expltfac  13247  ballotfilemsgt1  13311  ballotfilemsel1i  13313  ballotfilemfrcn0  13330  oddennn  13340  exmidunben  13374  nninfdclemlt  13399  gzsumshift  14238  znidomb  15101  psrbaglesuppg  15170  hoverlt1  15892  ivthdichlem  15894  dveflem  15969  reeff1oleme  16015  reeff1o  16016  efap1p  16022  cosz12  16024  sin0pilem2  16026  cos02pilt1  16096  rplogcl  16126  logdivlti  16128  logdivlt  16141  cxplt  16168  cxple  16169  ltexp2  16194  logbrec  16213  logbgt0b  16219  logbgcd1irr  16220  logbgcd1irraplemexp  16221  logbgcd1irraplemap  16222  zprmlogbaplem1  16232  zprmlogbaplem2  16233  log2tlbndlog2  16237  birthdaylem3  16244  pellexlem2  16247  ppiqltx  16298  ppiqub  16310  chtqub  16313  mersenne  16314  perfectlem2  16317  bcmono  16321  bposlem1  16328  bposlem2  16329  zabsle1  16340  lgslem3  16343  lgsdirprm  16375  gausslemma2dlem1a  16399  lgseisen  16415  lgsquadlem2  16419  2sqlem8  16464  clwwlkext2edg  16885  clwwlknonex2lem2  16901  iooref1o  17306  trilpolemgt1  17312  trilpolemlt1  17314  trilpo  17316  redcwlpo  17329  neapmkvlem  17341  neapmkv  17342  taupi  17347