Theorem zre 7143

Description: An integer is a real.

Assertion

Ref	Expression
zre	|- (N e. ZZ -> N e. RR)

Proof of Theorem zre

Step	Hyp	Ref	Expression
1		elz 7141	. 2 |- (N e. ZZ <-> (N e. RR /\ (N = 0 \/ N e. NN \/ -uN e. NN)))
2	1	pm3.26bi 347	1 |- (N e. ZZ -> N e. RR)

Syntax hints:   -> wi 3   \/ w3o 854   = wceq 1136   e. wcel 1138  RRcr 6181  0cc0 6182  -ucneg 6242  NNcn 6245  ZZcz 6247

This theorem is referenced by:  zcn 7144  zrei 7145  zssre 7146  elnn0z 7151  elnnz1 7159  znnnlt1 7160  elnn0nn 7175  znnsub 7181  znn0sub 7182  zleltp1 7186  z2ge 7195  zextle 7196  btwnnz 7199  msqznn 7203  peano2uz2 7208  dfuzi 7209  uzind 7212  uzindOLD 7215  uzwo4OLD 7217  uzwo3lem1 7224  zmax 7228  zbtwnre 7229  rebtwnz 7230  qre 7234  zq 7235  qbtwnre 7254  reflcl 7261  flge 7267  fllt 7268  flid 7269  flval3 7274  flbi2 7276  fladdz 7279  flhalf 7282  ceile 7286  quoremz 7287  intfracq 7291  zmodcl 7306  modcyc 7311  modmul1 7314  uzid 7391  uztrn 7392  uzneg 7393  uzss 7395  uz11 7396  eluzp1m1 7397  eluzp1p1 7399  eluzaddi 7400  eluzsubi 7401  peano2uz 7411  uzwo 7419  uzwoOLD 7420  elfzlem 7438  elfzle3 7450  eluzfz1 7452  eluzfz2 7454  elfz1eq 7457  fzn 7458  fzen 7459  elfz2nn0 7462  fznn0sub2 7466  fzaddel 7467  fzopth 7469  fzss1 7470  fzss2 7471  fzsuc 7473  elfzp1 7478  fztp 7481  fzrev 7484  fzneuz 7492  om2uzlti 7504  om2uzf1oi 7507  seqz1 7585  sqr2irr 7774  nn0abscl 7926  cau5ii 7964  cau4ii 7965  cau5i 7966  cvg1i 7967  cvg3i 7970  bcval4 8008  fsum1ps 8073  fsumsplit 8075  fsumrev 8084  fsumcmpndx2 8097  climshfti 8159  climrecl 8165  climge0 8167  climaddlem3 8171  climmullem8 8182  serzf0i 8224  fsum0diaglem1 8313  fsum0diag4 8318  efaddlem1 8395  efaddlem2 8396  efaddlem14 8408  efaddlem16 8410  znnenlem 8565  znnen 8566  lmle 9033  gxnval 9178  gxmodid 9197  vacnlem3 9464  coskpi 9859  fzind 13402  fnn0ind 13403  zmod10 13405  zmodid2 13406  zmodfz 13407  fseq1cl 13411  eqreznegel 13446  lbzbi 13449  nn0seqcvgd 13451  absdvdsb 13465  dvdsabsb 13466  dvdsle 13485  dvdsleabs 13486  alzdvds 13487  divalgmod 13501  gcd0id 13521  gcdneg 13524  gcdaddmlem 13526  gcdabs 13529  modgcd 13530  algcvga 13539  zgt1b1 13563  isprm3 13568  coprm 13574  seqzp2 14439  zmodfzcl 15462  uzm1 15466  fzfi 15468  fzmul 15472  fzadd2 15473  fzsplit 15474  fzdisj 15475  fzm1 15478  absrdbnd 15481  fdc 15494  incsequz2 15498  fsumlt1 15513  caushft 15533  heiborlem12 15648  heiborlem16 15652  rrntotbndlem1 15702  rrntotbndlem2 15703  rrntotbnd 15704

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-rex 1944  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-xp 3811  df-cnv 3813  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fv 3825  df-opr 4697  df-neg 6309  df-z 7140

Copyright terms: Public domain