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