![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nn0cn | Unicode version |
Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.) |
Ref | Expression |
---|---|
nn0cn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0sscn 9006 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3098 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-sep 4054 ax-cnex 7735 ax-resscn 7736 ax-1re 7738 ax-addrcl 7741 ax-rnegex 7753 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ral 2422 df-rex 2423 df-v 2691 df-un 3080 df-in 3082 df-ss 3089 df-sn 3538 df-int 3780 df-inn 8745 df-n0 9002 |
This theorem is referenced by: nn0nnaddcl 9032 elnn0nn 9043 nn0n0n1ge2 9145 uzaddcl 9408 fzctr 9941 nn0split 9944 zpnn0elfzo1 10016 ubmelm1fzo 10034 subfzo0 10050 modqmuladdnn0 10172 addmodidr 10177 modfzo0difsn 10199 nn0ennn 10237 expadd 10366 expmul 10369 bernneq 10443 bernneq2 10444 faclbnd 10519 faclbnd6 10522 bccmpl 10532 bcn0 10533 bcnn 10535 bcnp1n 10537 bcn2 10542 bcp1m1 10543 bcpasc 10544 bcn2p1 10548 hashfzo0 10601 hashfz0 10603 fisum0diag2 11248 hashiun 11279 binom1dif 11288 bcxmas 11290 geolim 11312 efaddlem 11417 efexp 11425 eftlub 11433 demoivreALT 11516 nn0ob 11641 modremain 11662 mulgcdr 11742 nn0seqcvgd 11758 znnen 11947 ennnfonelemp1 11955 |
Copyright terms: Public domain | W3C validator |