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