This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( |_ ` ( A / M ) ) / N ) ) = ( |_ ` ( A / ( M x. N ) ) ) )

Proof

Step Hyp Ref Expression
1 nndivre 
 |-  ( ( A e. RR /\ M e. NN ) -> ( A / M ) e. RR )
2 fldiv 
 |-  ( ( ( A / M ) e. RR /\ N e. NN ) -> ( |_ ` ( ( |_ ` ( A / M ) ) / N ) ) = ( |_ ` ( ( A / M ) / N ) ) )
3 1 2 stoic3 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( |_ ` ( A / M ) ) / N ) ) = ( |_ ` ( ( A / M ) / N ) ) )
4 recn 
 |-  ( A e. RR -> A e. CC )
5 nncn 
 |-  ( M e. NN -> M e. CC )
6 nnne0 
 |-  ( M e. NN -> M =/= 0 )
7 5 6 jca 
 |-  ( M e. NN -> ( M e. CC /\ M =/= 0 ) )
8 nncn 
 |-  ( N e. NN -> N e. CC )
9 nnne0 
 |-  ( N e. NN -> N =/= 0 )
10 8 9 jca 
 |-  ( N e. NN -> ( N e. CC /\ N =/= 0 ) )
11 divdiv1 
 |-  ( ( A e. CC /\ ( M e. CC /\ M =/= 0 ) /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( A / M ) / N ) = ( A / ( M x. N ) ) )
12 4 7 10 11 syl3an 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( ( A / M ) / N ) = ( A / ( M x. N ) ) )
13 12 fveq2d 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( A / M ) / N ) ) = ( |_ ` ( A / ( M x. N ) ) ) )
14 3 13 eqtrd 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( |_ ` ( A / M ) ) / N ) ) = ( |_ ` ( A / ( M x. N ) ) ) )