Description: The floor of an even integer divided by 2 is equal to the integer divided by 2. (Contributed by AV, 7-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | zefldiv2 | |- ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flid | |- ( ( N / 2 ) e. ZZ -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) ) |
|
2 | 1 | adantl | |- ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) ) |