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 8689 | . 2 | |
2 | 1 | sseli 3063 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 cc 7586 cn 8684 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-sep 4016 ax-cnex 7679 ax-resscn 7680 ax-1re 7682 ax-addrcl 7685 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-ral 2398 df-v 2662 df-in 3047 df-ss 3054 df-int 3742 df-inn 8685 |
This theorem is referenced by: nn1m1nn 8702 nn1suc 8703 nnaddcl 8704 nnmulcl 8705 nnsub 8723 nndiv 8725 nndivtr 8726 nnnn0addcl 8965 nn0nnaddcl 8966 elnnnn0 8978 nnnegz 9015 zaddcllempos 9049 zaddcllemneg 9051 nnaddm1cl 9073 elz2 9080 zdiv 9097 zdivadd 9098 zdivmul 9099 nneoor 9111 nneo 9112 divfnzn 9369 qmulz 9371 qaddcl 9383 qnegcl 9384 qmulcl 9385 qreccl 9390 nnledivrp 9508 nn0ledivnn 9509 fseq1m1p1 9830 nnsplit 9869 ubmelm1fzo 9958 subfzo0 9974 flqdiv 10049 addmodidr 10101 modfzo0difsn 10123 nn0ennn 10161 expnegap0 10256 expm1t 10276 nnsqcl 10317 nnlesq 10351 facdiv 10439 facndiv 10440 faclbnd 10442 bcn1 10459 bcn2m1 10470 arisum 11222 arisum2 11223 expcnvap0 11226 mertenslem2 11260 ef0lem 11280 efexp 11302 nndivides 11412 modmulconst 11437 dvdsflip 11461 nn0enne 11511 nno 11515 divalgmod 11536 ndvdsadd 11540 modgcd 11591 gcddiv 11619 gcdmultiple 11620 gcdmultiplez 11621 rpmulgcd 11626 rplpwr 11627 sqgcd 11629 lcmgcdlem 11670 qredeq 11689 qredeu 11690 divgcdcoprm0 11694 cncongrcoprm 11699 prmind2 11713 isprm6 11737 sqrt2irr 11752 oddpwdclemodd 11761 divnumden 11785 divdenle 11786 nn0gcdsq 11789 hashgcdlem 11814 dvexp 12755 |
Copyright terms: Public domain | W3C validator |