Metamath Proof Explorer
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 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
0re |
|
2 |
1
|
recni |
|