Metamath Proof Explorer


Theorem zefldiv2ALTV

Description: The floor of an even number divided by 2 is equal to the even number divided by 2. (Contributed by AV, 7-Jun-2020) (Revised by AV, 18-Jun-2020)

Ref Expression
Assertion zefldiv2ALTV
|- ( N e. Even -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )

Proof

Step Hyp Ref Expression
1 evendiv2z
 |-  ( N e. Even -> ( N / 2 ) e. ZZ )
2 flid
 |-  ( ( N / 2 ) e. ZZ -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
3 1 2 syl
 |-  ( N e. Even -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )