Theorem ceildivmod

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

	Ref	Expression
Assertion	ceildivmod	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌈\frac{A}{B}⌉=\frac{A+\left(\left(B-A\right)\mathrm{mod}B\right)}{B}$$

Proof

Step	Hyp	Ref	Expression
1		rerpdivcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in ℝ$$
2		ceilval	$$⊢\frac{A}{B}\in ℝ\to ⌈\frac{A}{B}⌉=-⌊-\frac{A}{B}⌋$$
3	1 2	syl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌈\frac{A}{B}⌉=-⌊-\frac{A}{B}⌋$$
4		recn	$$⊢A\in ℝ\to A\in ℂ$$
5	4	adantr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\in ℂ$$
6		rpcn	$$⊢B\in {ℝ}^{+}\to B\in ℂ$$
7	6	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in ℂ$$
8		rpne0	$$⊢B\in {ℝ}^{+}\to B\ne 0$$
9	8	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\ne 0$$
10	5 7 9	divnegd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -\frac{A}{B}=\frac{-A}{B}$$
11	10	fveq2d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊-\frac{A}{B}⌋=⌊\frac{-A}{B}⌋$$
12		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
13		fldivmod	$$⊢\left(-A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{-A}{B}⌋=\frac{-A-\left(\left(-A\right)\mathrm{mod}B\right)}{B}$$
14	12 13	sylan	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{-A}{B}⌋=\frac{-A-\left(\left(-A\right)\mathrm{mod}B\right)}{B}$$
15	11 14	eqtrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊-\frac{A}{B}⌋=\frac{-A-\left(\left(-A\right)\mathrm{mod}B\right)}{B}$$
16	15	negeqd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -⌊-\frac{A}{B}⌋=-\frac{-A-\left(\left(-A\right)\mathrm{mod}B\right)}{B}$$
17	12	recnd	$$⊢A\in ℝ\to -A\in ℂ$$
18	17	adantr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -A\in ℂ$$
19		modcl	$$⊢\left(-A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(-A\right)\mathrm{mod}B\in ℝ$$
20	12 19	sylan	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(-A\right)\mathrm{mod}B\in ℝ$$
21	20	recnd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(-A\right)\mathrm{mod}B\in ℂ$$
22	18 21	subcld	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -A-\left(\left(-A\right)\mathrm{mod}B\right)\in ℂ$$
23	22 7 9	divnegd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -\frac{-A-\left(\left(-A\right)\mathrm{mod}B\right)}{B}=\frac{-\left(-A-\left(\left(-A\right)\mathrm{mod}B\right)\right)}{B}$$
24	16 23	eqtrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -⌊-\frac{A}{B}⌋=\frac{-\left(-A-\left(\left(-A\right)\mathrm{mod}B\right)\right)}{B}$$
25	18 21	negsubdid	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -\left(-A-\left(\left(-A\right)\mathrm{mod}B\right)\right)=-\left(-A\right)+\left(\left(-A\right)\mathrm{mod}B\right)$$
26	4	negnegd	$$⊢A\in ℝ\to -\left(-A\right)=A$$
27	26	adantr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -\left(-A\right)=A$$
28	27	oveq1d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -\left(-A\right)+\left(\left(-A\right)\mathrm{mod}B\right)=A+\left(\left(-A\right)\mathrm{mod}B\right)$$
29		negmod	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(-A\right)\mathrm{mod}B=\left(B-A\right)\mathrm{mod}B$$
30	29	oveq2d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A+\left(\left(-A\right)\mathrm{mod}B\right)=A+\left(\left(B-A\right)\mathrm{mod}B\right)$$
31	25 28 30	3eqtrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to -\left(-A-\left(\left(-A\right)\mathrm{mod}B\right)\right)=A+\left(\left(B-A\right)\mathrm{mod}B\right)$$
32	31	oveq1d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{-\left(-A-\left(\left(-A\right)\mathrm{mod}B\right)\right)}{B}=\frac{A+\left(\left(B-A\right)\mathrm{mod}B\right)}{B}$$
33	3 24 32	3eqtrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌈\frac{A}{B}⌉=\frac{A+\left(\left(B-A\right)\mathrm{mod}B\right)}{B}$$