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 ( 𝑁 ∈ Odd → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ( 𝑁 − 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 oddz ⊢ ( 𝑁 ∈ Odd → 𝑁 ∈ ℤ )
2 1 zcnd ⊢ ( 𝑁 ∈ Odd → 𝑁 ∈ ℂ )
3 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
4 3 eqcomd ⊢ ( 𝑁 ∈ ℂ → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
5 4 oveq1d ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 / 2 ) = ( ( ( 𝑁 − 1 ) + 1 ) / 2 ) )
6 peano2cnm ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 − 1 ) ∈ ℂ )
7 1cnd ⊢ ( 𝑁 ∈ ℂ → 1 ∈ ℂ )
8 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
9 8 a1i ⊢ ( 𝑁 ∈ ℂ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
10 divdir ⊢ ( ( ( 𝑁 − 1 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝑁 − 1 ) + 1 ) / 2 ) = ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) )
11 6 7 9 10 syl3anc ⊢ ( 𝑁 ∈ ℂ → ( ( ( 𝑁 − 1 ) + 1 ) / 2 ) = ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) )
12 5 11 eqtrd ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 / 2 ) = ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) )
13 2 12 syl ⊢ ( 𝑁 ∈ Odd → ( 𝑁 / 2 ) = ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) )
14 13 fveq2d ⊢ ( 𝑁 ∈ Odd → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ⌊ ‘ ( ( ( 𝑁 − 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 ⊢ ( 𝑁 ∈ Odd → ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ )
19 halfre ⊢ ( 1 / 2 ) ∈ ℝ
20 flbi2 ⊢ ( ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ⌊ ‘ ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑁 − 1 ) / 2 ) ↔ ( 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
21 18 19 20 sylancl ⊢ ( 𝑁 ∈ Odd → ( ( ⌊ ‘ ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑁 − 1 ) / 2 ) ↔ ( 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
22 17 21 mpbiri ⊢ ( 𝑁 ∈ Odd → ( ⌊ ‘ ( ( ( 𝑁 − 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑁 − 1 ) / 2 ) )
23 14 22 eqtrd ⊢ ( 𝑁 ∈ Odd → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ( 𝑁 − 1 ) / 2 ) )