Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn . (Contributed by NM, 12-Apr-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax1cn | |- 1 e. CC |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axresscn | |- RR C_ CC |
|
| 2 | df-1 | |- 1 = <. 1R , 0R >. |
|
| 3 | 1sr | |- 1R e. R. |
|
| 4 | opelreal | |- ( <. 1R , 0R >. e. RR <-> 1R e. R. ) |
|
| 5 | 3 4 | mpbir | |- <. 1R , 0R >. e. RR |
| 6 | 2 5 | eqeltri | |- 1 e. RR |
| 7 | 1 6 | sselii | |- 1 e. CC |