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 ( ( ๐ด โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( โŒŠ โ€˜ ( ๐ด / ๐‘€ ) ) / ๐‘ ) ) = ( โŒŠ โ€˜ ( ๐ด / ( ๐‘€ ยท ๐‘ ) ) ) )

Proof

Step Hyp Ref Expression
1 nndivre โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ๐ด / ๐‘€ ) โˆˆ โ„ )
2 fldiv โŠข ( ( ( ๐ด / ๐‘€ ) โˆˆ โ„ โˆง ๐‘ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( โŒŠ โ€˜ ( ๐ด / ๐‘€ ) ) / ๐‘ ) ) = ( โŒŠ โ€˜ ( ( ๐ด / ๐‘€ ) / ๐‘ ) ) )
3 1 2 stoic3 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( โŒŠ โ€˜ ( ๐ด / ๐‘€ ) ) / ๐‘ ) ) = ( โŒŠ โ€˜ ( ( ๐ด / ๐‘€ ) / ๐‘ ) ) )
4 recn โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚ )
5 nncn โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„‚ )
6 nnne0 โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โ‰  0 )
7 5 6 jca โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โˆˆ โ„‚ โˆง ๐‘€ โ‰  0 ) )
8 nncn โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚ )
9 nnne0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0 )
10 8 9 jca โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0 ) )
11 divdiv1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘€ โˆˆ โ„‚ โˆง ๐‘€ โ‰  0 ) โˆง ( ๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0 ) ) โ†’ ( ( ๐ด / ๐‘€ ) / ๐‘ ) = ( ๐ด / ( ๐‘€ ยท ๐‘ ) ) )
12 4 7 10 11 syl3an โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) โ†’ ( ( ๐ด / ๐‘€ ) / ๐‘ ) = ( ๐ด / ( ๐‘€ ยท ๐‘ ) ) )
13 12 fveq2d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( ๐ด / ๐‘€ ) / ๐‘ ) ) = ( โŒŠ โ€˜ ( ๐ด / ( ๐‘€ ยท ๐‘ ) ) ) )
14 3 13 eqtrd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( โŒŠ โ€˜ ( ๐ด / ๐‘€ ) ) / ๐‘ ) ) = ( โŒŠ โ€˜ ( ๐ด / ( ๐‘€ ยท ๐‘ ) ) ) )