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 ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴 + 𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) )

Proof

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