ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zcn GIF version

Theorem zcn 8306
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
zcn (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Proof of Theorem zcn
StepHypRef Expression
1 zre 8305 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 7112 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  cc 6944  cz 8301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-resscn 7033
This theorem depends on definitions:  df-bi 114  df-3or 897  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-rab 2332  df-v 2576  df-un 2949  df-in 2951  df-ss 2958  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-iota 4894  df-fv 4937  df-ov 5542  df-neg 7247  df-z 8302
This theorem is referenced by:  zsscn  8309  zaddcllempos  8338  peano2zm  8339  zaddcllemneg  8340  zaddcl  8341  zsubcl  8342  zrevaddcl  8351  nzadd  8353  zlem1lt  8357  zltlem1  8358  zapne  8372  zdiv  8385  zdivadd  8386  zdivmul  8387  zextlt  8389  zneo  8397  zeo2  8402  peano5uzti  8404  zindd  8414  divfnzn  8652  qmulz  8654  zq  8657  qaddcl  8666  qnegcl  8667  qmulcl  8668  qreccl  8673  fzen  9008  uzsubsubfz  9012  fz01en  9018  fzmmmeqm  9022  fzsubel  9024  fztp  9041  fzsuc2  9042  fzrev2  9048  fzrev3  9050  elfzp1b  9060  fzrevral  9068  fzrevral2  9069  fzrevral3  9070  fzshftral  9071  fzoaddel2  9150  fzosubel2  9152  eluzgtdifelfzo  9154  fzocatel  9156  elfzom1elp1fzo  9159  fzval3  9161  zpnn0elfzo1  9165  fzosplitprm1  9191  fzoshftral  9195  flqzadd  9242  2tnp1ge0ge0  9245  ceilid  9259  intfracq  9264  zmod10  9284  modqmuladdnn0  9312  addmodlteq  9342  frecfzen2  9362  iseqshft2  9390  isermono  9395  m1expeven  9461  expsubap  9462  zesq  9528  sqoddm1div8  9562  bccmpl  9615  shftuz  9639  nnabscl  9919  climshftlemg  10046  climshft  10048  dvdsval2  10103  iddvds  10113  1dvds  10114  dvds0  10115  negdvdsb  10116  dvdsnegb  10117  0dvds  10120  dvdsmul1  10121  iddvdsexp  10123  muldvds1  10124  muldvds2  10125  dvdscmul  10126  dvdsmulc  10127  summodnegmod  10130  modmulconst  10131  dvds2ln  10132  dvds2add  10133  dvds2sub  10134  dvdstr  10136  dvdssub2  10141  dvdsadd  10142  dvdsaddr  10143  dvdssub  10144  dvdssubr  10145  dvdsadd2b  10146  dvdsabseq  10151  divconjdvds  10153  alzdvds  10158  addmodlteqALT  10163  zeo3  10171  odd2np1lem  10175  odd2np1  10176  even2n  10177  oddp1even  10179  mulsucdiv2z  10189  zob  10195  ltoddhalfle  10197  halfleoddlt  10198  opoe  10199  omoe  10200  opeo  10201  omeo  10202  m1exp1  10205  sqrt2irr  10223
  Copyright terms: Public domain W3C validator