# Metamath Proof Explorer

## Theorem 0cnALT

Description: Alternate proof of 0cn which does not reference ax-1cn . (Contributed by NM, 19-Feb-2005) (Revised by Mario Carneiro, 27-May-2016) Reduce dependencies on axioms. (Revised by Steven Nguyen, 7-Jan-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 0cnALT
`|- 0 e. CC`

### Proof

Step Hyp Ref Expression
1 ax-icn
` |-  _i e. CC`
2 cnre
` |-  ( _i e. CC -> E. x e. RR E. y e. RR _i = ( x + ( _i x. y ) ) )`
3 ax-rnegex
` |-  ( x e. RR -> E. z e. RR ( x + z ) = 0 )`
` |-  ( ( x e. RR /\ z e. RR ) -> ( x + z ) e. RR )`
5 eleq1
` |-  ( ( x + z ) = 0 -> ( ( x + z ) e. RR <-> 0 e. RR ) )`
6 4 5 syl5ibcom
` |-  ( ( x e. RR /\ z e. RR ) -> ( ( x + z ) = 0 -> 0 e. RR ) )`
7 6 rexlimdva
` |-  ( x e. RR -> ( E. z e. RR ( x + z ) = 0 -> 0 e. RR ) )`
8 3 7 mpd
` |-  ( x e. RR -> 0 e. RR )`
` |-  ( ( x e. RR /\ E. y e. RR _i = ( x + ( _i x. y ) ) ) -> 0 e. RR )`
` |-  ( E. x e. RR E. y e. RR _i = ( x + ( _i x. y ) ) -> 0 e. RR )`
` |-  0 e. RR`
` |-  0 e. CC`