Metamath Proof Explorer


Theorem fldiv2

Description: Cancellation of an embedded floor of a ratio. Generalization of Equation 2.4 in CormenLeisersonRivest p. 33 (where A must be an integer). (Contributed by NM, 9-Nov-2008)

Ref Expression
Assertion fldiv2 A M N A M N = A M N

Proof

Step Hyp Ref Expression
1 nndivre A M A M
2 fldiv A M N A M N = A M N
3 1 2 stoic3 A M N A M N = A M N
4 recn A A
5 nncn M M
6 nnne0 M M 0
7 5 6 jca M M M 0
8 nncn N N
9 nnne0 N N 0
10 8 9 jca N N N 0
11 divdiv1 A M M 0 N N 0 A M N = A M N
12 4 7 10 11 syl3an A M N A M N = A M N
13 12 fveq2d A M N A M N = A M N
14 3 13 eqtrd A M N A M N = A M N