![]() |
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 8591 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
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-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-resscn 7534 ax-1re 7536 ax-addrcl 7539 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-in 3019 df-ss 3026 df-2 8579 |
This theorem is referenced by: cnm2m1cnm3 8765 xp1d2m1eqxm1d2 8766 nneo 8948 zeo2 8951 2tnp1ge0ge0 9857 flhalf 9858 q2txmodxeq0 9940 mulbinom2 10201 binom3 10202 zesq 10203 sqoddm1div8 10237 cvg1nlemcxze 10546 resqrexlemover 10574 resqrexlemlo 10577 resqrexlemcalc1 10578 resqrexlemnm 10582 amgm2 10682 maxabslemab 10770 maxabslemlub 10771 max0addsup 10783 minabs 10798 bdtri 10802 trirecip 11060 geo2sum 11073 ege2le3 11126 efgt0 11139 tanval3ap 11170 even2n 11317 oddm1even 11318 oddp1even 11319 mulsucdiv2z 11328 ltoddhalfle 11336 m1exp1 11344 nn0enne 11345 flodddiv4 11377 flodddiv4t2lthalf 11380 sqrt2irrlem 11583 sqrt2irr 11584 pw2dvdslemn 11586 pw2dvdseulemle 11588 oddpwdc 11595 sqrt2irraplemnn 11600 oddennn 11648 evenennn 11649 |
Copyright terms: Public domain | W3C validator |