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 6040 |
. 2
 | |
| 2 | 1 | recni 5379 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wcel 999 cc 5297 c2 6022 |
| This theorem is referenced by: 2p2e4 6062 times2 6066 3p3e6 6069 4p3e7 6071 5p3e8 6074 6p3e9 6078 7p3e10 6081 2t2e4 6083 3t3e9 6085 4d2e2 6088 8th4div3 6092 halfpm6th 6093 halfcl 6094 half0 6096 2halves 6100 halfaddsub 6102 nneoi 6282 zeo 6284 zneo 6285 flhalf 6358 expubnd 6697 sq2 6727 cu2 6729 subsq2 6732 discrlem1 6746 nnesqi 6752 sqr2irrlem1 6814 sqr2irrlem4 6817 cjmulval 6892 recj 6908 imcj 6909 absmax 6987 abs3lemi 6991 fac2 7027 fac3 7028 faclbnd2 7036 faclbnd4lem1 7038 faclbnd4lem3 7040 faclbnd4lem4 7041 faclbnd5 7043 fsum4 7115 climaddlem3 7206 arisumi 7316 erelem2 7410 erelem3 7411 ele3lem 7416 ege2le3lem2 7419 efaddlem8 7435 efaddlem12 7439 efaddlem20 7447 efaddlem22 7449 eirrlem1 7479 ef4pi 7490 sincl 7522 efi4p 7526 sinneg 7533 efival 7538 sinaddi 7542 cosaddi 7543 subcos 7551 cos2tsin 7555 sin01bndlem1 7559 sin01bndlem3 7561 cos01bndlem2 7562 cos01bndlem3 7563 cos1bnd 7566 cos2bnd 7567 cos01gt0 7569 sin02gt0 7570 sin4lt0 7573 znnenlem 7593 znnen 7594 ruclem1 7602 ruclem3 7604 ioo2bl 7997 bcthlem1 8084 bcthlem17 8100 bcthlem21 8104 bcthlem33 8116 ipval2 8441 ipid 8447 cnph 8562 ip0i 8568 ip1ilem 8569 ipdirilem 8572 ubthlem8 8620 ubthlem9 8621 minveclem16 8644 minveclem18 8646 minveclem19 8647 minveclem27 8655 minveclem35 8663 minveclem36 8664 minveclem37 8665 minveclem38 8666 sinco 8750 cosco 8751 sincn 8752 coscn 8753 pilem1 8754 sinhalfpilem 8762 cospi 8765 sin2pi 8767 cos2pi 8768 sinperlem2 8770 sinper 8773 cosper 8774 sin2pim 8775 cos2pim 8776 sinkpi 8780 sinhalfpip 8782 sinhalfpim 8783 coshalfpip 8784 coshalfpim 8785 sincosq3sgn 8789 sincosq4sgn 8790 sinq12gt0t 8791 sincosq1eq 8792 sincos4thpi 8793 sincos6thpi 8794 abssinper 8795 cosh111lem1 8797 eff1o 8831 pilog 8851 hvsubcan2i 9014 norm-ii.i 9087 norm3lem 9099 normpar2i 9106 polid2i 9107 hhph 9128 projlem3 9271 projlem4 9272 projlem5 9273 projlem7 9275 projlem18 9286 mayete3i 9756 cdj3lem1 10445 mslb1 10711 2wsms 10712 msra3 10713 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1003 ax-gen 1004 ax-8 1005 ax-9 1006 ax-10 1007 ax-11 1008 ax-12 1009 ax-13 1010 ax-14 1011 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 ax-9o 1164 ax-10o 1182 ax-16 1252 ax-11o 1260 ax-ext 1504 ax-rep 2748 ax-sep 2758 ax-nul 2765 ax-pow 2798 ax-pr 2835 ax-un 2922 ax-inf2 4687 |
| This theorem depends on definitions: df-bi 154 df-or 231 df-an 232 df-3or 788 df-3an 789 df-ex 1022 df-sb 1214 df-eu 1424 df-mo 1425 df-clab 1510 df-cleq 1515 df-clel 1518 df-ne 1634 df-ral 1696 df-rex 1697 df-reu 1698 df-rab 1699 df-v 1859 df-sbc 1989 df-csb 2052 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-pss 2106 df-nul 2332 df-if 2414 df-pw 2454 df-sn 2464 df-pr 2465 df-tp 2467 df-op 2468 df-uni 2558 df-int 2588 df-iun 2622 df-br 2675 df-opab 2722 df-tr 2736 df-eprel 2888 df-id 2891 df-po 2896 df-so 2906 df-fr 2974 df-we 2991 df-ord 3008 df-on 3009 df-lim 3010 df-suc 3011 df-om 3189 df-xp 3241 df-rel 3242 df-cnv 3243 df-co 3244 df-dm 3245 df-rn 3246 df-res 3247 df-ima 3248 df-fun 3249 df-fn 3250 df-f 3251 df-fv 3255 df-rdg 3990 df-opr 4023 df-oprab 4024 df-1st 4137 df-2nd 4138 df-1o 4191 df-oadd 4193 df-omul 4194 df-er 4319 df-ec 4321 df-qs 4324 df-ni 5065 df-pli 5066 df-mi 5067 df-lti 5068 df-plpq 5100 df-mpq 5101 df-enq 5102 df-nq 5103 df-plq 5104 df-mq 5105 df-rq 5106 df-ltq 5107 df-1q 5108 df-np 5151 df-1p 5152 df-plp 5153 df-mp 5154 df-ltp 5155 df-plpr 5229 df-mpr 5230 df-enr 5231 df-nr 5232 df-plr 5233 df-mr 5234 df-ltr 5235 df-0r 5236 df-1r 5237 df-m1r 5238 df-c 5305 df-0 5306 df-1 5307 df-i 5308 df-r 5309 df-plus 5310 df-mul 5311 df-sub 5421 df-neg 5423 df-2 6031 |