Description: _i is a complex number. Axiom 3 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn . (Contributed by NM, 23-Feb-1996) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axicn | |- _i e. CC |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0r | |- 0R e. R. |
|
| 2 | 1sr | |- 1R e. R. |
|
| 3 | df-i | |- _i = <. 0R , 1R >. |
|
| 4 | 3 | eleq1i | |- ( _i e. CC <-> <. 0R , 1R >. e. CC ) |
| 5 | opelcn | |- ( <. 0R , 1R >. e. CC <-> ( 0R e. R. /\ 1R e. R. ) ) |
|
| 6 | 4 5 | bitri | |- ( _i e. CC <-> ( 0R e. R. /\ 1R e. R. ) ) |
| 7 | 1 2 6 | mpbir2an | |- _i e. CC |