Metamath Proof Explorer

Theorem zofldiv2ALTV

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

Ref Expression
Assertion zofldiv2ALTV ⊢ N ∈ Odd → N 2 = N − 1 2

Proof

Step Hyp Ref Expression
1 oddz ⊢ N ∈ Odd → N ∈ ℤ
2 1 zcnd ⊢ N ∈ Odd → N ∈ ℂ
3 npcan1 ⊢ N ∈ ℂ → N - 1 + 1 = N
4 3 eqcomd ⊢ N ∈ ℂ → N = N - 1 + 1
5 4 oveq1d ⊢ N ∈ ℂ → N 2 = N - 1 + 1 2
6 peano2cnm ⊢ N ∈ ℂ → N − 1 ∈ ℂ
7 1cnd ⊢ N ∈ ℂ → 1 ∈ ℂ
8 2cnne0 ⊢ 2 ∈ ℂ ∧ 2 ≠ 0
9 8 a1i ⊢ N ∈ ℂ → 2 ∈ ℂ ∧ 2 ≠ 0
10 divdir ⊢ N − 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → N - 1 + 1 2 = N − 1 2 + 1 2
11 6 7 9 10 syl3anc ⊢ N ∈ ℂ → N - 1 + 1 2 = N − 1 2 + 1 2
12 5 11 eqtrd ⊢ N ∈ ℂ → N 2 = N − 1 2 + 1 2
13 2 12 syl ⊢ N ∈ Odd → N 2 = N − 1 2 + 1 2
14 13 fveq2d ⊢ N ∈ Odd → N 2 = N − 1 2 + 1 2
15 halfge0 ⊢ 0 ≤ 1 2
16 halflt1 ⊢ 1 2 < 1
17 15 16 pm3.2i ⊢ 0 ≤ 1 2 ∧ 1 2 < 1
18 oddm1div2z ⊢ N ∈ Odd → N − 1 2 ∈ ℤ
19 halfre ⊢ 1 2 ∈ ℝ
20 flbi2 ⊢ N − 1 2 ∈ ℤ ∧ 1 2 ∈ ℝ → N − 1 2 + 1 2 = N − 1 2 ↔ 0 ≤ 1 2 ∧ 1 2 < 1
21 18 19 20 sylancl ⊢ N ∈ Odd → N − 1 2 + 1 2 = N − 1 2 ↔ 0 ≤ 1 2 ∧ 1 2 < 1
22 17 21 mpbiri ⊢ N ∈ Odd → N − 1 2 + 1 2 = N − 1 2
23 14 22 eqtrd ⊢ N ∈ Odd → N 2 = N − 1 2