Theorem sgnp

Description: The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015)

	Ref	Expression
Assertion	sgnp	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( sgn ‘ 𝐴 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		sgnval	⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
3		0xr	⊢ 0 ∈ ℝ*
4		xrltne	⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
5	3 4	mp3an1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
6	5	neneqd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ¬ 𝐴 = 0 )
7	6	iffalsed	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) = if ( 𝐴 < 0 , - 1 , 1 ) )
8		xrltnsym	⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 0 < 𝐴 → ¬ 𝐴 < 0 ) )
9	3 8	mpan	⊢ ( 𝐴 ∈ ℝ* → ( 0 < 𝐴 → ¬ 𝐴 < 0 ) )
10	9	imp	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ¬ 𝐴 < 0 )
11	10	iffalsed	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → if ( 𝐴 < 0 , - 1 , 1 ) = 1 )
12	2 7 11	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( sgn ‘ 𝐴 ) = 1 )