HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: An integer is a complex number. |
| Ref | Expression |
|---|---|
| zcn |
   
 
  |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zre 7348 |
. 2
 | |
| 2 | 1 | recnd 6468 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wi 3 wcel 1300 cc 6384 cz 6451 |
| This theorem is referenced by: zsscn 7352 nn0sub 7370 zsubcl 7377 zrevaddcl 7379 zlem1lt 7392 zltlem1 7393 zdiv 7397 zdivadd 7398 zdivmul 7399 zextlt 7402 zneo 7412 dfuzi 7414 uzindOLD 7420 zindd 7427 zmax 7433 rebtwnz 7435 qaddcl 7449 qnegcl 7450 qmulcl 7451 qreccl 7453 fladdz 7484 flzadd 7485 flhalf 7487 quoremz 7492 intfrac2 7495 intfracq 7496 modcyc 7516 modcyc2 7517 modmul1 7519 peano2uzr 7617 uzaddcl 7618 fzen 7664 fz01en 7665 fzsubel 7673 fztp 7686 fzrev2 7690 fzrev3 7692 fzrevral 7698 fzrevral2 7699 fzrevral3 7700 fzshftral 7701 seqz1 7790 seqzp1 7791 seqzm1 7792 seqzval2 7796 nn0abscl 8131 fsum0split 8281 fsum3 8284 fsum4 8285 fsumrev 8289 fsumrev2 8290 fsumshft 8291 fsumshftm 8292 fsumconst 8298 fsum0 8299 serzsplit 8316 binomlem1 8326 binomlem2 8327 climshfti 8364 climshft2i 8366 iserzshft2i 8367 iserzshfti 8404 iserzexi 8406 isumshfti 8465 isumshft2i 8466 arisumilem 8486 arisumi 8487 fsum0diaglem2 8519 fsum0diag2 8521 efaddlem14 8613 efaddlem16 8615 eirrlem2 8652 znnenlem 8770 znnen 8771 gxneg 9389 gxsuc 9395 gxnn0add 9397 gxadd 9398 gxsub 9399 gxnn0mul 9400 gxmul 9401 gxmodid 9402 zaddsubg 9438 ipasslem5 9835 sinperlem2 10036 sinper 10039 cosper 10040 abssinper 10062 sinkpi 10063 coskpi 10064 efper 10101 pilog 10122 nnabscl 13601 elfzp1b 13605 zmod10 13613 iddvds 13668 1dvds 13669 dvds0 13670 negdvdsb 13671 dvdsnegb 13672 0dvds 13675 dvdsmul1 13676 muldvds1 13678 muldvds2 13679 dvdscmul 13680 dvdsmulc 13681 dvdscmulr 13682 dvdsmulcr 13683 dvds2ln 13684 dvds2add 13685 dvds2sub 13686 dvdstr 13687 dvdsadd 13688 dvdsaddr 13689 dvdssub 13690 dvdssubr 13691 alzdvds 13695 divalglem0 13696 divalglem2 13698 divalglem4 13699 divalglem5 13700 divalglem8 13703 divalglem9 13704 divalgb 13707 divalgmod 13709 ndvdssub 13710 ndvdsadd 13711 gcdneg 13732 gcdaddmlem 13734 gcdaddm 13735 gcdid 13736 modgcd 13738 mulgcd 13763 absmulgcd 13764 dvdsgcd 13765 coprmdvds 13783 rdr 15781 uzp1 15785 fzm1 15796 absrdbnd 15799 fdc 15812 fsumltisumi 15823 fsumlt1 15831 mettrifi2 15848 geomcau 15849 caushft 15851 heiborlem30 15984 heiborlem35 15989 rrntotbndlem1 16020 zaddablxNEW 17141 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-fv 4014 df-opr 4886 df-oprab 4887 df-1st 5020 df-2nd 5021 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 df-enr 6318 df-nr 6319 df-0r 6323 df-c 6392 df-r 6396 df-neg 6513 df-z 7345 |