HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The number 2 is a complex number. |
| Ref | Expression |
|---|---|
| 2cn |
    |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2re 7163 |
. 2
 | |
| 2 | 1 | recni 6467 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wcel 1300 cc 6384 c2 7145 |
| This theorem is referenced by: 2p2e4 7185 times2 7189 3p3e6 7192 4p3e7 7194 5p3e8 7197 6p3e9 7201 7p3e10 7204 2t2e4 7206 3t3e9 7208 4d2e2 7211 8th4div3 7217 halfpm6th 7218 halfcl 7219 half0 7221 2halves 7225 halfaddsub 7227 addltmul 7229 nneoi 7409 zeo 7411 zneo 7412 flhalf 7487 fztpval 7688 expubnd 7853 sq2 7883 cu2 7885 subsq2 7889 discrlem1 7906 nnesqi 7912 sqr2irrlem1 7974 sqr2irrlem4 7977 cjmulval 8052 recj 8068 imcj 8069 absmax 8149 abs3lemi 8153 fac2 8189 fac3 8190 faclbnd2 8198 faclbnd4lem1 8200 faclbnd4lem3 8202 faclbnd4lem4 8203 faclbnd5 8205 fsum4 8285 climaddlem3 8376 arisumi 8487 erelem2 8582 erelem3 8583 ele3lem 8588 ege2le3lem2 8591 efaddlem8 8607 efaddlem12 8611 efaddlem20 8619 efaddlem22 8621 eirrlem1 8651 ef4pi 8664 sincl 8696 efi4p 8700 sinneg 8707 efival 8712 sinaddi 8716 cosaddi 8717 subcos 8725 cos2tsin 8729 sin01bndlem1 8733 sin01bndlem3 8735 cos01bndlem2 8736 cos01bndlem3 8737 cos1bnd 8740 cos2bnd 8741 cos01gt0 8743 sin02gt0 8744 sin4lt0 8747 znnenlem 8770 znnen 8771 ruclem1 8779 ruclem3 8781 ioo2bl 9190 bcthlem1 9277 bcthlem17 9293 bcthlem21 9297 bcthlem33 9309 ipval2 9696 ipid 9702 cnph 9819 ip0i 9825 ip1ilem 9826 ipdirilem 9829 ubthlem8 9879 ubthlem9 9880 minveclem16 9905 minveclem18 9907 minveclem19 9908 minveclem27 9916 minveclem35 9924 minveclem36 9925 minveclem37 9926 minveclem38 9927 sinco 10016 cosco 10017 sincn 10018 coscn 10019 pilem1 10020 sinhalfpilem 10028 cospi 10031 sin2pi 10033 cos2pi 10034 sinperlem2 10036 sinper 10039 cosper 10040 sin2pim 10041 cos2pim 10042 sinhalfpip 10048 sinhalfpim 10049 coshalfpip 10050 coshalfpim 10051 sincosq3sgn 10055 sincosq4sgn 10056 sinq12gt0t 10057 sincosq1eq 10059 sincos4thpi 10060 sincos6thpi 10061 abssinper 10062 coskpi 10064 sineq0re 10067 cosh111lem1 10068 eff1o 10102 pilog 10122 hvsubcan2i 10563 norm-ii.i 10637 norm3lem 10649 normpar2i 10656 polid2i 10657 hhph 10678 projlem3 10821 projlem4 10822 projlem5 10823 projlem7 10825 projlem18 10836 mayete3i 11308 mayete3OLDi 11309 opsqrlem6 11716 cdj3lem1 12006 addltmulALT 12018 2prm 13779 3prm 13780 3timesi 14523 2eq3m1 14526 cntrsetlem 14999 mslb1 15007 2wsms 15008 msra3 15009 rddif 15798 fsumltisumi 15823 csbrni 15832 trirni 15833 isbnd3 15941 heiborlem32 15986 heiborlem33 15987 phtpycolem2 16052 phtpycolem3 16053 phtpycolem4 16054 phtpyco 16056 pcoval2 16075 pcocn 16076 pco0 16077 pco1 16078 pcohtpylem2 16081 pcohtpylem3 16082 pcohtpy 16083 pcopt 16084 pcoass 16085 pcorevlem 16086 pcorev 16087 stb3xpl 16743 |
| 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-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-mpt 5006 df-1st 5020 df-2nd 5021 df-iota 5089 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-en 5427 df-dom 5428 df-sdom 5429 df-undef 5556 df-riota 5560 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-plp 6240 df-mp 6241 df-ltp 6242 df-plpr 6316 df-mpr 6317 df-enr 6318 df-nr 6319 df-plr 6320 df-mr 6321 df-ltr 6322 df-0r 6323 df-1r 6324 df-m1r 6325 df-c 6392 df-0 6393 df-1 6394 df-i 6395 df-r 6396 df-plus 6397 df-mul 6398 df-sub 6511 df-neg 6513 df-2 7154 |