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

Proof

Step Hyp Ref Expression
1 0re 0
2 1 recni 0