Metamath Proof Explorer

Theorem zofldiv2

Description: The floor of an odd integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion zofldiv2 ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ( 𝑁 − 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
3 2 eqcomd ⊢ ( 𝑁 ∈ ℂ → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
4 1 3 syl ⊢ ( 𝑁 ∈ ℤ → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
5 4 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / 2 ) = ( ( ( 𝑁 − 1 ) + 1 ) / 2 ) )
6 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
7 6 zcnd ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℂ )
8 1cnd ⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℂ )
9 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
10 9 a1i ⊢ ( 𝑁 ∈ ℤ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
11 divdir ⊢ ( ( ( 𝑁 − 1 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝑁 − 1 ) + 1 ) / 2 ) = ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) )
12 7 8 10 11 syl3anc ⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 − 1 ) + 1 ) / 2 ) = ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) )
13 5 12 eqtrd ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / 2 ) = ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) )
14 13 fveq2d ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ⌊ ‘ ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) ) )
15 14 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ⌊ ‘ ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) ) )
16 halfge0 ⊢ 0 ≤ ( 1 / 2 )
17 halflt1 ⊢ ( 1 / 2 ) < 1
18 16 17 pm3.2i ⊢ ( 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 )
19 zob ⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
20 19 biimpa ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ )
21 halfre ⊢ ( 1 / 2 ) ∈ ℝ
22 flbi2 ⊢ ( ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ⌊ ‘ ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑁 − 1 ) / 2 ) ↔ ( 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
23 20 21 22 sylancl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( ⌊ ‘ ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑁 − 1 ) / 2 ) ↔ ( 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
24 18 23 mpbiri ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ⌊ ‘ ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑁 − 1 ) / 2 ) )
25 15 24 eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ( 𝑁 − 1 ) / 2 ) )