Theorem 1red 8087

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

Syntax hints:   -> wi 4   e. wcel 2176   RRcr 7924   1c1 7926

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

This theorem is referenced by:  recgt0  8923  ltrec  8956  recp1lt1  8972  peano5nni  9039  peano2nn  9048  nn0p1gt0  9324  nn0ge2m1nn  9355  peano2z  9408  suprzclex  9471  ledivge1le  9848  iccf1o  10126  zltaddlt1le  10129  fznatpl1  10198  elfz1b  10212  fzonn0p1p1  10342  elfzom1p1elfzo  10343  zssinfcl  10375  exbtwnzlemstep  10390  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2z  10397  qfraclt1  10423  flqaddz  10440  btwnzge0  10443  2tnp1ge0ge0  10444  flhalf  10445  fldiv4lem1div2uz2  10449  modqid  10494  m1modge3gt1  10516  modqltm1p1mod  10521  addmodlteq  10543  seq3f1olemqsumkj  10656  ltexp2a  10736  leexp2a  10737  leexp2r  10738  nnlesq  10788  bernneq3  10807  expnbnd  10808  expnlbnd2  10810  nn0ltexp2  10854  expcanlem  10860  expcan  10861  bcval5  10908  wrdlenge2n0  11029  cvg1nlemcau  11295  resqrexlem1arp  11316  resqrexlemf1  11319  resqrexlemover  11321  resqrexlemdecn  11323  resqrexlemlo  11324  resqrexlemcalc2  11326  resqrexlemnm  11329  resqrexlemga  11334  reccn2ap  11624  sumsnf  11720  expcnvre  11814  geolim  11822  geolim2  11823  georeclim  11824  geoisumr  11829  geoisum1c  11831  cvgratnnlembern  11834  cvgratnnlemsumlt  11839  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratnn  11842  cvgratz  11843  prodsnf  11903  fprodrecl  11919  fprodreclf  11925  efcllemp  11969  efgt1  12008  eflegeo  12012  sinltxirr  12072  eirraplem  12088  p1modz1  12105  oddge22np1  12192  ltoddhalfle  12204  nno  12217  nn0oddm1d2  12220  nnoddm1d2  12221  bitsfzolem  12265  bitsfzo  12266  bitsmod  12267  bitscmp  12269  bitsinv1lem  12272  uzwodc  12358  coprmgcdb  12410  prmind2  12442  dvdsnprmd  12447  prmdc  12452  isprm5lem  12463  znege1  12500  sqrt2irrap  12502  divdenle  12519  nn0sqrtelqelz  12528  difsqpwdvds  12661  fldivp1  12671  pcfaclem  12672  4sqlem11  12724  4sqlem12  12725  2expltfac  12762  oddennn  12763  exmidunben  12797  nninfdclemlt  12822  znidomb  14420  psrbaglesuppg  14434  hoverlt1  15121  ivthdichlem  15123  dveflem  15198  reeff1oleme  15244  reeff1o  15245  cosz12  15252  sin0pilem2  15254  cos02pilt1  15323  rplogcl  15351  logdivlti  15353  cxplt  15388  cxple  15389  ltexp2  15413  logbrec  15432  logbgt0b  15438  logbgcd1irr  15439  logbgcd1irraplemexp  15440  logbgcd1irraplemap  15441  mersenne  15469  perfectlem2  15472  zabsle1  15476  lgslem3  15479  lgsdirprm  15511  gausslemma2dlem1a  15535  lgseisen  15551  lgsquadlem2  15555  2sqlem8  15600  iooref1o  15973  trilpolemgt1  15978  trilpolemlt1  15980  trilpo  15982  redcwlpo  15994  neapmkvlem  16006  neapmkv  16007  taupi  16012