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  9638  peano2z  9691  suprzclex  9755  ledivge1le  10144  lincmble  10423  iccf1o  10424  zltaddlt1le  10427  fznatpl1  10500  elfz1b  10514  fzonn0p1p1  10648  elfzom1p1elfzo  10649  zssinfcl  10682  exbtwnzlemstep  10699  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  qfraclt1  10734  flqaddz  10753  btwnzge0  10756  2tnp1ge0ge0  10757  flhalf  10758  fldiv4lem1div2uz2  10762  modqid  10807  m1modge3gt1  10829  modqltm1p1mod  10834  addmodlteq  10856  seq3f1olemqsumkj  10969  ltexp2a  11049  leexp2a  11050  leexp2r  11051  nnlesq  11101  resq01  11116  bernneq3  11121  expnbnd  11122  expnlbnd2  11124  nn0ltexp2  11169  expcanlem  11175  expcan  11176  bcval5  11223  ssenneg  11302  wrdlenge2n0  11362  sq01  11682  cvg1nlemcau  11772  resqrexlem1arp  11793  resqrexlemf1  11796  resqrexlemover  11798  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc2  11803  resqrexlemnm  11806  resqrexlemga  11811  reccn2ap  12104  sumsnf  12201  expcnvre  12295  geolim  12303  geolim2  12304  georeclim  12305  geoisumr  12310  geoisum1c  12312  cvgratnnlembern  12315  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratnn  12323  cvgratz  12324  prodsnf  12384  fprodrecl  12400  fprodreclf  12406  efcllemp  12450  efgt1  12489  eflegeo  12493  sinltxirr  12553  eirraplem  12569  p1modz1  12586  oddge22np1  12673  ltoddhalfle  12685  nno  12698  nn0oddm1d2  12701  nnoddm1d2  12702  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitscmp  12750  bitsinv1lem  12753  uzwodc  12839  coprmgcdb  12891  prmind2  12923  dvdsnprmd  12928  prmdc  12933  isprm5lem  12945  znege1  12983  sqrt2irrap  12985  divdenle  13002  nn0sqrtelqelz  13011  difsqpwdvds  13146  fldivp1  13156  pcfaclem  13157  4sqlem11  13209  4sqlem12  13210  2expltfac  13248  ballotfilemsgt1  13312  ballotfilemsel1i  13314  ballotfilemfrcn0  13331  oddennn  13341  exmidunben  13375  nninfdclemlt  13400  gzsumshift  14239  znidomb  15102  psrbaglesuppg  15166  hoverlt1  15875  ivthdichlem  15877  dveflem  15952  reeff1oleme  15998  reeff1o  15999  efap1p  16005  cosz12  16007  sin0pilem2  16009  cos02pilt1  16079  rplogcl  16109  logdivlti  16111  logdivlt  16124  cxplt  16151  cxple  16152  ltexp2  16177  logbrec  16196  logbgt0b  16202  logbgcd1irr  16203  logbgcd1irraplemexp  16204  logbgcd1irraplemap  16205  zprmlogbaplem1  16215  zprmlogbaplem2  16216  log2tlbndlog2  16220  birthdaylem3  16227  pellexlem2  16230  ppiqltx  16281  ppiqub  16293  chtqub  16296  mersenne  16297  perfectlem2  16300  bcmono  16304  bposlem1  16311  bposlem2  16312  zabsle1  16323  lgslem3  16326  lgsdirprm  16358  gausslemma2dlem1a  16382  lgseisen  16398  lgsquadlem2  16402  2sqlem8  16447  clwwlkext2edg  16868  clwwlknonex2lem2  16884  iooref1o  17289  trilpolemgt1  17295  trilpolemlt1  17297  trilpo  17299  redcwlpo  17312  neapmkvlem  17324  neapmkv  17325  taupi  17330