Metamath Proof Explorer

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 e. RR
2 2rp 
 |-  2 e. RR+
3 ceildivmod 
 |-  ( ( 5 e. RR /\ 2 e. RR+ ) -> ( |^ ` ( 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 x. 2 ) = 6
7 2t2e4 
 |-  ( 2 x. 2 ) = 4
8 7 oveq1i 
 |-  ( ( 2 x. 2 ) + ( 2 - 5 ) ) = ( 4 + ( 2 - 5 ) )
9 4cn 
 |-  4 e. CC
10 2cn 
 |-  2 e. CC
11 5cn 
 |-  5 e. CC
12 9 10 11 addsubassi 
 |-  ( ( 4 + 2 ) - 5 ) = ( 4 + ( 2 - 5 ) )
13 ax-1cn 
 |-  1 e. CC
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 x. 2 ) + ( 2 - 5 ) ) = 1
18 17 oveq1i 
 |-  ( ( ( 2 x. 2 ) + ( 2 - 5 ) ) mod 2 ) = ( 1 mod 2 )
19 2re 
 |-  2 e. RR
20 19 1 resubcli 
 |-  ( 2 - 5 ) e. RR
21 2z 
 |-  2 e. ZZ
22 muladdmod 
 |-  ( ( ( 2 - 5 ) e. RR /\ 2 e. RR+ /\ 2 e. ZZ ) -> ( ( ( 2 x. 2 ) + ( 2 - 5 ) ) mod 2 ) = ( ( 2 - 5 ) mod 2 ) )
23 20 2 21 22 mp3an 
 |-  ( ( ( 2 x. 2 ) + ( 2 - 5 ) ) mod 2 ) = ( ( 2 - 5 ) mod 2 )
24 1lt2 
 |-  1 < 2
25 1mod 
 |-  ( ( 2 e. RR /\ 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 x. 2 )
30 29 oveq1i 
 |-  ( ( 5 + ( ( 2 - 5 ) mod 2 ) ) / 2 ) = ( ( 3 x. 2 ) / 2 )
31 3cn 
 |-  3 e. CC
32 2ne0 
 |-  2 =/= 0
33 31 10 32 divcan4i 
 |-  ( ( 3 x. 2 ) / 2 ) = 3
34 30 33 eqtri 
 |-  ( ( 5 + ( ( 2 - 5 ) mod 2 ) ) / 2 ) = 3
35 4 34 eqtri 
 |-  ( |^ ` ( 5 / 2 ) ) = 3