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