Metamath Proof Explorer

Theorem flsubz

Description: An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020)

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

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 zcn 
 |-  ( N e. ZZ -> N e. CC )
3 negsub 
 |-  ( ( A e. CC /\ N e. CC ) -> ( A + -u N ) = ( A - N ) )
4 1 2 3 syl2an 
 |-  ( ( A e. RR /\ N e. ZZ ) -> ( A + -u N ) = ( A - N ) )
5 4 eqcomd 
 |-  ( ( A e. RR /\ N e. ZZ ) -> ( A - N ) = ( A + -u N ) )
6 5 fveq2d 
 |-  ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A - N ) ) = ( |_ ` ( A + -u N ) ) )
7 znegcl 
 |-  ( N e. ZZ -> -u N e. ZZ )
8 fladdz 
 |-  ( ( A e. RR /\ -u N e. ZZ ) -> ( |_ ` ( A + -u N ) ) = ( ( |_ ` A ) + -u N ) )
9 7 8 sylan2 
 |-  ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A + -u N ) ) = ( ( |_ ` A ) + -u N ) )
10 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
11 10 recnd 
 |-  ( A e. RR -> ( |_ ` A ) e. CC )
12 negsub 
 |-  ( ( ( |_ ` A ) e. CC /\ N e. CC ) -> ( ( |_ ` A ) + -u N ) = ( ( |_ ` A ) - N ) )
13 11 2 12 syl2an 
 |-  ( ( A e. RR /\ N e. ZZ ) -> ( ( |_ ` A ) + -u N ) = ( ( |_ ` A ) - N ) )
14 6 9 13 3eqtrd 
 |-  ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A - N ) ) = ( ( |_ ` A ) - N ) )