Theorem 1red 7935

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

Syntax hints:   -> wi 4   e. wcel 2141   RRcr 7773   1c1 7775

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

This theorem is referenced by:  recgt0  8766  ltrec  8799  recp1lt1  8815  peano5nni  8881  peano2nn  8890  nn0p1gt0  9164  nn0ge2m1nn  9195  peano2z  9248  suprzclex  9310  ledivge1le  9683  iccf1o  9961  zltaddlt1le  9964  fznatpl1  10032  elfz1b  10046  fzonn0p1p1  10169  elfzom1p1elfzo  10170  exbtwnzlemstep  10204  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2z  10211  qfraclt1  10236  flqaddz  10253  btwnzge0  10256  2tnp1ge0ge0  10257  flhalf  10258  modqid  10305  m1modge3gt1  10327  modqltm1p1mod  10332  addmodlteq  10354  seq3f1olemqsumkj  10454  ltexp2a  10528  leexp2a  10529  leexp2r  10530  nnlesq  10579  bernneq3  10598  expnbnd  10599  expnlbnd2  10601  nn0ltexp2  10644  expcanlem  10649  expcan  10650  bcval5  10697  cvg1nlemcau  10948  resqrexlem1arp  10969  resqrexlemf1  10972  resqrexlemover  10974  resqrexlemdecn  10976  resqrexlemlo  10977  resqrexlemcalc2  10979  resqrexlemnm  10982  resqrexlemga  10987  reccn2ap  11276  sumsnf  11372  expcnvre  11466  geolim  11474  geolim2  11475  georeclim  11476  geoisumr  11481  geoisum1c  11483  cvgratnnlembern  11486  cvgratnnlemsumlt  11491  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratnn  11494  cvgratz  11495  prodsnf  11555  fprodrecl  11571  fprodreclf  11577  efcllemp  11621  efgt1  11660  eflegeo  11664  eirraplem  11739  p1modz1  11756  oddge22np1  11840  ltoddhalfle  11852  nno  11865  nn0oddm1d2  11868  nnoddm1d2  11869  zssinfcl  11903  uzwodc  11992  coprmgcdb  12042  prmind2  12074  dvdsnprmd  12079  prmdc  12084  isprm5lem  12095  znege1  12132  sqrt2irrap  12134  divdenle  12151  nn0sqrtelqelz  12160  difsqpwdvds  12291  fldivp1  12300  pcfaclem  12301  oddennn  12347  exmidunben  12381  nninfdclemlt  12406  dveflem  13481  reeff1oleme  13487  reeff1o  13488  cosz12  13495  sin0pilem2  13497  cos02pilt1  13566  rplogcl  13594  logdivlti  13596  cxplt  13630  cxple  13631  ltexp2  13654  logbrec  13672  logbgt0b  13678  logbgcd1irr  13679  logbgcd1irraplemexp  13680  logbgcd1irraplemap  13681  zabsle1  13694  lgslem3  13697  lgsdirprm  13729  2sqlem8  13753  iooref1o  14066  trilpolemgt1  14071  trilpolemlt1  14073  trilpo  14075  redcwlpo  14087  neapmkvlem  14098  neapmkv  14099  taupi  14102