This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )
4 readdcl 
 |-  ( ( 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 )
9 8 adantr 
 |-  ( ( x e. RR /\ E. y e. RR _i = ( x + ( _i x. y ) ) ) -> 0 e. RR )
10 9 rexlimiva 
 |-  ( E. x e. RR E. y e. RR _i = ( x + ( _i x. y ) ) -> 0 e. RR )
11 1 2 10 mp2b 
 |-  0 e. RR
12 11 recni 
 |-  0 e. CC