![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nncn | Unicode version |
Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
Ref | Expression |
---|---|
nncn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnsscn 8749 |
. 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 |
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-v 2691 df-in 3082 df-ss 3089 df-int 3780 df-inn 8745 |
This theorem is referenced by: nn1m1nn 8762 nn1suc 8763 nnaddcl 8764 nnmulcl 8765 nnsub 8783 nndiv 8785 nndivtr 8786 nnnn0addcl 9031 nn0nnaddcl 9032 elnnnn0 9044 nnnegz 9081 zaddcllempos 9115 zaddcllemneg 9117 nnaddm1cl 9139 elz2 9146 zdiv 9163 zdivadd 9164 zdivmul 9165 nneoor 9177 nneo 9178 divfnzn 9440 qmulz 9442 qaddcl 9454 qnegcl 9455 qmulcl 9456 qreccl 9461 nnledivrp 9583 nn0ledivnn 9584 fseq1m1p1 9906 nnsplit 9945 ubmelm1fzo 10034 subfzo0 10050 flqdiv 10125 addmodidr 10177 modfzo0difsn 10199 nn0ennn 10237 expnegap0 10332 expm1t 10352 nnsqcl 10393 nnlesq 10427 facdiv 10516 facndiv 10517 faclbnd 10519 bcn1 10536 bcn2m1 10547 arisum 11299 arisum2 11300 expcnvap0 11303 mertenslem2 11337 ef0lem 11403 efexp 11425 nndivides 11536 modmulconst 11561 dvdsflip 11585 nn0enne 11635 nno 11639 divalgmod 11660 ndvdsadd 11664 modgcd 11715 gcddiv 11743 gcdmultiple 11744 gcdmultiplez 11745 rpmulgcd 11750 rplpwr 11751 sqgcd 11753 lcmgcdlem 11794 qredeq 11813 qredeu 11814 divgcdcoprm0 11818 cncongrcoprm 11823 prmind2 11837 isprm6 11861 sqrt2irr 11876 oddpwdclemodd 11886 divnumden 11910 divdenle 11911 nn0gcdsq 11914 hashgcdlem 11939 dvexp 12883 rpcxproot 13042 logbgcd1irr 13092 |
Copyright terms: Public domain | W3C validator |