Theorem 1red 8172

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 8156	. 2 |- 1 e. RR
2	1	a1i 9	1 |- ( ph -> 1 e. RR )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8009   1c1 8011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1re 8104

This theorem is referenced by:  recgt0  9008  ltrec  9041  recp1lt1  9057  peano5nni  9124  peano2nn  9133  nn0p1gt0  9409  nn0ge2m1nn  9440  peano2z  9493  suprzclex  9556  ledivge1le  9934  iccf1o  10212  zltaddlt1le  10215  fznatpl1  10284  elfz1b  10298  fzonn0p1p1  10431  elfzom1p1elfzo  10432  zssinfcl  10464  exbtwnzlemstep  10479  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2z  10486  qfraclt1  10512  flqaddz  10529  btwnzge0  10532  2tnp1ge0ge0  10533  flhalf  10534  fldiv4lem1div2uz2  10538  modqid  10583  m1modge3gt1  10605  modqltm1p1mod  10610  addmodlteq  10632  seq3f1olemqsumkj  10745  ltexp2a  10825  leexp2a  10826  leexp2r  10827  nnlesq  10877  bernneq3  10896  expnbnd  10897  expnlbnd2  10899  nn0ltexp2  10943  expcanlem  10949  expcan  10950  bcval5  10997  wrdlenge2n0  11120  cvg1nlemcau  11510  resqrexlem1arp  11531  resqrexlemf1  11534  resqrexlemover  11536  resqrexlemdecn  11538  resqrexlemlo  11539  resqrexlemcalc2  11541  resqrexlemnm  11544  resqrexlemga  11549  reccn2ap  11839  sumsnf  11935  expcnvre  12029  geolim  12037  geolim2  12038  georeclim  12039  geoisumr  12044  geoisum1c  12046  cvgratnnlembern  12049  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratnn  12057  cvgratz  12058  prodsnf  12118  fprodrecl  12134  fprodreclf  12140  efcllemp  12184  efgt1  12223  eflegeo  12227  sinltxirr  12287  eirraplem  12303  p1modz1  12320  oddge22np1  12407  ltoddhalfle  12419  nno  12432  nn0oddm1d2  12435  nnoddm1d2  12436  bitsfzolem  12480  bitsfzo  12481  bitsmod  12482  bitscmp  12484  bitsinv1lem  12487  uzwodc  12573  coprmgcdb  12625  prmind2  12657  dvdsnprmd  12662  prmdc  12667  isprm5lem  12678  znege1  12715  sqrt2irrap  12717  divdenle  12734  nn0sqrtelqelz  12743  difsqpwdvds  12876  fldivp1  12886  pcfaclem  12887  4sqlem11  12939  4sqlem12  12940  2expltfac  12977  oddennn  12978  exmidunben  13012  nninfdclemlt  13037  znidomb  14637  psrbaglesuppg  14651  hoverlt1  15338  ivthdichlem  15340  dveflem  15415  reeff1oleme  15461  reeff1o  15462  cosz12  15469  sin0pilem2  15471  cos02pilt1  15540  rplogcl  15568  logdivlti  15570  cxplt  15605  cxple  15606  ltexp2  15630  logbrec  15649  logbgt0b  15655  logbgcd1irr  15656  logbgcd1irraplemexp  15657  logbgcd1irraplemap  15658  mersenne  15686  perfectlem2  15689  zabsle1  15693  lgslem3  15696  lgsdirprm  15728  gausslemma2dlem1a  15752  lgseisen  15768  lgsquadlem2  15772  2sqlem8  15817  iooref1o  16462  trilpolemgt1  16467  trilpolemlt1  16469  trilpo  16471  redcwlpo  16483  neapmkvlem  16495  neapmkv  16496  taupi  16501