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	⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) < ( 𝑁 / 4 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
2		4z	⊢ 4 ∈ ℤ
3		4ne0	⊢ 4 ≠ 0
4	2 3	pm3.2i	⊢ ( 4 ∈ ℤ ∧ 4 ≠ 0 )
5	4	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( 4 ∈ ℤ ∧ 4 ≠ 0 ) )
6		4dvdseven	⊢ ( 4 ∥ 𝑁 → 2 ∥ 𝑁 )
7	6	con3i	⊢ ( ¬ 2 ∥ 𝑁 → ¬ 4 ∥ 𝑁 )
8	7	adantl	⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ¬ 4 ∥ 𝑁 )
9		fldivndvdslt	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 4 ∈ ℤ ∧ 4 ≠ 0 ) ∧ ¬ 4 ∥ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) < ( 𝑁 / 4 ) )
10	1 5 8 9	syl3anc	⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) < ( 𝑁 / 4 ) )