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