ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  1red Unicode version

Theorem 1red 7749
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
StepHypRef Expression
1 1re 7733 . 2  |-  1  e.  RR
21a1i 9 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1465   RRcr 7587   1c1 7589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1re 7682
This theorem is referenced by:  recgt0  8576  ltrec  8609  recp1lt1  8625  peano5nni  8691  peano2nn  8700  nn0p1gt0  8974  nn0ge2m1nn  9005  peano2z  9058  suprzclex  9117  ledivge1le  9481  iccf1o  9755  zltaddlt1le  9757  fznatpl1  9824  elfz1b  9838  fzonn0p1p1  9958  elfzom1p1elfzo  9959  exbtwnzlemstep  9993  exbtwnz  9996  rebtwn2zlemstep  9998  rebtwn2z  10000  qfraclt1  10021  flqaddz  10038  btwnzge0  10041  2tnp1ge0ge0  10042  flhalf  10043  modqid  10090  m1modge3gt1  10112  modqltm1p1mod  10117  addmodlteq  10139  seq3f1olemqsumkj  10239  ltexp2a  10313  leexp2a  10314  leexp2r  10315  nnlesq  10364  bernneq3  10382  expnbnd  10383  expnlbnd2  10385  expcanlem  10430  expcan  10431  bcval5  10477  cvg1nlemcau  10724  resqrexlem1arp  10745  resqrexlemf1  10748  resqrexlemover  10750  resqrexlemdecn  10752  resqrexlemlo  10753  resqrexlemcalc2  10755  resqrexlemnm  10758  resqrexlemga  10763  reccn2ap  11050  sumsnf  11146  expcnvre  11240  geolim  11248  geolim2  11249  georeclim  11250  geoisumr  11255  geoisum1c  11257  cvgratnnlembern  11260  cvgratnnlemsumlt  11265  cvgratnnlemfm  11266  cvgratnnlemrate  11267  cvgratnn  11268  cvgratz  11269  efcllemp  11291  efgt1  11330  eflegeo  11335  eirraplem  11410  oddge22np1  11505  ltoddhalfle  11517  nno  11530  nn0oddm1d2  11533  nnoddm1d2  11534  zssinfcl  11568  coprmgcdb  11696  prmind2  11728  dvdsnprmd  11733  znege1  11783  sqrt2irrap  11785  divdenle  11802  nn0sqrtelqelz  11811  oddennn  11832  exmidunben  11866  dveflem  12782  cosz12  12788  sin0pilem2  12790  cos02pilt1  12859  trilpolemgt1  13159  trilpolemlt1  13161  trilpo  13163  taupi  13166
  Copyright terms: Public domain W3C validator