Theorem zret 6086

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 6084	. 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 772   = wceq 953   e. wcel 955  RRcr 5205  0cc0 5206  -ucneg 5265  NNcn 5268  ZZcz 5270

This theorem is referenced by:  zcnt 6087  zre 6088  zssre 6089  elnn0z 6094  elnnz1 6102  znnnlt1t 6103  elnn0nn 6118  znnsubt 6124  znn0subt 6125  zleltp1t 6129  z2get 6135  zextlet 6136  btwnnzt 6139  msqznn 6143  peano2uz2 6149  dfuz 6150  uzind 6153  uzindOLD 6156  uzwo4OLD 6158  uzwo3lem1 6164  zmax 6168  zbtwnre 6169  rebtwnz 6170  flget 6178  flltt 6179  flidt 6180  flval3t 6182  flwordit 6183  fladdzt 6187  flhalft 6189  ceiget 6191  ceim1lt 6192  ceilet 6193  qret 6197  zqt 6198  qbtwnre 6216  om2uzlt 6235  om2uzf1o 6238  uzidt 6359  uztrn 6360  uznegit 6361  uzss 6363  uz11t 6364  eluzp1m1t 6365  eluzp1p1t 6367  eluzaddi 6368  eluzsubi 6369  peano2uz 6379  uzwo 6387  uzwoOLD 6388  elfzlem 6405  elfzle3 6417  eluzfz1t 6419  eluzfz2t 6421  elfz1eqt 6424  fznt 6425  elfz2nn0t 6427  fznn0sub2t 6431  fzaddelt 6432  fzoptht 6434  fzss1t 6435  fzss2t 6436  elfzp1 6442  fzrevt 6443  fzneuzt 6450  seqz1 6479  sqr2irr 6659  nn0absclt 6816  cau5i 6854  cau4i 6855  cau5 6856  cvg1i 6857  cvg3 6860  facavgt 6892  bcval4t 6899  fsum1ps 6956  fsumsplit 6958  fsumrev 6967  fsumcmpndx2 6980  climshft 7041  climrecl 7047  climge0 7049  climaddlem3 7052  climmullem8 7063  serzf0 7105  ser1f0 7106  fsum0diaglem1 7191  fsum0diag4 7196  efaddlem1 7280  efaddlem2 7281  efaddlem14 7293  efaddlem16 7295  efaddlem23 7302  znnenlem 7443  znnenlemOLD 7444  znnen 7445  lmnn 7873  lmle 7895

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-rab 1644  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188  df-opr 3950  df-neg 5330  df-z 6083

Copyright terms: Public domain