![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnre | GIF version |
Description: Alias for ax-cnre 7921, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre | ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 7921 | 1 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ∈ wcel 2148 ∃wrex 2456 (class class class)co 5874 ℂcc 7808 ℝcr 7809 ici 7812 + caddc 7813 · cmul 7815 |
This theorem was proved from axioms: ax-cnre 7921 |
This theorem is referenced by: mulrid 7953 cnegexlem2 8131 cnegex 8133 apirr 8560 apsym 8561 apcotr 8562 apadd1 8563 apneg 8566 mulext1 8567 apti 8577 recexap 8608 creur 8914 creui 8915 cju 8916 cnref1o 9648 replim 10863 cjap 10910 |
Copyright terms: Public domain | W3C validator |