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

Metamath Proof Explorer

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