Theorem reds

Description: The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019)

	Ref	Expression
Assertion	reds	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		reex	$$⊢ℝ\in \mathrm{V}$$
2		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
3		cnfldds	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$$
4	2 3	ressds	$$⊢ℝ\in \mathrm{V}\to \mathrm{abs}\circ -=\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)$$
5	1 4	ax-mp	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)$$