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 ) )