Theorem zret 6141

Description: An integer is a real.

Assertion

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

Proof of Theorem zret

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

Syntax hints:   -> wi 3   \/ w3o 776   = wceq 958   e. wcel 960  RRcr 5245  0cc0 5246  -ucneg 5305  NNcn 5308  ZZcz 5310

This theorem is referenced by:  zcnt 6142  zre 6143  zssre 6144  elnn0z 6149  elnnz1 6157  znnnlt1t 6158  elnn0nn 6173  znnsubt 6179  znn0subt 6180  zleltp1t 6184  z2get 6190  zextlet 6191  btwnnzt 6194  msqznn 6198  peano2uz2 6203  dfuz 6204  uzind 6207  uzindOLD 6210  uzwo4OLD 6212  uzwo3lem1 6218  zmax 6222  zbtwnre 6223  rebtwnz 6224  flreclt 6229  flget 6235  flltt 6236  flidt 6237  flval3t 6241  flbi2t 6243  fladdzt 6246  flhalft 6248  ceilet 6252  quoremz 6253  intfracq 6255  qret 6260  zqt 6261  qbtwnre 6279  om2uzlt 6299  om2uzf1o 6302  uzidt 6428  uztrn 6429  uznegit 6430  uzss 6432  uz11t 6433  eluzp1m1t 6434  eluzp1p1t 6436  eluzaddi 6437  eluzsubi 6438  peano2uz 6448  uzwo 6456  uzwoOLD 6457  elfzlem 6474  elfzle3 6486  eluzfz1t 6488  eluzfz2t 6490  elfz1eqt 6493  fznt 6494  elfz2nn0t 6496  fznn0sub2t 6500  fzaddelt 6501  fzoptht 6503  fzss1t 6504  fzss2t 6505  elfzp1 6511  fzrevt 6512  fzneuzt 6519  seqz1 6548  sqr2irr 6730  nn0absclt 6879  cau5i 6917  cau4i 6918  cau5 6919  cvg1i 6920  cvg3 6923  bcval4t 6961  fsum1ps 7018  fsumsplit 7020  fsumrev 7029  fsumcmpndx2 7042  climshft 7104  climrecl 7110  climge0 7112  climaddlem3 7116  climmullem8 7127  serzf0 7169  ser1f0 7170  fsum0diaglem1 7256  fsum0diag4 7261  efaddlem1 7338  efaddlem2 7339  efaddlem14 7351  efaddlem16 7353  znnenlem 7502  znnen 7503  lmle 7957

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-rab 1655  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-xp 3190  df-cnv 3192  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fv 3204  df-opr 3971  df-neg 5370  df-z 6138

Copyright terms: Public domain