Theorem flzadd

Description: An integer can be moved in and out of the floor of a sum. (Contributed by NM, 2-Jan-2009)

	Ref	Expression
Assertion	flzadd	|- ( ( N e. ZZ /\ A e. RR ) -> ( |_ ` ( N + A ) ) = ( N + ( |_ ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		fladdz	|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A + N ) ) = ( ( |_ ` A ) + N ) )
2		recn	|- ( A e. RR -> A e. CC )
3		zcn	|- ( N e. ZZ -> N e. CC )
4		addcom	|- ( ( A e. CC /\ N e. CC ) -> ( A + N ) = ( N + A ) )
5	2 3 4	syl2an	|- ( ( A e. RR /\ N e. ZZ ) -> ( A + N ) = ( N + A ) )
6	5	fveq2d	|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A + N ) ) = ( |_ ` ( N + A ) ) )
7		reflcl	|- ( A e. RR -> ( |_ ` A ) e. RR )
8	7	recnd	|- ( A e. RR -> ( |_ ` A ) e. CC )
9		addcom	|- ( ( ( |_ ` A ) e. CC /\ N e. CC ) -> ( ( |_ ` A ) + N ) = ( N + ( |_ ` A ) ) )
10	8 3 9	syl2an	|- ( ( A e. RR /\ N e. ZZ ) -> ( ( |_ ` A ) + N ) = ( N + ( |_ ` A ) ) )
11	1 6 10	3eqtr3d	|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( N + A ) ) = ( N + ( |_ ` A ) ) )
12	11	ancoms	|- ( ( N e. ZZ /\ A e. RR ) -> ( |_ ` ( N + A ) ) = ( N + ( |_ ` A ) ) )