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

Metamath Proof Explorer

Theorem neglt

Description: The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	neglt	⊢ ( 𝐴 ∈ ℝ⁺ → - 𝐴 < 𝐴 )

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ )
2	1	renegcld	⊢ ( 𝐴 ∈ ℝ⁺ → - 𝐴 ∈ ℝ )
3		0red	⊢ ( 𝐴 ∈ ℝ⁺ → 0 ∈ ℝ )
4		rpgt0	⊢ ( 𝐴 ∈ ℝ⁺ → 0 < 𝐴 )
5	1	lt0neg2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 0 < 𝐴 ↔ - 𝐴 < 0 ) )
6	4 5	mpbid	⊢ ( 𝐴 ∈ ℝ⁺ → - 𝐴 < 0 )
7	2 3 1 6 4	lttrd	⊢ ( 𝐴 ∈ ℝ⁺ → - 𝐴 < 𝐴 )