Metamath Proof Explorer
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 |
⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
flid |
⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) ) |
| 2 |
1
|
adantl |
⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) ) |