Theorem zret 6054

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 6052	. 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 771   = wceq 1099   e. wcel 1104  RRcr 5173  0cc0 5174  -ucneg 5233  NNcn 5236  ZZcz 5238

This theorem is referenced by:  zcnt 6055  zre 6056  zssre 6057  elnn0z 6062  elnnz1 6070  znnnlt1t 6071  elnn0nn 6086  znnsubt 6092  znn0subt 6093  zleltp1t 6097  z2get 6103  zextlet 6104  btwnnzt 6107  msqznn 6111  peano2uz2 6117  dfuz 6118  uzind 6121  uzindOLD 6124  uzwo4OLD 6126  uzwo3lem1 6132  zmax 6136  zbtwnre 6137  rebtwnz 6138  flget 6146  flltt 6147  flidt 6148  flval3t 6150  flwordit 6151  fladdzt 6155  flhalft 6157  ceiget 6159  ceim1lt 6160  ceilet 6161  qret 6165  zqt 6166  qbtwnre 6184  om2uzlt 6203  om2uzf1o 6206  uzidt 6327  uztrn 6328  uznegit 6329  uzss 6331  uz11t 6332  eluzp1m1t 6333  eluzp1p1t 6335  eluzaddi 6336  eluzsubi 6337  peano2uz 6347  uzwo 6355  uzwoOLD 6356  elfzlem 6373  elfzle3 6385  eluzfz1t 6387  eluzfz2t 6389  elfz1eqt 6392  fznt 6393  elfz2nn0t 6395  fznn0sub2t 6399  fzaddelt 6400  fzoptht 6402  fzss1t 6403  fzss2t 6404  elfzp1 6410  fzrevt 6411  fzneuzt 6418  seqz1 6447  sqr2irr 6627  nn0absclt 6784  cau5i 6822  cau4i 6823  cau5 6824  cvg1i 6825  cvg3 6828  facavgt 6860  bcval4t 6867  fsum1ps 6924  fsumsplit 6926  fsumrev 6935  fsumcmpndx2 6948  climshft 7009  climrecl 7015  climge0 7017  climaddlem3 7020  climmullem8 7031  serzf0 7073  ser1f0 7074  fsum0diaglem1 7159  fsum0diag4 7164  efaddlem1 7248  efaddlem2 7249  efaddlem14 7261  efaddlem16 7263  efaddlem23 7270  znnenlem 7411  znnenlemOLD 7412  znnen 7413  lmnn 7838  lmle 7860

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-12 1103  ax-13 1106  ax-14 1107  ax-11 1124  ax-10o 1125  ax-10 1126  ax-17 1191  ax-16 1195  ax-11o 1203  ax-ext 1438  ax-sep 2676  ax-pow 2715  ax-pr 2752

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-ex 957  df-sb 1157  df-eu 1361  df-mo 1362  df-clab 1443  df-cleq 1448  df-clel 1451  df-ne 1565  df-rab 1630  df-v 1789  df-dif 2025  df-un 2026  df-in 2027  df-ss 2029  df-nul 2257  df-pw 2378  df-sn 2388  df-pr 2389  df-op 2392  df-uni 2477  df-br 2593  df-opab 2640  df-xp 3153  df-cnv 3155  df-dm 3157  df-rn 3158  df-res 3159  df-ima 3160  df-fv 3167  df-opr 3918  df-neg 5298  df-z 6051

Copyright terms: Public domain