Metamath Proof Explorer

Theorem flodddiv4lt

Description: The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021)

Ref Expression
Assertion flodddiv4lt 
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( |_ ` ( N / 4 ) ) < ( N / 4 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> N e. ZZ )
2 4z 
 |-  4 e. ZZ
3 4ne0 
 |-  4 =/= 0
4 2 3 pm3.2i 
 |-  ( 4 e. ZZ /\ 4 =/= 0 )
5 4 a1i 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( 4 e. ZZ /\ 4 =/= 0 ) )
6 4dvdseven 
 |-  ( 4 || N -> 2 || N )
7 6 con3i 
 |-  ( -. 2 || N -> -. 4 || N )
8 7 adantl 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> -. 4 || N )
9 fldivndvdslt 
 |-  ( ( N e. ZZ /\ ( 4 e. ZZ /\ 4 =/= 0 ) /\ -. 4 || N ) -> ( |_ ` ( N / 4 ) ) < ( N / 4 ) )
10 1 5 8 9 syl3anc 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( |_ ` ( N / 4 ) ) < ( N / 4 ) )