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

Theorem nn0cnd 9207
Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1 (𝜑𝐴 ∈ ℕ0)
Assertion
Ref Expression
nn0cnd (𝜑𝐴 ∈ ℂ)

Proof of Theorem nn0cnd
StepHypRef Expression
1 nn0red.1 . . 3 (𝜑𝐴 ∈ ℕ0)
21nn0red 9206 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 7963 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  cc 7787  0cn0 9152
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  ax-sep 4118  ax-cnex 7880  ax-resscn 7881  ax-1re 7883  ax-addrcl 7886  ax-rnegex 7898
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3597  df-int 3843  df-inn 8896  df-n0 9153
This theorem is referenced by:  modsumfzodifsn  10369  addmodlteq  10371  uzennn  10409  expaddzaplem  10536  expaddzap  10537  expmulzap  10539  nn0le2msqd  10670  nn0opthlem1d  10671  nn0opthd  10673  nn0opth2d  10674  facdiv  10689  bcp1n  10712  bcn2m1  10720  bcn2p1  10721  omgadd  10753  fihashssdif  10769  hashdifpr  10771  hashxp  10777  zfz1isolemsplit  10789  zfz1isolem1  10791  fsumconst  11433  hash2iun1dif1  11459  binomlem  11462  bcxmas  11468  arisum  11477  arisum2  11478  mertensabs  11516  effsumlt  11671  dvdsexp  11837  nn0ob  11883  divalglemnn  11893  divalgmod  11902  bezoutlemnewy  11967  bezoutlema  11970  bezoutlemb  11971  mulgcd  11987  absmulgcd  11988  mulgcdr  11989  gcddiv  11990  lcmgcd  12048  lcmid  12050  lcm1  12051  3lcm2e6woprm  12056  6lcm4e12  12057  mulgcddvds  12064  qredeu  12067  divgcdcoprm0  12071  divgcdcoprmex  12072  cncongr1  12073  cncongr2  12074  pw2dvdseulemle  12137  phiprmpw  12192  eulerthlema  12200  prmdiveq  12206  odzdvds  12215  powm2modprm  12222  coprimeprodsq  12227  pceulem  12264  pczpre  12267  pcqmul  12273  pcaddlem  12308  pcmpt  12311  pcmpt2  12312  sumhashdc  12315  pcfac  12318  oddprmdvds  12322  mul4sq  12362  mulgnn0dir  12888  mulgnn0ass  12894  lgslem1  14034  lgsvalmod  14053  2sqlem8  14092
  Copyright terms: Public domain W3C validator