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 0 A N A N A

Proof

Step Hyp Ref Expression
1 reflcl A A
2 1 adantl N 0 A A
3 simpr N 0 A A
4 simpl N 0 A N 0
5 4 nn0red N 0 A N
6 4 nn0ge0d N 0 A 0 N
7 flle A A A
8 7 adantl N 0 A A A
9 2 3 5 6 8 lemul2ad N 0 A N A N A
10 5 3 remulcld N 0 A N A
11 nn0z N 0 N
12 flcl A A
13 zmulcl N A N A
14 11 12 13 syl2an N 0 A N A
15 flge N A N A N A N A N A N A
16 10 14 15 syl2anc N 0 A N A N A N A N A
17 9 16 mpbid N 0 A N A N A