Theorem ceil5half3

Description: The ceiling of half of 5 is 3. (Contributed by AV, 7-Sep-2025)

	Ref	Expression
Assertion	ceil5half3	$$⊢⌈\frac{5}{2}⌉=3$$

Proof

Step	Hyp	Ref	Expression
1		5re	$$⊢5\in ℝ$$
2		2rp	$$⊢2\in {ℝ}^{+}$$
3		ceildivmod	$$⊢\left(5\in ℝ\wedge 2\in {ℝ}^{+}\right)\to ⌈\frac{5}{2}⌉=\frac{5+\left(\left(2-5\right)\mathrm{mod}2\right)}{2}$$
4	1 2 3	mp2an	$$⊢⌈\frac{5}{2}⌉=\frac{5+\left(\left(2-5\right)\mathrm{mod}2\right)}{2}$$
5		df-6	$$⊢6=5+1$$
6		3t2e6	$$⊢3\cdot 2=6$$
7		2t2e4	$$⊢2\cdot 2=4$$
8	7	oveq1i	$$⊢2\cdot 2+2-5=4+2-5$$
9		4cn	$$⊢4\in ℂ$$
10		2cn	$$⊢2\in ℂ$$
11		5cn	$$⊢5\in ℂ$$
12	9 10 11	addsubassi	$$⊢4+2-5=4+2-5$$
13		ax-1cn	$$⊢1\in ℂ$$
14		4p2e6	$$⊢4+2=6$$
15	14 5	eqtri	$$⊢4+2=5+1$$
16	11 13 15	mvrladdi	$$⊢4+2-5=1$$
17	8 12 16	3eqtr2i	$$⊢2\cdot 2+2-5=1$$
18	17	oveq1i	$$⊢\left(2\cdot 2+2-5\right)\mathrm{mod}2=1\mathrm{mod}2$$
19		2re	$$⊢2\in ℝ$$
20	19 1	resubcli	$$⊢2-5\in ℝ$$
21		2z	$$⊢2\in \mathbb{Z}$$
22		muladdmod	$$⊢\left(2-5\in ℝ\wedge 2\in {ℝ}^{+}\wedge 2\in \mathbb{Z}\right)\to \left(2\cdot 2+2-5\right)\mathrm{mod}2=\left(2-5\right)\mathrm{mod}2$$
23	20 2 21 22	mp3an	$$⊢\left(2\cdot 2+2-5\right)\mathrm{mod}2=\left(2-5\right)\mathrm{mod}2$$
24		1lt2	$$⊢1<2$$
25		1mod	$$⊢\left(2\in ℝ\wedge 1<2\right)\to 1\mathrm{mod}2=1$$
26	19 24 25	mp2an	$$⊢1\mathrm{mod}2=1$$
27	18 23 26	3eqtr3i	$$⊢\left(2-5\right)\mathrm{mod}2=1$$
28	27	oveq2i	$$⊢5+\left(\left(2-5\right)\mathrm{mod}2\right)=5+1$$
29	5 6 28	3eqtr4ri	$$⊢5+\left(\left(2-5\right)\mathrm{mod}2\right)=3\cdot 2$$
30	29	oveq1i	$$⊢\frac{5+\left(\left(2-5\right)\mathrm{mod}2\right)}{2}=\frac{3\cdot 2}{2}$$
31		3cn	$$⊢3\in ℂ$$
32		2ne0	$$⊢2\ne 0$$
33	31 10 32	divcan4i	$$⊢\frac{3\cdot 2}{2}=3$$
34	30 33	eqtri	$$⊢\frac{5+\left(\left(2-5\right)\mathrm{mod}2\right)}{2}=3$$
35	4 34	eqtri	$$⊢⌈\frac{5}{2}⌉=3$$