Metamath Proof Explorer


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
|- ( A e. RR+ -> A < ( 2 x. A ) )

Proof

Step Hyp Ref Expression
1 rpre
 |-  ( A e. RR+ -> A e. RR )
2 id
 |-  ( A e. RR+ -> A e. RR+ )
3 1 2 ltaddrp2d
 |-  ( A e. RR+ -> A < ( A + A ) )
4 rpcn
 |-  ( A e. RR+ -> A e. CC )
5 2times
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
6 5 eqcomd
 |-  ( A e. CC -> ( A + A ) = ( 2 x. A ) )
7 4 6 syl
 |-  ( A e. RR+ -> ( A + A ) = ( 2 x. A ) )
8 3 7 breqtrd
 |-  ( A e. RR+ -> A < ( 2 x. A ) )