Theorem zret 6094

Description: An integer is a real.

Assertion

Ref	Expression
zret	⊢ (N ∈ ℤ → N ∈ ℝ)

Proof of Theorem zret

Step	Hyp	Ref	Expression
1		elz 6092	. 2 ⊢ (N ∈ ℤ ↔ (N ∈ ℝ ⋀ (N = 0 ⋁ N ∈ ℕ ⋁ -N ∈ ℕ)))
2	1	pm3.26bi 322	1 ⊢ (N ∈ ℤ → N ∈ ℝ)

Syntax hints:   → wi 3   ⋁ w3o 773   = wceq 954   ∈ wcel 956  ℝcr 5213  0cc0 5214  -cneg 5273  ℕcn 5276  ℤcz 5278

This theorem is referenced by:  zcnt 6095  zre 6096  zssre 6097  elnn0z 6102  elnnz1 6110  znnnlt1t 6111  elnn0nn 6126  znnsubt 6132  znn0subt 6133  zleltp1t 6137  z2get 6143  zextlet 6144  btwnnzt 6147  msqznn 6151  peano2uz2 6157  dfuz 6158  uzind 6161  uzindOLD 6164  uzwo4OLD 6166  uzwo3lem1 6172  zmax 6176  zbtwnre 6177  rebtwnz 6178  flget 6186  flltt 6187  flidt 6188  flval3t 6190  flwordit 6191  fladdzt 6195  flhalft 6197  ceiget 6199  ceim1lt 6200  ceilet 6201  qret 6205  zqt 6206  qbtwnre 6224  om2uzlt 6243  om2uzf1o 6246  uzidt 6367  uztrn 6368  uznegit 6369  uzss 6371  uz11t 6372  eluzp1m1t 6373  eluzp1p1t 6375  eluzaddi 6376  eluzsubi 6377  peano2uz 6387  uzwo 6395  uzwoOLD 6396  elfzlem 6413  elfzle3 6425  eluzfz1t 6427  eluzfz2t 6429  elfz1eqt 6432  fznt 6433  elfz2nn0t 6435  fznn0sub2t 6439  fzaddelt 6440  fzoptht 6442  fzss1t 6443  fzss2t 6444  elfzp1 6450  fzrevt 6451  fzneuzt 6458  seqz1 6487  sqr2irr 6667  nn0absclt 6824  cau5i 6862  cau4i 6863  cau5 6864  cvg1i 6865  cvg3 6868  facavgt 6900  bcval4t 6907  fsum1ps 6964  fsumsplit 6966  fsumrev 6975  fsumcmpndx2 6988  climshft 7049  climrecl 7055  climge0 7057  climaddlem3 7060  climmullem8 7071  serzf0 7113  ser1f0 7114  fsum0diaglem1 7199  fsum0diag4 7204  efaddlem1 7288  efaddlem2 7289  efaddlem14 7301  efaddlem16 7303  efaddlem23 7310  znnenlem 7451  znnenlemOLD 7452  znnen 7453  lmnn 7887  lmle 7911

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-rab 1649  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193  df-opr 3956  df-neg 5338  df-z 6091

Copyright terms: Public domain