Metamath Proof Explorer

Theorem nnmulge

Description: Multiplying by a positive integer M yields greater than or equal nonnegative integers. (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Assertion nnmulge 
|- ( ( M e. NN /\ N e. NN0 ) -> N <_ ( M x. N ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( M e. NN /\ N e. NN0 ) -> N e. NN0 )
2 1 nn0cnd 
 |-  ( ( M e. NN /\ N e. NN0 ) -> N e. CC )
3 2 mulid2d 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( 1 x. N ) = N )
4 1red 
 |-  ( ( M e. NN /\ N e. NN0 ) -> 1 e. RR )
5 nnre 
 |-  ( M e. NN -> M e. RR )
6 5 adantr 
 |-  ( ( M e. NN /\ N e. NN0 ) -> M e. RR )
7 1 nn0red 
 |-  ( ( M e. NN /\ N e. NN0 ) -> N e. RR )
8 1 nn0ge0d 
 |-  ( ( M e. NN /\ N e. NN0 ) -> 0 <_ N )
9 nnge1 
 |-  ( M e. NN -> 1 <_ M )
10 9 adantr 
 |-  ( ( M e. NN /\ N e. NN0 ) -> 1 <_ M )
11 4 6 7 8 10 lemul1ad 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( 1 x. N ) <_ ( M x. N ) )
12 3 11 eqbrtrrd 
 |-  ( ( M e. NN /\ N e. NN0 ) -> N <_ ( M x. N ) )