sgnval2

Description: Value of the signum of a real number, expresssed using absolute value. (Contributed by Thierry Arnoux, 9-Nov-2025)

		Ref	Expression
	Assertion	sgnval2	$⊢ (A \in ℝ \land A \neq 0) \to sgn (A) = \frac{A}{\|A\|}$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℝ$
2		0red	$⊢ (A \in ℝ \land A \neq 0) \to 0 \in ℝ$
3	1	recnd	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℂ$
4	3	adantr	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to A \in ℂ$
5		simplr	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to A \neq 0$
6	4 4 5	divneg2d	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to - \frac{A}{A} = \frac{A}{- A}$
7		simpr	$⊢ (A \in ℝ \land A \neq 0) \to A \neq 0$
8	3 7	dividd	$⊢ (A \in ℝ \land A \neq 0) \to \frac{A}{A} = 1$
9	8	adantr	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to \frac{A}{A} = 1$
10	9	negeqd	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to - \frac{A}{A} = - 1$
11	6 10	eqtr3d	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to \frac{A}{- A} = - 1$
12		absnid	$⊢ (A \in ℝ \land A \leq 0) \to \|A\| = - A$
13	12	adantlr	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to \|A\| = - A$
14	13	oveq2d	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to \frac{A}{\|A\|} = \frac{A}{- A}$
15	1	rexrd	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℝ^{*}$
16	1	adantr	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to A \in ℝ$
17		0red	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to 0 \in ℝ$
18		simpr	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to A \leq 0$
19	7	necomd	$⊢ (A \in ℝ \land A \neq 0) \to 0 \neq A$
20	19	adantr	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to 0 \neq A$
21	16 17 18 20	leneltd	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to A < 0$
22		sgnn	$⊢ (A \in ℝ^{*} \land A < 0) \to sgn (A) = - 1$
23	15 21 22	syl2an2r	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to sgn (A) = - 1$
24	11 14 23	3eqtr4rd	$⊢ ((A \in ℝ \land A \neq 0) \land A \leq 0) \to sgn (A) = \frac{A}{\|A\|}$
25	8	adantr	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to \frac{A}{A} = 1$
26	1	adantr	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to A \in ℝ$
27		simpr	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to 0 \leq A$
28	26 27	absidd	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to \|A\| = A$
29	28	oveq2d	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to \frac{A}{\|A\|} = \frac{A}{A}$
30		simplr	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to A \neq 0$
31	26 27 30	ne0gt0d	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to 0 < A$
32		sgnp	$⊢ (A \in ℝ^{*} \land 0 < A) \to sgn (A) = 1$
33	15 31 32	syl2an2r	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to sgn (A) = 1$
34	25 29 33	3eqtr4rd	$⊢ ((A \in ℝ \land A \neq 0) \land 0 \leq A) \to sgn (A) = \frac{A}{\|A\|}$
35	1 2 24 34	lecasei	$⊢ (A \in ℝ \land A \neq 0) \to sgn (A) = \frac{A}{\|A\|}$

Metamath Proof Explorer

Theorem sgnval2

Proof