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

Theorem 1red 7745
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
StepHypRef Expression
1 1re 7729 . 2 1 ∈ ℝ
21a1i 9 1 (𝜑 → 1 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1463  cr 7583  1c1 7585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1re 7678
This theorem is referenced by:  recgt0  8565  ltrec  8598  recp1lt1  8614  peano5nni  8680  peano2nn  8689  nn0p1gt0  8957  nn0ge2m1nn  8988  peano2z  9041  suprzclex  9100  ledivge1le  9459  iccf1o  9727  zltaddlt1le  9729  fznatpl1  9796  elfz1b  9810  fzonn0p1p1  9930  elfzom1p1elfzo  9931  exbtwnzlemstep  9965  exbtwnz  9968  rebtwn2zlemstep  9970  rebtwn2z  9972  qfraclt1  9993  flqaddz  10010  btwnzge0  10013  2tnp1ge0ge0  10014  flhalf  10015  modqid  10062  m1modge3gt1  10084  modqltm1p1mod  10089  addmodlteq  10111  seq3f1olemqsumkj  10211  ltexp2a  10285  leexp2a  10286  leexp2r  10287  nnlesq  10336  bernneq3  10354  expnbnd  10355  expnlbnd2  10357  expcanlem  10402  expcan  10403  bcval5  10449  cvg1nlemcau  10696  resqrexlem1arp  10717  resqrexlemf1  10720  resqrexlemover  10722  resqrexlemdecn  10724  resqrexlemlo  10725  resqrexlemcalc2  10727  resqrexlemnm  10730  resqrexlemga  10735  reccn2ap  11022  sumsnf  11118  expcnvre  11212  geolim  11220  geolim2  11221  georeclim  11222  geoisumr  11227  geoisum1c  11229  cvgratnnlembern  11232  cvgratnnlemsumlt  11237  cvgratnnlemfm  11238  cvgratnnlemrate  11239  cvgratnn  11240  cvgratz  11241  efcllemp  11263  efgt1  11302  eflegeo  11307  eirraplem  11379  oddge22np1  11474  ltoddhalfle  11486  nno  11499  nn0oddm1d2  11502  nnoddm1d2  11503  zssinfcl  11537  coprmgcdb  11665  prmind2  11697  dvdsnprmd  11702  znege1  11751  sqrt2irrap  11753  divdenle  11770  nn0sqrtelqelz  11779  oddennn  11800  exmidunben  11834  dveflem  12729  trilpolemgt1  13034  trilpolemlt1  13036  trilpo  13038
  Copyright terms: Public domain W3C validator