Metamath Proof Explorer

Theorem 0reALT

Description: Alternate proof of 0re . (Contributed by NM, 19-Feb-2005) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 0reALT 
|- 0 e. RR

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 1 subidi 
 |-  ( 1 - 1 ) = 0
3 1re 
 |-  1 e. RR
4 3 3 resubcli 
 |-  ( 1 - 1 ) e. RR
5 2 4 eqeltrri 
 |-  0 e. RR