Metamath Proof Explorer


Theorem zefldiv2

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 N 2 N 2 = N 2

Proof

Step Hyp Ref Expression
1 flid N 2 N 2 = N 2
2 1 adantl N N 2 N 2 = N 2