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	⊢ ( 𝑁 ∈ Even → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		evendiv2z	⊢ ( 𝑁 ∈ Even → ( 𝑁 / 2 ) ∈ ℤ )
2		flid	⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
3	1 2	syl	⊢ ( 𝑁 ∈ Even → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )