Theorem fldiv4lem1div2

Description: The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021)

	Ref	Expression
Assertion	fldiv4lem1div2	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn1uz2	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
2		1lt4	⊢ 1 < 4
3		1nn0	⊢ 1 ∈ ℕ0
4		4nn	⊢ 4 ∈ ℕ
5		divfl0	⊢ ( ( 1 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( 1 < 4 ↔ ( ⌊ ‘ ( 1 / 4 ) ) = 0 ) )
6	3 4 5	mp2an	⊢ ( 1 < 4 ↔ ( ⌊ ‘ ( 1 / 4 ) ) = 0 )
7	2 6	mpbi	⊢ ( ⌊ ‘ ( 1 / 4 ) ) = 0
8		1re	⊢ 1 ∈ ℝ
9		4re	⊢ 4 ∈ ℝ
10		4ne0	⊢ 4 ≠ 0
11		redivcl	⊢ ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ ∧ 4 ≠ 0 ) → ( 1 / 4 ) ∈ ℝ )
12	11	flcld	⊢ ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ ∧ 4 ≠ 0 ) → ( ⌊ ‘ ( 1 / 4 ) ) ∈ ℤ )
13	12	zred	⊢ ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ ∧ 4 ≠ 0 ) → ( ⌊ ‘ ( 1 / 4 ) ) ∈ ℝ )
14	8 9 10 13	mp3an	⊢ ( ⌊ ‘ ( 1 / 4 ) ) ∈ ℝ
15	14	eqlei	⊢ ( ( ⌊ ‘ ( 1 / 4 ) ) = 0 → ( ⌊ ‘ ( 1 / 4 ) ) ≤ 0 )
16	7 15	mp1i	⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 1 / 4 ) ) ≤ 0 )
17		fvoveq1	⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 𝑁 / 4 ) ) = ( ⌊ ‘ ( 1 / 4 ) ) )
18		oveq1	⊢ ( 𝑁 = 1 → ( 𝑁 − 1 ) = ( 1 − 1 ) )
19		1m1e0	⊢ ( 1 − 1 ) = 0
20	18 19	eqtrdi	⊢ ( 𝑁 = 1 → ( 𝑁 − 1 ) = 0 )
21	20	oveq1d	⊢ ( 𝑁 = 1 → ( ( 𝑁 − 1 ) / 2 ) = ( 0 / 2 ) )
22		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
23		div0	⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 0 / 2 ) = 0 )
24	22 23	ax-mp	⊢ ( 0 / 2 ) = 0
25	21 24	eqtrdi	⊢ ( 𝑁 = 1 → ( ( 𝑁 − 1 ) / 2 ) = 0 )
26	16 17 25	3brtr4d	⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
27		fldiv4lem1div2uz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
28	26 27	jaoi	⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
29	1 28	sylbi	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )