Theorem ceil5half3

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

	Ref	Expression
Assertion	ceil5half3	⊢ ( ⌈ ‘ ( 5 / 2 ) ) = 3

Proof

Step	Hyp	Ref	Expression
1		5re	⊢ 5 ∈ ℝ
2		2rp	⊢ 2 ∈ ℝ+
3		ceildivmod	⊢ ( ( 5 ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ⌈ ‘ ( 5 / 2 ) ) = ( ( 5 + ( ( 2 − 5 ) mod 2 ) ) / 2 ) )
4	1 2 3	mp2an	⊢ ( ⌈ ‘ ( 5 / 2 ) ) = ( ( 5 + ( ( 2 − 5 ) mod 2 ) ) / 2 )
5		df-6	⊢ 6 = ( 5 + 1 )
6		3t2e6	⊢ ( 3 · 2 ) = 6
7		2t2e4	⊢ ( 2 · 2 ) = 4
8	7	oveq1i	⊢ ( ( 2 · 2 ) + ( 2 − 5 ) ) = ( 4 + ( 2 − 5 ) )
9		4cn	⊢ 4 ∈ ℂ
10		2cn	⊢ 2 ∈ ℂ
11		5cn	⊢ 5 ∈ ℂ
12	9 10 11	addsubassi	⊢ ( ( 4 + 2 ) − 5 ) = ( 4 + ( 2 − 5 ) )
13		ax-1cn	⊢ 1 ∈ ℂ
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 · 2 ) + ( 2 − 5 ) ) = 1
18	17	oveq1i	⊢ ( ( ( 2 · 2 ) + ( 2 − 5 ) ) mod 2 ) = ( 1 mod 2 )
19		2re	⊢ 2 ∈ ℝ
20	19 1	resubcli	⊢ ( 2 − 5 ) ∈ ℝ
21		2z	⊢ 2 ∈ ℤ
22		muladdmod	⊢ ( ( ( 2 − 5 ) ∈ ℝ ∧ 2 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( ( 2 · 2 ) + ( 2 − 5 ) ) mod 2 ) = ( ( 2 − 5 ) mod 2 ) )
23	20 2 21 22	mp3an	⊢ ( ( ( 2 · 2 ) + ( 2 − 5 ) ) mod 2 ) = ( ( 2 − 5 ) mod 2 )
24		1lt2	⊢ 1 < 2
25		1mod	⊢ ( ( 2 ∈ ℝ ∧ 1 < 2 ) → ( 1 mod 2 ) = 1 )
26	19 24 25	mp2an	⊢ ( 1 mod 2 ) = 1
27	18 23 26	3eqtr3i	⊢ ( ( 2 − 5 ) mod 2 ) = 1
28	27	oveq2i	⊢ ( 5 + ( ( 2 − 5 ) mod 2 ) ) = ( 5 + 1 )
29	5 6 28	3eqtr4ri	⊢ ( 5 + ( ( 2 − 5 ) mod 2 ) ) = ( 3 · 2 )
30	29	oveq1i	⊢ ( ( 5 + ( ( 2 − 5 ) mod 2 ) ) / 2 ) = ( ( 3 · 2 ) / 2 )
31		3cn	⊢ 3 ∈ ℂ
32		2ne0	⊢ 2 ≠ 0
33	31 10 32	divcan4i	⊢ ( ( 3 · 2 ) / 2 ) = 3
34	30 33	eqtri	⊢ ( ( 5 + ( ( 2 − 5 ) mod 2 ) ) / 2 ) = 3
35	4 34	eqtri	⊢ ( ⌈ ‘ ( 5 / 2 ) ) = 3