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\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2	1	subidi	$$⊢1-1=0$$
3		1re	$$⊢1\in ℝ$$
4	3 3	resubcli	$$⊢1-1\in ℝ$$
5	2 4	eqeltrri	$$⊢0\in ℝ$$