submodlt

Description: The difference of an element of a half-open range of nonnegative integers and the upper bound of this range modulo an integer greater than the upper bound. (Contributed by AV, 1-Sep-2025)

		Ref	Expression
	Assertion	submodlt	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (A - B) \mod N = N + A - B$

Proof

Step	Hyp	Ref	Expression
1		elfzoel2	$⊢ A \in (0 ..^B) \to B \in ℤ$
2	1	zcnd	$⊢ A \in (0 ..^B) \to B \in ℂ$
3		elfzoelz	$⊢ A \in (0 ..^B) \to A \in ℤ$
4	3	zcnd	$⊢ A \in (0 ..^B) \to A \in ℂ$
5	2 4	jca	$⊢ A \in (0 ..^B) \to (B \in ℂ \land A \in ℂ)$
6	5	3ad2ant2	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (B \in ℂ \land A \in ℂ)$
7		negsubdi2	$⊢ (B \in ℂ \land A \in ℂ) \to - (B - A) = A - B$
8	6 7	syl	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to - (B - A) = A - B$
9	8	eqcomd	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to A - B = - (B - A)$
10	9	oveq1d	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (A - B) \mod N = (- (B - A)) \mod N$
11	1 3	zsubcld	$⊢ A \in (0 ..^B) \to B - A \in ℤ$
12	11	zred	$⊢ A \in (0 ..^B) \to B - A \in ℝ$
13	12	3ad2ant2	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to B - A \in ℝ$
14		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
15	14	3ad2ant1	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to N \in ℝ^{+}$
16		negmod	$⊢ (B - A \in ℝ \land N \in ℝ^{+}) \to (- (B - A)) \mod N = (N - (B - A)) \mod N$
17	13 15 16	syl2anc	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (- (B - A)) \mod N = (N - (B - A)) \mod N$
18	10 17	eqtrd	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (A - B) \mod N = (N - (B - A)) \mod N$
19		nnz	$⊢ N \in ℕ \to N \in ℤ$
20	19	3ad2ant1	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to N \in ℤ$
21	11	3ad2ant2	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to B - A \in ℤ$
22	20 21	zsubcld	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to N - (B - A) \in ℤ$
23	22	zred	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to N - (B - A) \in ℝ$
24	1	zred	$⊢ A \in (0 ..^B) \to B \in ℝ$
25	24	3ad2ant2	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to B \in ℝ$
26		nnre	$⊢ N \in ℕ \to N \in ℝ$
27	26	3ad2ant1	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to N \in ℝ$
28		elfzo0suble	$⊢ A \in (0 ..^B) \to B - A \leq B$
29	28	3ad2ant2	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to B - A \leq B$
30		simp3	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to B < N$
31		leltletr	$⊢ (B - A \in ℝ \land B \in ℝ \land N \in ℝ) \to ((B - A \leq B \land B < N) \to B - A \leq N)$
32	31	imp	$⊢ ((B - A \in ℝ \land B \in ℝ \land N \in ℝ) \land (B - A \leq B \land B < N)) \to B - A \leq N$
33	13 25 27 29 30 32	syl32anc	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to B - A \leq N$
34	27 13	subge0d	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (0 \leq N - (B - A) \leftrightarrow B - A \leq N)$
35	33 34	mpbird	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to 0 \leq N - (B - A)$
36		elfzo0	$⊢ A \in (0 ..^B) \leftrightarrow (A \in ℕ_{0} \land B \in ℕ \land A < B)$
37		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
38		nnre	$⊢ B \in ℕ \to B \in ℝ$
39		posdif	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow 0 < B - A)$
40	37 38 39	syl2an	$⊢ (A \in ℕ_{0} \land B \in ℕ) \to (A < B \leftrightarrow 0 < B - A)$
41	40	biimp3a	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < B) \to 0 < B - A$
42	36 41	sylbi	$⊢ A \in (0 ..^B) \to 0 < B - A$
43	42	3ad2ant2	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to 0 < B - A$
44	13 27	ltsubposd	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (0 < B - A \leftrightarrow N - (B - A) < N)$
45	43 44	mpbid	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to N - (B - A) < N$
46		modid	$⊢ ((N - (B - A) \in ℝ \land N \in ℝ^{+}) \land (0 \leq N - (B - A) \land N - (B - A) < N)) \to (N - (B - A)) \mod N = N - (B - A)$
47	23 15 35 45 46	syl22anc	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (N - (B - A)) \mod N = N - (B - A)$
48		nncn	$⊢ N \in ℕ \to N \in ℂ$
49	48	3ad2ant1	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to N \in ℂ$
50	2	3ad2ant2	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to B \in ℂ$
51	4	3ad2ant2	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to A \in ℂ$
52	49 50 51	subsub3d	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to N - (B - A) = N + A - B$
53	18 47 52	3eqtrd	$⊢ (N \in ℕ \land A \in (0 ..^B) \land B < N) \to (A - B) \mod N = N + A - B$

Metamath Proof Explorer

Theorem submodlt

Proof