Theorem 0cnALT3

Description: Alternate proof of 0cn using ax-resscn , ax-addrcl , ax-rnegex , ax-cnre instead of ax-icn , ax-addcl , ax-mulcl , ax-i2m1 . Version of 0cnALT using ax-1cn instead of ax-icn . (Contributed by Steven Nguyen, 7-Jan-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	0cnALT3	|- 0 e. CC

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2	1	recni	|- 0 e. CC