Metamath Proof Explorer

Theorem oddm1div2z

Description: The result of dividing an odd number decreased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020)

Ref Expression
Assertion oddm1div2z 
|- ( Z e. Odd -> ( ( Z - 1 ) / 2 ) e. ZZ )

Proof

Step Hyp Ref Expression
1 oddp1div2z 
 |-  ( Z e. Odd -> ( ( Z + 1 ) / 2 ) e. ZZ )
2 oddz 
 |-  ( Z e. Odd -> Z e. ZZ )
3 zob 
 |-  ( Z e. ZZ -> ( ( ( Z + 1 ) / 2 ) e. ZZ <-> ( ( Z - 1 ) / 2 ) e. ZZ ) )
4 2 3 syl 
 |-  ( Z e. Odd -> ( ( ( Z + 1 ) / 2 ) e. ZZ <-> ( ( Z - 1 ) / 2 ) e. ZZ ) )
5 1 4 mpbid 
 |-  ( Z e. Odd -> ( ( Z - 1 ) / 2 ) e. ZZ )