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 \in ℤ \land \neg 2 ∥ N) \to ⌊\frac{N}{4}⌋ < \frac{N}{4}$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to N \in ℤ$
2		4z	$⊢ 4 \in ℤ$
3		4ne0	$⊢ 4 \neq 0$
4	2 3	pm3.2i	$⊢ (4 \in ℤ \land 4 \neq 0)$
5	4	a1i	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to (4 \in ℤ \land 4 \neq 0)$
6		4dvdseven	$⊢ 4 ∥ N \to 2 ∥ N$
7	6	con3i	$⊢ \neg 2 ∥ N \to \neg 4 ∥ N$
8	7	adantl	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to \neg 4 ∥ N$
9		fldivndvdslt	$⊢ (N \in ℤ \land (4 \in ℤ \land 4 \neq 0) \land \neg 4 ∥ N) \to ⌊\frac{N}{4}⌋ < \frac{N}{4}$
10	1 5 8 9	syl3anc	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to ⌊\frac{N}{4}⌋ < \frac{N}{4}$

Metamath Proof Explorer