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 ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2	1	subidi	⊢ ( 1 − 1 ) = 0
3		1re	⊢ 1 ∈ ℝ
4	3 3	resubcli	⊢ ( 1 − 1 ) ∈ ℝ
5	2 4	eqeltrri	⊢ 0 ∈ ℝ