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

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