Theorem 2timesgt

Description: Double of a positive real is larger than the real itself. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	2timesgt	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 < ( 2 · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2		id	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ+ )
3	1 2	ltaddrp2d	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 < ( 𝐴 + 𝐴 ) )
4		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
5		2times	⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
6	5	eqcomd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 𝐴 ) = ( 2 · 𝐴 ) )
7	4 6	syl	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 + 𝐴 ) = ( 2 · 𝐴 ) )
8	3 7	breqtrd	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 < ( 2 · 𝐴 ) )