This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reds

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

Ref Expression
Assertion reds ( abs ∘ − ) = ( dist ‘ ℝfld )

Proof

Step Hyp Ref Expression
1 reex ⊢ ℝ ∈ V
2 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
3 cnfldds ⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
4 2 3 ressds ⊢ ( ℝ ∈ V → ( abs ∘ − ) = ( dist ‘ ℝfld ) )
5 1 4 ax-mp ⊢ ( abs ∘ − ) = ( dist ‘ ℝfld )