Metamath Proof Explorer


Theorem flmulnn0

Description: Move a nonnegative integer in and out of a floor. (Contributed by NM, 2-Jan-2009) (Proof shortened by Fan Zheng, 7-Jun-2016)

Ref Expression
Assertion flmulnn0
|- ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) )

Proof

Step Hyp Ref Expression
1 reflcl
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
2 1 adantl
 |-  ( ( N e. NN0 /\ A e. RR ) -> ( |_ ` A ) e. RR )
3 simpr
 |-  ( ( N e. NN0 /\ A e. RR ) -> A e. RR )
4 simpl
 |-  ( ( N e. NN0 /\ A e. RR ) -> N e. NN0 )
5 4 nn0red
 |-  ( ( N e. NN0 /\ A e. RR ) -> N e. RR )
6 4 nn0ge0d
 |-  ( ( N e. NN0 /\ A e. RR ) -> 0 <_ N )
7 flle
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
8 7 adantl
 |-  ( ( N e. NN0 /\ A e. RR ) -> ( |_ ` A ) <_ A )
9 2 3 5 6 8 lemul2ad
 |-  ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) <_ ( N x. A ) )
10 5 3 remulcld
 |-  ( ( N e. NN0 /\ A e. RR ) -> ( N x. A ) e. RR )
11 nn0z
 |-  ( N e. NN0 -> N e. ZZ )
12 flcl
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
13 zmulcl
 |-  ( ( N e. ZZ /\ ( |_ ` A ) e. ZZ ) -> ( N x. ( |_ ` A ) ) e. ZZ )
14 11 12 13 syl2an
 |-  ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) e. ZZ )
15 flge
 |-  ( ( ( N x. A ) e. RR /\ ( N x. ( |_ ` A ) ) e. ZZ ) -> ( ( N x. ( |_ ` A ) ) <_ ( N x. A ) <-> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) ) )
16 10 14 15 syl2anc
 |-  ( ( N e. NN0 /\ A e. RR ) -> ( ( N x. ( |_ ` A ) ) <_ ( N x. A ) <-> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) ) )
17 9 16 mpbid
 |-  ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) )