Metamath Proof Explorer


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