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