modifeq2int

Description: If a nonnegative integer is less than twice a positive integer, the nonnegative integer modulo the positive integer equals the nonnegative integer or the nonnegative integer minus the positive integer. (Contributed by Alexander van der Vekens, 21-May-2018)

		Ref	Expression
	Assertion	modifeq2int	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \to A \mod B = if (A < B, A, A - B)$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
2		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
3	1 2	anim12i	$⊢ (A \in ℕ_{0} \land B \in ℕ) \to (A \in ℝ \land B \in ℝ^{+})$
4	3	3adant3	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \to (A \in ℝ \land B \in ℝ^{+})$
5		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
6	5	3ad2ant1	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \to 0 \leq A$
7	6	anim1i	$⊢ ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \land A < B) \to (0 \leq A \land A < B)$
8	7	ancoms	$⊢ (A < B \land (A \in ℕ_{0} \land B \in ℕ \land A < 2 B)) \to (0 \leq A \land A < B)$
9		modid	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A \mod B = A$
10	4 8 9	syl2an2	$⊢ (A < B \land (A \in ℕ_{0} \land B \in ℕ \land A < 2 B)) \to A \mod B = A$
11		iftrue	$⊢ A < B \to if (A < B, A, A - B) = A$
12	11	eqcomd	$⊢ A < B \to A = if (A < B, A, A - B)$
13	12	adantr	$⊢ (A < B \land (A \in ℕ_{0} \land B \in ℕ \land A < 2 B)) \to A = if (A < B, A, A - B)$
14	10 13	eqtrd	$⊢ (A < B \land (A \in ℕ_{0} \land B \in ℕ \land A < 2 B)) \to A \mod B = if (A < B, A, A - B)$
15	14	ex	$⊢ A < B \to ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \to A \mod B = if (A < B, A, A - B))$
16	4	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \land \neg A < B) \to (A \in ℝ \land B \in ℝ^{+})$
17		nnre	$⊢ B \in ℕ \to B \in ℝ$
18		lenlt	$⊢ (B \in ℝ \land A \in ℝ) \to (B \leq A \leftrightarrow \neg A < B)$
19	17 1 18	syl2anr	$⊢ (A \in ℕ_{0} \land B \in ℕ) \to (B \leq A \leftrightarrow \neg A < B)$
20	19	3adant3	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \to (B \leq A \leftrightarrow \neg A < B)$
21	20	biimpar	$⊢ ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \land \neg A < B) \to B \leq A$
22		simpl3	$⊢ ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \land \neg A < B) \to A < 2 B$
23		2submod	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (B \leq A \land A < 2 B)) \to A \mod B = A - B$
24	16 21 22 23	syl12anc	$⊢ ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \land \neg A < B) \to A \mod B = A - B$
25		iffalse	$⊢ \neg A < B \to if (A < B, A, A - B) = A - B$
26	25	adantl	$⊢ ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \land \neg A < B) \to if (A < B, A, A - B) = A - B$
27	26	eqcomd	$⊢ ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \land \neg A < B) \to A - B = if (A < B, A, A - B)$
28	24 27	eqtrd	$⊢ ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \land \neg A < B) \to A \mod B = if (A < B, A, A - B)$
29	28	expcom	$⊢ \neg A < B \to ((A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \to A \mod B = if (A < B, A, A - B))$
30	15 29	pm2.61i	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < 2 B) \to A \mod B = if (A < B, A, A - B)$

Metamath Proof Explorer

Theorem modifeq2int

Proof