![]() |
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 11226, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre | ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 11226 | 1 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2106 ∃wrex 3068 (class class class)co 7431 ℂcc 11151 ℝcr 11152 ici 11155 + caddc 11156 · cmul 11158 |
This theorem was proved from axioms: ax-cnre 11226 |
This theorem is referenced by: mulrid 11257 1re 11259 0re 11261 mul02 11437 cnegex 11440 0cnALT 11494 recex 11893 creur 12258 creui 12259 cju 12260 cnref1o 13025 replim 15152 ipasslem11 30869 sn-addlid 42411 sn-it0e0 42422 sn-negex12 42423 sn-mullid 42442 sn-0tie0 42446 sn-mul02 42447 |
Copyright terms: Public domain | W3C validator |