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 ⊢ N ∈ ℤ ∧ N + 1 2 ∈ ℤ → N 2 = N − 1 2

Proof

Step Hyp Ref Expression
1 zcn ⊢ N ∈ ℤ → N ∈ ℂ
2 npcan1 ⊢ N ∈ ℂ → N - 1 + 1 = N
3 2 eqcomd ⊢ N ∈ ℂ → N = N - 1 + 1
4 1 3 syl ⊢ N ∈ ℤ → N = N - 1 + 1
5 4 oveq1d ⊢ N ∈ ℤ → N 2 = N - 1 + 1 2
6 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
7 6 zcnd ⊢ N ∈ ℤ → N − 1 ∈ ℂ
8 1cnd ⊢ N ∈ ℤ → 1 ∈ ℂ
9 2cnne0 ⊢ 2 ∈ ℂ ∧ 2 ≠ 0
10 9 a1i ⊢ N ∈ ℤ → 2 ∈ ℂ ∧ 2 ≠ 0
11 divdir ⊢ N − 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → N - 1 + 1 2 = N − 1 2 + 1 2
12 7 8 10 11 syl3anc ⊢ N ∈ ℤ → N - 1 + 1 2 = N − 1 2 + 1 2
13 5 12 eqtrd ⊢ N ∈ ℤ → N 2 = N − 1 2 + 1 2
14 13 fveq2d ⊢ N ∈ ℤ → N 2 = N − 1 2 + 1 2
15 14 adantr ⊢ N ∈ ℤ ∧ N + 1 2 ∈ ℤ → N 2 = N − 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 ⊢ N ∈ ℤ → N + 1 2 ∈ ℤ ↔ N − 1 2 ∈ ℤ
20 19 biimpa ⊢ N ∈ ℤ ∧ N + 1 2 ∈ ℤ → N − 1 2 ∈ ℤ
21 halfre ⊢ 1 2 ∈ ℝ
22 flbi2 ⊢ N − 1 2 ∈ ℤ ∧ 1 2 ∈ ℝ → N − 1 2 + 1 2 = N − 1 2 ↔ 0 ≤ 1 2 ∧ 1 2 < 1
23 20 21 22 sylancl ⊢ N ∈ ℤ ∧ N + 1 2 ∈ ℤ → N − 1 2 + 1 2 = N − 1 2 ↔ 0 ≤ 1 2 ∧ 1 2 < 1
24 18 23 mpbiri ⊢ N ∈ ℤ ∧ N + 1 2 ∈ ℤ → N − 1 2 + 1 2 = N − 1 2
25 15 24 eqtrd ⊢ N ∈ ℤ ∧ N + 1 2 ∈ ℤ → N 2 = N − 1 2