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+12∈ℤ→N2=N−12

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∈ℤ→N2=N-1+12
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+12=N−12+12
12 7 8 10 11 syl3anc ⊢N∈ℤ→N-1+12=N−12+12
13 5 12 eqtrd ⊢N∈ℤ→N2=N−12+12
14 13 fveq2d ⊢N∈ℤ→N2=N−12+12
15 14 adantr ⊢N∈ℤ∧N+12∈ℤ→N2=N−12+12
16 halfge0 ⊢0≤12
17 halflt1 ⊢12<1
18 16 17 pm3.2i ⊢0≤12∧12<1
19 zob ⊢N∈ℤ→N+12∈ℤ↔N−12∈ℤ
20 19 biimpa ⊢N∈ℤ∧N+12∈ℤ→N−12∈ℤ
21 halfre ⊢12∈ℝ
22 flbi2 ⊢N−12∈ℤ∧12∈ℝ→N−12+12=N−12↔0≤12∧12<1
23 20 21 22 sylancl ⊢N∈ℤ∧N+12∈ℤ→N−12+12=N−12↔0≤12∧12<1
24 18 23 mpbiri ⊢N∈ℤ∧N+12∈ℤ→N−12+12=N−12
25 15 24 eqtrd ⊢N∈ℤ∧N+12∈ℤ→N2=N−12