Theorem nn0ofldiv2

Description: The floor of an odd nonnegative integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020) (Proof shortened by AV, 7-Jun-2020)

	Ref	Expression
Assertion	nn0ofldiv2	|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	|- ( N e. NN0 -> N e. ZZ )
2		nn0z	|- ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( N + 1 ) / 2 ) e. ZZ )
3		zofldiv2	|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )
4	1 2 3	syl2an	|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )