Theorem 1red 8341

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 8325	. 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 8178   1c1 8180

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

This theorem is used by:  recgt0  9182  ltrec  9215  recp1lt1  9231  indfdc  9300  peano5nni  9309  peano2nn  9318  nn0p1gt0  9596  nn0ge2m1nn  9631  peano2z  9684  suprzclex  9748  ledivge1le  10137  lincmble  10416  iccf1o  10417  zltaddlt1le  10420  fznatpl1  10493  elfz1b  10507  fzonn0p1p1  10641  elfzom1p1elfzo  10642  zssinfcl  10675  exbtwnzlemstep  10692  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2z  10699  qfraclt1  10727  flqaddz  10745  btwnzge0  10748  2tnp1ge0ge0  10749  flhalf  10750  fldiv4lem1div2uz2  10754  modqid  10799  m1modge3gt1  10821  modqltm1p1mod  10826  addmodlteq  10848  seq3f1olemqsumkj  10961  ltexp2a  11041  leexp2a  11042  leexp2r  11043  nnlesq  11093  resq01  11108  bernneq3  11113  expnbnd  11114  expnlbnd2  11116  nn0ltexp2  11161  expcanlem  11167  expcan  11168  bcval5  11215  ssenneg  11294  wrdlenge2n0  11354  sq01  11674  cvg1nlemcau  11764  resqrexlem1arp  11785  resqrexlemf1  11788  resqrexlemover  11790  resqrexlemdecn  11792  resqrexlemlo  11793  resqrexlemcalc2  11795  resqrexlemnm  11798  resqrexlemga  11803  reccn2ap  12095  sumsnf  12192  expcnvre  12286  geolim  12294  geolim2  12295  georeclim  12296  geoisumr  12301  geoisum1c  12303  cvgratnnlembern  12306  cvgratnnlemsumlt  12311  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratnn  12314  cvgratz  12315  prodsnf  12375  fprodrecl  12391  fprodreclf  12397  efcllemp  12441  efgt1  12480  eflegeo  12484  sinltxirr  12544  eirraplem  12560  p1modz1  12577  oddge22np1  12664  ltoddhalfle  12676  nno  12689  nn0oddm1d2  12692  nnoddm1d2  12693  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitscmp  12741  bitsinv1lem  12744  uzwodc  12830  coprmgcdb  12882  prmind2  12914  dvdsnprmd  12919  prmdc  12924  isprm5lem  12936  znege1  12974  sqrt2irrap  12976  divdenle  12993  nn0sqrtelqelz  13002  difsqpwdvds  13137  fldivp1  13147  pcfaclem  13148  4sqlem11  13200  4sqlem12  13201  2expltfac  13239  ballotfilemsgt1  13303  ballotfilemsel1i  13305  ballotfilemfrcn0  13322  oddennn  13332  exmidunben  13366  nninfdclemlt  13391  gzsumshift  14198  znidomb  15042  psrbaglesuppg  15106  hoverlt1  15799  ivthdichlem  15801  dveflem  15876  reeff1oleme  15922  reeff1o  15923  efap1p  15929  cosz12  15931  sin0pilem2  15933  cos02pilt1  16002  rplogcl  16031  logdivlti  16033  logdivlt  16046  cxplt  16071  cxple  16072  ltexp2  16096  logbrec  16115  logbgt0b  16121  logbgcd1irr  16122  logbgcd1irraplemexp  16123  logbgcd1irraplemap  16124  zprmlogbaplem1  16134  zprmlogbaplem2  16135  log2tlbndlog2  16139  birthdaylem3  16146  pellexlem2  16149  ppiqltx  16183  ppiqub  16194  mersenne  16195  perfectlem2  16198  bcmono  16202  bposlem1  16209  bposlem2  16210  zabsle1  16216  lgslem3  16219  lgsdirprm  16251  gausslemma2dlem1a  16275  lgseisen  16291  lgsquadlem2  16295  2sqlem8  16340  clwwlkext2edg  16761  clwwlknonex2lem2  16777  iooref1o  17181  trilpolemgt1  17186  trilpolemlt1  17188  trilpo  17190  redcwlpo  17203  neapmkvlem  17215  neapmkv  17216  taupi  17221