Theorem ceildivmod

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

	Ref	Expression
Assertion	ceildivmod	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌈ ‘ ( 𝐴 / 𝐵 ) ) = ( ( 𝐴 + ( ( 𝐵 − 𝐴 ) mod 𝐵 ) ) / 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
2		ceilval	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌈ ‘ ( 𝐴 / 𝐵 ) ) = - ( ⌊ ‘ - ( 𝐴 / 𝐵 ) ) )
3	1 2	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌈ ‘ ( 𝐴 / 𝐵 ) ) = - ( ⌊ ‘ - ( 𝐴 / 𝐵 ) ) )
4		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
6		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
7	6	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
8		rpne0	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
9	8	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ≠ 0 )
10	5 7 9	divnegd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - ( 𝐴 / 𝐵 ) = ( - 𝐴 / 𝐵 ) )
11	10	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ - ( 𝐴 / 𝐵 ) ) = ( ⌊ ‘ ( - 𝐴 / 𝐵 ) ) )
12		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
13		fldivmod	⊢ ( ( - 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( - 𝐴 / 𝐵 ) ) = ( ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) / 𝐵 ) )
14	12 13	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( - 𝐴 / 𝐵 ) ) = ( ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) / 𝐵 ) )
15	11 14	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ - ( 𝐴 / 𝐵 ) ) = ( ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) / 𝐵 ) )
16	15	negeqd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - ( ⌊ ‘ - ( 𝐴 / 𝐵 ) ) = - ( ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) / 𝐵 ) )
17	12	recnd	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℂ )
18	17	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - 𝐴 ∈ ℂ )
19		modcl	⊢ ( ( - 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - 𝐴 mod 𝐵 ) ∈ ℝ )
20	12 19	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - 𝐴 mod 𝐵 ) ∈ ℝ )
21	20	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - 𝐴 mod 𝐵 ) ∈ ℂ )
22	18 21	subcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) ∈ ℂ )
23	22 7 9	divnegd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - ( ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( - ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) / 𝐵 ) )
24	16 23	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - ( ⌊ ‘ - ( 𝐴 / 𝐵 ) ) = ( - ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) / 𝐵 ) )
25	18 21	negsubdid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) = ( - - 𝐴 + ( - 𝐴 mod 𝐵 ) ) )
26	4	negnegd	⊢ ( 𝐴 ∈ ℝ → - - 𝐴 = 𝐴 )
27	26	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - - 𝐴 = 𝐴 )
28	27	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - - 𝐴 + ( - 𝐴 mod 𝐵 ) ) = ( 𝐴 + ( - 𝐴 mod 𝐵 ) ) )
29		negmod	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - 𝐴 mod 𝐵 ) = ( ( 𝐵 − 𝐴 ) mod 𝐵 ) )
30	29	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 + ( - 𝐴 mod 𝐵 ) ) = ( 𝐴 + ( ( 𝐵 − 𝐴 ) mod 𝐵 ) ) )
31	25 28 30	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) = ( 𝐴 + ( ( 𝐵 − 𝐴 ) mod 𝐵 ) ) )
32	31	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - ( - 𝐴 − ( - 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ( 𝐴 + ( ( 𝐵 − 𝐴 ) mod 𝐵 ) ) / 𝐵 ) )
33	3 24 32	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌈ ‘ ( 𝐴 / 𝐵 ) ) = ( ( 𝐴 + ( ( 𝐵 − 𝐴 ) mod 𝐵 ) ) / 𝐵 ) )