Metamath Proof Explorer


Theorem lemulge12d

Description: Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses ltp1d.1
|- ( ph -> A e. RR )
divgt0d.2
|- ( ph -> B e. RR )
lemulge11d.3
|- ( ph -> 0 <_ A )
lemulge11d.4
|- ( ph -> 1 <_ B )
Assertion lemulge12d
|- ( ph -> A <_ ( B x. A ) )

Proof

Step Hyp Ref Expression
1 ltp1d.1
 |-  ( ph -> A e. RR )
2 divgt0d.2
 |-  ( ph -> B e. RR )
3 lemulge11d.3
 |-  ( ph -> 0 <_ A )
4 lemulge11d.4
 |-  ( ph -> 1 <_ B )
5 lemulge12
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A <_ ( B x. A ) )
6 1 2 3 4 5 syl22anc
 |-  ( ph -> A <_ ( B x. A ) )