Theorem flnn0ohalf

Description: The floor of the half of an odd positive integer is equal to the floor of the half of the integer decreased by 1. (Contributed by AV, 5-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		nn0ofldiv2	|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )
2		nn0o	|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )
3	2	nn0zd	|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. ZZ )
4		flid	|- ( ( ( N - 1 ) / 2 ) e. ZZ -> ( |_ ` ( ( N - 1 ) / 2 ) ) = ( ( N - 1 ) / 2 ) )
5	3 4	syl	|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( ( N - 1 ) / 2 ) ) = ( ( N - 1 ) / 2 ) )
6	1 5	eqtr4d	|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( N / 2 ) ) = ( |_ ` ( ( N - 1 ) / 2 ) ) )