Theorem zcn 8026

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 8025	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 6851	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1390  ℂcc 6709  ℤcz 8021

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-resscn 6775

This theorem depends on definitions:  df-bi 110  df-3or 885  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-rab 2309  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458  df-neg 6982  df-z 8022

This theorem is referenced by:  zsscn  8029  zaddcllempos  8058  peano2zm  8059  zaddcllemneg  8060  zaddcl  8061  zsubcl  8062  zrevaddcl  8071  zlem1lt  8076  zltlem1  8077  zapne  8091  zdiv  8104  zdivadd  8105  zdivmul  8106  zextlt  8108  zneo  8115  zeo2  8120  peano5uzti  8122  zindd  8132  divfnzn  8332  qmulz  8334  zq  8337  qaddcl  8346  qnegcl  8347  qmulcl  8348  qreccl  8351  fzen  8677  uzsubsubfz  8681  fz01en  8687  fzmmmeqm  8691  fzsubel  8693  fztp  8710  fzsuc2  8711  fzrev2  8717  fzrev3  8719  elfzp1b  8729  fzrevral  8737  fzrevral2  8738  fzrevral3  8739  fzshftral  8740  fzoaddel2  8819  fzosubel2  8821  eluzgtdifelfzo  8823  fzocatel  8825  elfzom1elp1fzo  8828  fzval3  8830  zpnn0elfzo1  8834  fzosplitprm1  8860  fzoshftral  8864  frecfzen2  8885  expsubap  8956  zesq  9020