Theorem zcn 8250

Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
zcn	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Proof of Theorem zcn

Step	Hyp	Ref	Expression
1		zre 8249	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 7054	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1393  ℂcc 6887  ℤcz 8245

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-resscn 6976

This theorem depends on definitions:  df-bi 110  df-3or 886  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-rab 2315  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515  df-neg 7185  df-z 8246

This theorem is referenced by:  zsscn  8253  zaddcllempos  8282  peano2zm  8283  zaddcllemneg  8284  zaddcl  8285  zsubcl  8286  zrevaddcl  8295  zlem1lt  8300  zltlem1  8301  zapne  8315  zdiv  8328  zdivadd  8329  zdivmul  8330  zextlt  8332  zneo  8339  zeo2  8344  peano5uzti  8346  zindd  8356  divfnzn  8556  qmulz  8558  zq  8561  qaddcl  8570  qnegcl  8571  qmulcl  8572  qreccl  8576  fzen  8907  uzsubsubfz  8911  fz01en  8917  fzmmmeqm  8921  fzsubel  8923  fztp  8940  fzsuc2  8941  fzrev2  8947  fzrev3  8949  elfzp1b  8959  fzrevral  8967  fzrevral2  8968  fzrevral3  8969  fzshftral  8970  fzoaddel2  9049  fzosubel2  9051  eluzgtdifelfzo  9053  fzocatel  9055  elfzom1elp1fzo  9058  fzval3  9060  zpnn0elfzo1  9064  fzosplitprm1  9090  fzoshftral  9094  flqzadd  9140  2tnp1ge0ge0  9143  ceilid  9157  intfracq  9162  zmod10  9182  frecfzen2  9204  iseqshft2  9232  isermono  9237  expsubap  9302  zesq  9367  shftuz  9418  nnabscl  9696  climshftlemg  9823  climshft  9825  sqrt2irr  9878