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

Theorem 1red 7405
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 7389 . 2 1 ∈ ℝ
21a1i 9 1 (𝜑 → 1 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1434  cr 7251  1c1 7253
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1re 7341
This theorem is referenced by:  recgt0  8204  ltrec  8237  recp1lt1  8253  peano5nni  8318  peano2nn  8327  nn0p1gt0  8593  nn0ge2m1nn  8624  peano2z  8681  suprzclex  8739  ledivge1le  9097  iccf1o  9315  zltaddlt1le  9317  fznatpl1  9382  elfz1b  9396  fzonn0p1p1  9512  elfzom1p1elfzo  9513  exbtwnzlemstep  9547  exbtwnz  9550  rebtwn2zlemstep  9552  rebtwn2z  9554  qfraclt1  9575  flqaddz  9592  btwnzge0  9595  2tnp1ge0ge0  9596  flhalf  9597  modqid  9644  m1modge3gt1  9666  modqltm1p1mod  9671  addmodlteq  9693  ltexp2a  9843  leexp2a  9844  leexp2r  9845  nnlesq  9893  bernneq3  9910  expnbnd  9911  expnlbnd2  9913  expcanlem  9958  expcan  9959  ibcval5  10005  cvg1nlemcau  10243  resqrexlem1arp  10264  resqrexlemf1  10267  resqrexlemover  10269  resqrexlemdecn  10271  resqrexlemlo  10272  resqrexlemcalc2  10274  resqrexlemnm  10277  resqrexlemga  10282  oddge22np1  10660  ltoddhalfle  10672  nno  10685  nn0oddm1d2  10688  nnoddm1d2  10689  zssinfcl  10723  coprmgcdb  10849  prmind2  10881  dvdsnprmd  10886  znege1  10935  sqrt2irrap  10937  divdenle  10954  nn0sqrtelqelz  10963  oddennn  10984
  Copyright terms: Public domain W3C validator