![]() |
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 11231, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre | ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 11231 | 1 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 ∃wrex 3060 (class class class)co 7424 ℂcc 11156 ℝcr 11157 ici 11160 + caddc 11161 · cmul 11163 |
This theorem was proved from axioms: ax-cnre 11231 |
This theorem is referenced by: mulrid 11262 1re 11264 0re 11266 mul02 11442 cnegex 11445 0cnALT 11498 recex 11896 creur 12258 creui 12259 cju 12260 cnref1o 13021 replim 15121 ipasslem11 30773 sn-addlid 42184 sn-it0e0 42195 sn-negex12 42196 sn-mullid 42215 sn-0tie0 42219 sn-mul02 42220 |
Copyright terms: Public domain | W3C validator |