Metamath Proof Explorer

Theorem sgnrn

Description: The range of the signum function. (Contributed by AV, 16-Jun-2026) (Proof shortened by TA, 21-Jun-2026)

Ref Expression
Assertion sgnrn ⊢ ran ⁡ sgn = − 1 0 1

Proof

Step Hyp Ref Expression
1 df-sgn ⊢ sgn = x ∈ ℝ * ⟼ if x = 0 0 if x < 0 − 1 1
2 1 fnmpt ⊢ ∀ x ∈ ℝ * if x = 0 0 if x < 0 − 1 1 ∈ − 1 0 1 → sgn Fn ℝ *
3 sgnval ⊢ x ∈ ℝ * → sgn ⁡ x = if x = 0 0 if x < 0 − 1 1
4 sgncl ⊢ x ∈ ℝ * → sgn ⁡ x ∈ − 1 0 1
5 3 4 eqeltrrd ⊢ x ∈ ℝ * → if x = 0 0 if x < 0 − 1 1 ∈ − 1 0 1
6 2 5 mprg ⊢ sgn Fn ℝ *
7 4 rgen ⊢ ∀ x ∈ ℝ * sgn ⁡ x ∈ − 1 0 1
8 fnfvrnss ⊢ sgn Fn ℝ * ∧ ∀ x ∈ ℝ * sgn ⁡ x ∈ − 1 0 1 → ran ⁡ sgn ⊆ − 1 0 1
9 6 7 8 mp2an ⊢ ran ⁡ sgn ⊆ − 1 0 1
10 sgnmnf ⊢ sgn ⁡ −∞ = − 1
11 mnfxr ⊢ −∞ ∈ ℝ *
12 fnfvelrn ⊢ sgn Fn ℝ * ∧ −∞ ∈ ℝ * → sgn ⁡ −∞ ∈ ran ⁡ sgn
13 6 11 12 mp2an ⊢ sgn ⁡ −∞ ∈ ran ⁡ sgn
14 10 13 eqeltrri ⊢ − 1 ∈ ran ⁡ sgn
15 sgn0 ⊢ sgn ⁡ 0 = 0
16 0xr ⊢ 0 ∈ ℝ *
17 fnfvelrn ⊢ sgn Fn ℝ * ∧ 0 ∈ ℝ * → sgn ⁡ 0 ∈ ran ⁡ sgn
18 6 16 17 mp2an ⊢ sgn ⁡ 0 ∈ ran ⁡ sgn
19 15 18 eqeltrri ⊢ 0 ∈ ran ⁡ sgn
20 sgn1 ⊢ sgn ⁡ 1 = 1
21 1xr ⊢ 1 ∈ ℝ *
22 fnfvelrn ⊢ sgn Fn ℝ * ∧ 1 ∈ ℝ * → sgn ⁡ 1 ∈ ran ⁡ sgn
23 6 21 22 mp2an ⊢ sgn ⁡ 1 ∈ ran ⁡ sgn
24 20 23 eqeltrri ⊢ 1 ∈ ran ⁡ sgn
25 tpssi ⊢ − 1 ∈ ran ⁡ sgn ∧ 0 ∈ ran ⁡ sgn ∧ 1 ∈ ran ⁡ sgn → − 1 0 1 ⊆ ran ⁡ sgn
26 14 19 24 25 mp3an ⊢ − 1 0 1 ⊆ ran ⁡ sgn
27 9 26 eqssi ⊢ ran ⁡ sgn = − 1 0 1