Metamath Proof Explorer

Theorem ceildivmod

Description: Expressing the ceiling of a division by the modulo operator. (Contributed by AV, 7-Sep-2025)

Ref Expression
Assertion ceildivmod 
|- ( ( A e. RR /\ B e. RR+ ) -> ( |^ ` ( A / B ) ) = ( ( A + ( ( B - A ) mod B ) ) / B ) )

Proof

Step Hyp Ref Expression
1 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
2 ceilval 
 |-  ( ( A / B ) e. RR -> ( |^ ` ( A / B ) ) = -u ( |_ ` -u ( A / B ) ) )
3 1 2 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |^ ` ( A / B ) ) = -u ( |_ ` -u ( A / B ) ) )
4 recn 
 |-  ( A e. RR -> A e. CC )
5 4 adantr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> A e. CC )
6 rpcn 
 |-  ( B e. RR+ -> B e. CC )
7 6 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
8 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
9 8 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B =/= 0 )
10 5 7 9 divnegd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u ( A / B ) = ( -u A / B ) )
11 10 fveq2d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` -u ( A / B ) ) = ( |_ ` ( -u A / B ) ) )
12 renegcl 
 |-  ( A e. RR -> -u A e. RR )
13 fldivmod 
 |-  ( ( -u A e. RR /\ B e. RR+ ) -> ( |_ ` ( -u A / B ) ) = ( ( -u A - ( -u A mod B ) ) / B ) )
14 12 13 sylan 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( -u A / B ) ) = ( ( -u A - ( -u A mod B ) ) / B ) )
15 11 14 eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` -u ( A / B ) ) = ( ( -u A - ( -u A mod B ) ) / B ) )
16 15 negeqd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u ( |_ ` -u ( A / B ) ) = -u ( ( -u A - ( -u A mod B ) ) / B ) )
17 12 recnd 
 |-  ( A e. RR -> -u A e. CC )
18 17 adantr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u A e. CC )
19 modcl 
 |-  ( ( -u A e. RR /\ B e. RR+ ) -> ( -u A mod B ) e. RR )
20 12 19 sylan 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( -u A mod B ) e. RR )
21 20 recnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( -u A mod B ) e. CC )
22 18 21 subcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( -u A - ( -u A mod B ) ) e. CC )
23 22 7 9 divnegd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u ( ( -u A - ( -u A mod B ) ) / B ) = ( -u ( -u A - ( -u A mod B ) ) / B ) )
24 16 23 eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u ( |_ ` -u ( A / B ) ) = ( -u ( -u A - ( -u A mod B ) ) / B ) )
25 18 21 negsubdid 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u ( -u A - ( -u A mod B ) ) = ( -u -u A + ( -u A mod B ) ) )
26 4 negnegd 
 |-  ( A e. RR -> -u -u A = A )
27 26 adantr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u -u A = A )
28 27 oveq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( -u -u A + ( -u A mod B ) ) = ( A + ( -u A mod B ) ) )
29 negmod 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( -u A mod B ) = ( ( B - A ) mod B ) )
30 29 oveq2d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A + ( -u A mod B ) ) = ( A + ( ( B - A ) mod B ) ) )
31 25 28 30 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u ( -u A - ( -u A mod B ) ) = ( A + ( ( B - A ) mod B ) ) )
32 31 oveq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( -u ( -u A - ( -u A mod B ) ) / B ) = ( ( A + ( ( B - A ) mod B ) ) / B ) )
33 3 24 32 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |^ ` ( A / B ) ) = ( ( A + ( ( B - A ) mod B ) ) / B ) )