![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnre | Structured version Visualization version GIF version |
Description: Alias for ax-cnre 11131, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre | โข (๐ด โ โ โ โ๐ฅ โ โ โ๐ฆ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 11131 | 1 โข (๐ด โ โ โ โ๐ฅ โ โ โ๐ฆ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 = wceq 1542 โ wcel 2107 โwrex 3074 (class class class)co 7362 โcc 11056 โcr 11057 ici 11060 + caddc 11061 ยท cmul 11063 |
This theorem was proved from axioms: ax-cnre 11131 |
This theorem is referenced by: mulid1 11160 1re 11162 0re 11164 mul02 11340 cnegex 11343 0cnALT 11396 recex 11794 creur 12154 creui 12155 cju 12156 cnref1o 12917 replim 15008 ipasslem11 29824 sn-addid2 40902 sn-it0e0 40913 sn-negex12 40914 sn-mulid2 40933 sn-0tie0 40937 sn-mul02 40938 |
Copyright terms: Public domain | W3C validator |