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 ∈ ℤ ∧ 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