Theorem fldiv4lem1div2uz2

Description: The floor of an integer greater than 1, divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 5-Jul-2021) (Proof shortened by AV, 9-Jul-2022)

	Ref	Expression
Assertion	fldiv4lem1div2uz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ )
2		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
3		id	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
4		4re	⊢ 4 ∈ ℝ
5	4	a1i	⊢ ( 𝑁 ∈ ℝ → 4 ∈ ℝ )
6		4ne0	⊢ 4 ≠ 0
7	6	a1i	⊢ ( 𝑁 ∈ ℝ → 4 ≠ 0 )
8	3 5 7	redivcld	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 / 4 ) ∈ ℝ )
9	2 8	syl	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / 4 ) ∈ ℝ )
10		flle	⊢ ( ( 𝑁 / 4 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) )
11	1 9 10	3syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) )
12		1red	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
13		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ )
14		rehalfcl	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 / 2 ) ∈ ℝ )
15	1 2 14	3syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 2 ) ∈ ℝ )
16		2rp	⊢ 2 ∈ ℝ+
17	16	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ+ )
18		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
19		divge1	⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 1 ≤ ( 𝑁 / 2 ) )
20	17 13 18 19	syl3anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ ( 𝑁 / 2 ) )
21		eluzelcn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℂ )
22		subhalfhalf	⊢ ( 𝑁 ∈ ℂ → ( 𝑁 − ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
23	21 22	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
24	20 23	breqtrrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ ( 𝑁 − ( 𝑁 / 2 ) ) )
25	12 13 15 24	lesubd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) )
26		2t2e4	⊢ ( 2 · 2 ) = 4
27	26	eqcomi	⊢ 4 = ( 2 · 2 )
28	27	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 4 = ( 2 · 2 ) )
29	28	oveq2d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 4 ) = ( 𝑁 / ( 2 · 2 ) ) )
30		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
31	30	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
32		divdiv1	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑁 / 2 ) / 2 ) = ( 𝑁 / ( 2 · 2 ) ) )
33	21 31 31 32	syl3anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 / 2 ) / 2 ) = ( 𝑁 / ( 2 · 2 ) ) )
34	29 33	eqtr4d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 4 ) = ( ( 𝑁 / 2 ) / 2 ) )
35	34	breq1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ↔ ( ( 𝑁 / 2 ) / 2 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
36		peano2rem	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
37	13 36	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℝ )
38	15 37 17	lediv1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) ↔ ( ( 𝑁 / 2 ) / 2 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
39	35 38	bitr4d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ↔ ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) ) )
40	25 39	mpbird	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
41	8	flcld	⊢ ( 𝑁 ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℤ )
42	41	zred	⊢ ( 𝑁 ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ )
43	36	rehalfcld	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ )
44	42 8 43	3jca	⊢ ( 𝑁 ∈ ℝ → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) )
45	1 2 44	3syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) )
46		letr	⊢ ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) → ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) ∧ ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
47	45 46	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) ∧ ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
48	11 40 47	mp2and	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )