![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > zcn | Unicode version |
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.) |
Ref | Expression |
---|---|
zcn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre 8852 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | recnd 7613 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-resscn 7534 |
This theorem depends on definitions: df-bi 116 df-3or 928 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-rex 2376 df-rab 2379 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-iota 5014 df-fv 5057 df-ov 5693 df-neg 7753 df-z 8849 |
This theorem is referenced by: zsscn 8856 zaddcllempos 8885 peano2zm 8886 zaddcllemneg 8887 zaddcl 8888 zsubcl 8889 zrevaddcl 8898 nzadd 8900 zlem1lt 8904 zltlem1 8905 zapne 8919 zdiv 8933 zdivadd 8934 zdivmul 8935 zextlt 8937 zneo 8946 zeo2 8951 peano5uzti 8953 zindd 8963 divfnzn 9205 qmulz 9207 zq 9210 qaddcl 9219 qnegcl 9220 qmulcl 9221 qreccl 9226 fzen 9606 uzsubsubfz 9610 fz01en 9616 fzmmmeqm 9621 fzsubel 9623 fztp 9641 fzsuc2 9642 fzrev2 9648 fzrev3 9650 elfzp1b 9660 fzrevral 9668 fzrevral2 9669 fzrevral3 9670 fzshftral 9671 fzoaddel2 9753 fzosubel2 9755 eluzgtdifelfzo 9757 fzocatel 9759 elfzom1elp1fzo 9762 fzval3 9764 zpnn0elfzo1 9768 fzosplitprm1 9794 fzoshftral 9798 flqzadd 9854 2tnp1ge0ge0 9857 ceilid 9871 intfracq 9876 zmod10 9896 modqmuladdnn0 9924 addmodlteq 9954 frecfzen2 9983 ser3mono 10044 m1expeven 10133 expsubap 10134 zesq 10203 sqoddm1div8 10237 bccmpl 10293 shftuz 10382 nnabscl 10664 climshftlemg 10861 climshft 10863 mptfzshft 11000 fsumrev 11001 fisum0diag2 11005 efexp 11136 efzval 11137 demoivre 11226 dvdsval2 11241 iddvds 11251 1dvds 11252 dvds0 11253 negdvdsb 11254 dvdsnegb 11255 0dvds 11258 dvdsmul1 11260 iddvdsexp 11262 muldvds1 11263 muldvds2 11264 dvdscmul 11265 dvdsmulc 11266 summodnegmod 11269 modmulconst 11270 dvds2ln 11271 dvds2add 11272 dvds2sub 11273 dvdstr 11275 dvdssub2 11280 dvdsadd 11281 dvdsaddr 11282 dvdssub 11283 dvdssubr 11284 dvdsadd2b 11285 dvdsabseq 11290 divconjdvds 11292 alzdvds 11297 addmodlteqALT 11302 zeo3 11310 odd2np1lem 11314 odd2np1 11315 even2n 11316 oddp1even 11318 mulsucdiv2z 11327 zob 11333 ltoddhalfle 11335 halfleoddlt 11336 opoe 11337 omoe 11338 opeo 11339 omeo 11340 m1exp1 11343 divalgb 11367 divalgmod 11369 modremain 11371 ndvdssub 11372 ndvdsadd 11373 flodddiv4 11376 flodddiv4t2lthalf 11379 gcdneg 11415 gcdadd 11418 gcdid 11419 modgcd 11424 dvdsgcd 11443 mulgcd 11447 absmulgcd 11448 mulgcdr 11449 gcddiv 11450 gcdmultiplez 11452 dvdssqim 11455 dvdssq 11462 bezoutr1 11464 lcmneg 11498 lcmgcdlem 11501 lcmgcd 11502 lcmid 11504 lcm1 11505 coprmdvds 11516 coprmdvds2 11517 qredeq 11520 qredeu 11521 divgcdcoprmex 11526 cncongr1 11527 cncongr2 11528 prmdvdsexp 11569 rpexp1i 11575 sqrt2irr 11583 divnumden 11616 phiprmpw 11640 |
Copyright terms: Public domain | W3C validator |