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

Theorem zre 8025
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre  N  ZZ  N  RR

Proof of Theorem zre
StepHypRef Expression
1 elz 8023 . 2  N  ZZ  N  RR  N  0  N  NN  -u N  NN
21simplbi 259 1  N  ZZ  N  RR
Colors of variables: wff set class
Syntax hints:   wi 4   w3o 883   wceq 1242   wcel 1390   RRcr 6710   0cc0 6711   -ucneg 6980   NNcn 7695   ZZcz 8021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3or 885  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-rab 2309  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458  df-neg 6982  df-z 8022
This theorem is referenced by:  zcn  8026  zrei  8027  zssre  8028  elnn0z  8034  elnnz1  8044  peano2z  8057  zaddcl  8061  ztri3or0  8063  ztri3or  8064  zletric  8065  zlelttric  8066  zltnle  8067  zleloe  8068  zletr  8070  znnsub  8072  zltp1le  8074  zleltp1  8075  znn0sub  8085  zapne  8091  zdceq  8092  zdcle  8093  zdclt  8094  zltlen  8095  nn0ge0div  8103  zextle  8107  btwnnz  8110  msqznn  8114  peano2uz2  8121  uzind  8125  fzind  8129  fnn0ind  8130  eluzuzle  8257  uzid  8263  uzneg  8267  uz11  8271  eluzp1m1  8272  eluzp1p1  8274  eluzaddi  8275  eluzsubi  8276  uzin  8281  uz3m2nn  8291  peano2uz  8302  nn0pzuz  8306  eluz2b2  8316  uz2mulcl  8321  eqreznegel  8325  lbzbi  8327  qre  8336  elfz1eq  8669  fznlem  8675  fzen  8677  uzsubsubfz  8681  fzaddel  8692  fzsuc2  8711  fzp1disj  8712  fzrev  8716  elfz1b  8722  fzneuz  8733  fzp1nel  8736  elfz0fzfz0  8753  fz0fzelfz0  8754  fznn0sub2  8755  fz0fzdiffz0  8757  elfzmlbmOLD  8759  elfzmlbp  8760  difelfznle  8763  elfzouz2  8787  fzonlt0  8793  fzossrbm1  8799  fzo1fzo0n0  8809  elfzo0z  8810  fzofzim  8814  eluzgtdifelfzo  8823  fzossfzop1  8838  ssfzo12bi  8851  elfzomelpfzo  8857  fzosplitprm1  8860  fzostep1  8863  zsqcl2  8984  nn0abscl  9229
  Copyright terms: Public domain W3C validator