Metamath Proof Explorer


Theorem flsubz

Description: An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020)

Ref Expression
Assertion flsubz ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) − 𝑁 ) )

Proof

Step Hyp Ref Expression
1 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
3 negsub ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐴 + - 𝑁 ) = ( 𝐴𝑁 ) )
4 1 2 3 syl2an ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + - 𝑁 ) = ( 𝐴𝑁 ) )
5 4 eqcomd ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( 𝐴𝑁 ) = ( 𝐴 + - 𝑁 ) )
6 5 fveq2d ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴𝑁 ) ) = ( ⌊ ‘ ( 𝐴 + - 𝑁 ) ) )
7 znegcl ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
8 fladdz ( ( 𝐴 ∈ ℝ ∧ - 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴 + - 𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) + - 𝑁 ) )
9 7 8 sylan2 ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴 + - 𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) + - 𝑁 ) )
10 reflcl ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
11 10 recnd ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
12 negsub ( ( ( ⌊ ‘ 𝐴 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ⌊ ‘ 𝐴 ) + - 𝑁 ) = ( ( ⌊ ‘ 𝐴 ) − 𝑁 ) )
13 11 2 12 syl2an ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) + - 𝑁 ) = ( ( ⌊ ‘ 𝐴 ) − 𝑁 ) )
14 6 9 13 3eqtrd ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) − 𝑁 ) )