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 10767, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre | ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 10767 | 1 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 ∃wrex 3052 (class class class)co 7191 ℂcc 10692 ℝcr 10693 ici 10696 + caddc 10697 · cmul 10699 |
This theorem was proved from axioms: ax-cnre 10767 |
This theorem is referenced by: mulid1 10796 1re 10798 0re 10800 mul02 10975 cnegex 10978 0cnALT 11031 recex 11429 creur 11789 creui 11790 cju 11791 cnref1o 12546 replim 14644 ipasslem11 28875 sn-addid2 40036 sn-it0e0 40046 sn-negex12 40047 sn-mulid2 40066 sn-0tie0 40070 sn-mul02 40071 |
Copyright terms: Public domain | W3C validator |