Metamath Proof Explorer

Theorem fladdz

Description: An integer can be moved in and out of the floor of a sum. (Contributed by NM, 27-Apr-2005) (Proof shortened by Fan Zheng, 16-Jun-2016)

Ref Expression
Assertion fladdz ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + N = A + N

Proof

Step Hyp Ref Expression
1 reflcl ⊢ A ∈ ℝ → A ∈ ℝ
2 1 adantr ⊢ A ∈ ℝ ∧ N ∈ ℤ → A ∈ ℝ
3 simpl ⊢ A ∈ ℝ ∧ N ∈ ℤ → A ∈ ℝ
4 simpr ⊢ A ∈ ℝ ∧ N ∈ ℤ → N ∈ ℤ
5 4 zred ⊢ A ∈ ℝ ∧ N ∈ ℤ → N ∈ ℝ
6 flle ⊢ A ∈ ℝ → A ≤ A
7 6 adantr ⊢ A ∈ ℝ ∧ N ∈ ℤ → A ≤ A
8 2 3 5 7 leadd1dd ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + N ≤ A + N
9 1red ⊢ A ∈ ℝ ∧ N ∈ ℤ → 1 ∈ ℝ
10 2 9 readdcld ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + 1 ∈ ℝ
11 flltp1 ⊢ A ∈ ℝ → A < A + 1
12 11 adantr ⊢ A ∈ ℝ ∧ N ∈ ℤ → A < A + 1
13 3 10 5 12 ltadd1dd ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + N < A + 1 + N
14 2 recnd ⊢ A ∈ ℝ ∧ N ∈ ℤ → A ∈ ℂ
15 1cnd ⊢ A ∈ ℝ ∧ N ∈ ℤ → 1 ∈ ℂ
16 5 recnd ⊢ A ∈ ℝ ∧ N ∈ ℤ → N ∈ ℂ
17 14 15 16 add32d ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + 1 + N = A + N + 1
18 13 17 breqtrd ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + N < A + N + 1
19 3 5 readdcld ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + N ∈ ℝ
20 3 flcld ⊢ A ∈ ℝ ∧ N ∈ ℤ → A ∈ ℤ
21 20 4 zaddcld ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + N ∈ ℤ
22 flbi ⊢ A + N ∈ ℝ ∧ A + N ∈ ℤ → A + N = A + N ↔ A + N ≤ A + N ∧ A + N < A + N + 1
23 19 21 22 syl2anc ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + N = A + N ↔ A + N ≤ A + N ∧ A + N < A + N + 1
24 8 18 23 mpbir2and ⊢ A ∈ ℝ ∧ N ∈ ℤ → A + N = A + N