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

Proof

Step Hyp Ref Expression
1 fladdz A N A + N = A + N
2 recn A A
3 zcn N N
4 addcom A N A + N = N + A
5 2 3 4 syl2an A N A + N = N + A
6 5 fveq2d A N A + N = N + A
7 reflcl A A
8 7 recnd A A
9 addcom A N A + N = N + A
10 8 3 9 syl2an A N A + N = N + A
11 1 6 10 3eqtr3d A N N + A = N + A
12 11 ancoms N A N + A = N + A