Theorem zofldiv2ALTV

Description: The floor of an odd number 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 ) )