Theorem 1red 7967

Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1red	⊢ (𝜑 → 1 ∈ ℝ)

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 7951	. 2 ⊢ 1 ∈ ℝ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7805  1c1 7807

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

This theorem is referenced by:  recgt0  8801  ltrec  8834  recp1lt1  8850  peano5nni  8916  peano2nn  8925  nn0p1gt0  9199  nn0ge2m1nn  9230  peano2z  9283  suprzclex  9345  ledivge1le  9720  iccf1o  9998  zltaddlt1le  10001  fznatpl1  10069  elfz1b  10083  fzonn0p1p1  10206  elfzom1p1elfzo  10207  exbtwnzlemstep  10241  exbtwnz  10244  rebtwn2zlemstep  10246  rebtwn2z  10248  qfraclt1  10273  flqaddz  10290  btwnzge0  10293  2tnp1ge0ge0  10294  flhalf  10295  modqid  10342  m1modge3gt1  10364  modqltm1p1mod  10369  addmodlteq  10391  seq3f1olemqsumkj  10491  ltexp2a  10565  leexp2a  10566  leexp2r  10567  nnlesq  10616  bernneq3  10635  expnbnd  10636  expnlbnd2  10638  nn0ltexp2  10681  expcanlem  10686  expcan  10687  bcval5  10734  cvg1nlemcau  10984  resqrexlem1arp  11005  resqrexlemf1  11008  resqrexlemover  11010  resqrexlemdecn  11012  resqrexlemlo  11013  resqrexlemcalc2  11015  resqrexlemnm  11018  resqrexlemga  11023  reccn2ap  11312  sumsnf  11408  expcnvre  11502  geolim  11510  geolim2  11511  georeclim  11512  geoisumr  11517  geoisum1c  11519  cvgratnnlembern  11522  cvgratnnlemsumlt  11527  cvgratnnlemfm  11528  cvgratnnlemrate  11529  cvgratnn  11530  cvgratz  11531  prodsnf  11591  fprodrecl  11607  fprodreclf  11613  efcllemp  11657  efgt1  11696  eflegeo  11700  eirraplem  11775  p1modz1  11792  oddge22np1  11876  ltoddhalfle  11888  nno  11901  nn0oddm1d2  11904  nnoddm1d2  11905  zssinfcl  11939  uzwodc  12028  coprmgcdb  12078  prmind2  12110  dvdsnprmd  12115  prmdc  12120  isprm5lem  12131  znege1  12168  sqrt2irrap  12170  divdenle  12187  nn0sqrtelqelz  12196  difsqpwdvds  12327  fldivp1  12336  pcfaclem  12337  oddennn  12383  exmidunben  12417  nninfdclemlt  12442  dveflem  13969  reeff1oleme  13975  reeff1o  13976  cosz12  13983  sin0pilem2  13985  cos02pilt1  14054  rplogcl  14082  logdivlti  14084  cxplt  14118  cxple  14119  ltexp2  14142  logbrec  14160  logbgt0b  14166  logbgcd1irr  14167  logbgcd1irraplemexp  14168  logbgcd1irraplemap  14169  zabsle1  14182  lgslem3  14185  lgsdirprm  14217  2sqlem8  14241  iooref1o  14553  trilpolemgt1  14558  trilpolemlt1  14560  trilpo  14562  redcwlpo  14574  neapmkvlem  14585  neapmkv  14586  taupi  14591