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 N A N = A N

Proof

Step Hyp Ref Expression
1 recn A A
2 zcn N N
3 negsub A N A + -N = A N
4 1 2 3 syl2an A N A + -N = A N
5 4 eqcomd A N A N = A + -N
6 5 fveq2d A N A N = A + -N
7 znegcl N N
8 fladdz A N A + -N = A + -N
9 7 8 sylan2 A N A + -N = A + -N
10 reflcl A A
11 10 recnd A A
12 negsub A N A + -N = A N
13 11 2 12 syl2an A N A + -N = A N
14 6 9 13 3eqtrd A N A N = A N