# Metamath Proof Explorer

## Axiom ax-cnre

Description: A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of Gleason p. 130. Axiom 17 of 22 for real and complex numbers, justified by theorem axcnre . For naming consistency, use cnre for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999)

Ref Expression
Assertion ax-cnre ${⊢}{A}\in ℂ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cc ${class}ℂ$
2 0 1 wcel ${wff}{A}\in ℂ$
3 vx ${setvar}{x}$
4 cr ${class}ℝ$
5 vy ${setvar}{y}$
6 3 cv ${setvar}{x}$
7 caddc ${class}+$
8 ci ${class}\mathrm{i}$
9 cmul ${class}×$
10 5 cv ${setvar}{y}$
11 8 10 9 co ${class}\mathrm{i}{y}$
12 6 11 7 co ${class}\left({x}+\mathrm{i}{y}\right)$
13 0 12 wceq ${wff}{A}={x}+\mathrm{i}{y}$
14 13 5 4 wrex ${wff}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}$
15 14 3 4 wrex ${wff}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}$
16 2 15 wi ${wff}\left({A}\in ℂ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}\right)$