Theorem zre 9253

Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
zre	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre

Step	Hyp	Ref	Expression
1		elz 9251	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 274	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∨ w3o 977   = wceq 1353   ∈ wcel 2148  ℝcr 7807  0cc0 7808  -cneg 8125  ℕcn 8915  ℤcz 9249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4003  df-iota 5177  df-fv 5223  df-ov 5875  df-neg 8127  df-z 9250

This theorem is referenced by:  zcn  9254  zrei  9255  zssre  9256  elnn0z  9262  elnnz1  9272  peano2z  9285  zaddcl  9289  ztri3or0  9291  ztri3or  9292  zletric  9293  zlelttric  9294  zltnle  9295  zleloe  9296  zletr  9298  znnsub  9300  nzadd  9301  zltp1le  9303  zleltp1  9304  znn0sub  9314  zapne  9323  zdceq  9324  zdcle  9325  zdclt  9326  zltlen  9327  nn0ge0div  9336  zextle  9340  btwnnz  9343  suprzclex  9347  msqznn  9349  peano2uz2  9356  uzind  9360  fzind  9364  fnn0ind  9365  eluzuzle  9532  uzid  9538  uzneg  9542  uz11  9546  eluzp1m1  9547  eluzp1p1  9549  eluzaddi  9550  eluzsubi  9551  uzin  9556  uz3m2nn  9569  peano2uz  9579  nn0pzuz  9583  eluz2b2  9599  uz2mulcl  9604  eqreznegel  9610  lbzbi  9612  qre  9621  elpq  9644  zltaddlt1le  10003  elfz1eq  10030  fznlem  10036  fzen  10038  uzsubsubfz  10042  fzaddel  10054  fzsuc2  10074  fzp1disj  10075  fzrev  10079  elfz1b  10085  fzneuz  10096  fzp1nel  10099  elfz0fzfz0  10121  fz0fzelfz0  10122  fznn0sub2  10123  fz0fzdiffz0  10125  elfzmlbp  10127  difelfznle  10130  elfzouz2  10156  fzonlt0  10162  fzossrbm1  10168  fzo1fzo0n0  10178  elfzo0z  10179  fzofzim  10183  eluzgtdifelfzo  10192  fzossfzop1  10207  ssfzo12bi  10220  elfzomelpfzo  10226  fzosplitprm1  10229  fzostep1  10232  flid  10279  flqbi2  10286  2tnp1ge0ge0  10296  flhalf  10297  fldiv4p1lem1div2  10300  ceiqle  10308  uzsinds  10437  zsqcl2  10592  nn0abscl  11087  zmaxcl  11226  2zsupmax  11227  2zinfmin  11244  p1modz1  11794  evennn02n  11879  evennn2n  11880  ltoddhalfle  11890  infssuzex  11942  dfgcd2  12007  algcvga  12043  isprm3  12110  dvdsnprmd  12117  sqnprm  12128  zgcdsq  12193  hashdvds  12213  fldivp1  12338  zgz  12363  4sqlem4  12382  mulgval  12918  coskpi  14140  relogexp  14164  rplogbzexp  14243  zabsle1  14271  lgsne0  14310  2sqlem2  14322