Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2cnd | Unicode version |
Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
2cnd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 8936 | . 2 | |
2 | 1 | a1i 9 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2141 cc 7759 c2 8916 |
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-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-resscn 7853 ax-1re 7855 ax-addrcl 7858 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134 df-2 8924 |
This theorem is referenced by: cnm2m1cnm3 9116 xp1d2m1eqxm1d2 9117 nneo 9302 zeo2 9305 2tnp1ge0ge0 10244 flhalf 10245 q2txmodxeq0 10327 mulbinom2 10579 binom3 10580 zesq 10581 sqoddm1div8 10616 cvg1nlemcxze 10933 resqrexlemover 10961 resqrexlemlo 10964 resqrexlemcalc1 10965 resqrexlemnm 10969 amgm2 11069 maxabslemab 11157 maxabslemlub 11158 max0addsup 11170 minabs 11186 bdtri 11190 trirecip 11451 geo2sum 11464 ege2le3 11621 efgt0 11634 tanval3ap 11664 even2n 11820 oddm1even 11821 oddp1even 11822 mulsucdiv2z 11831 ltoddhalfle 11839 m1exp1 11847 nn0enne 11848 flodddiv4 11880 flodddiv4t2lthalf 11883 sqrt2irrlem 12102 sqrt2irr 12103 pw2dvdslemn 12106 pw2dvdseulemle 12108 oddpwdc 12115 sqrt2irraplemnn 12120 prmdiv 12176 pythagtriplem15 12219 pythagtriplem16 12220 pythagtriplem17 12221 4sqlem7 12323 4sqlem10 12326 oddennn 12334 evenennn 12335 sin0pilem2 13456 lgslem1 13654 cvgcmp2nlemabs 14024 trilpolemisumle 14030 apdifflemr 14039 apdiff 14040 |
Copyright terms: Public domain | W3C validator |