negmod

Description: The negation of a number modulo a positive number is equal to the difference of the modulus and the number modulo the modulus. (Contributed by AV, 5-Jul-2020)

		Ref	Expression
	Assertion	negmod	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (- A) \mod N = (N - A) \mod N$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$⊢ N \in ℝ^{+} \to N \in ℂ$
2		recn	$⊢ A \in ℝ \to A \in ℂ$
3		negsub	$⊢ (N \in ℂ \land A \in ℂ) \to N + (- A) = N - A$
4	1 2 3	syl2anr	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to N + (- A) = N - A$
5	4	eqcomd	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to N - A = N + (- A)$
6	5	oveq1d	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (N - A) \mod N = (N + (- A)) \mod N$
7	1	mulid2d	$⊢ N \in ℝ^{+} \to 1 \cdot N = N$
8	7	adantl	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to 1 \cdot N = N$
9	8	oveq1d	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to 1 \cdot N + (- A) = N + (- A)$
10	9	oveq1d	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (1 \cdot N + (- A)) \mod N = (N + (- A)) \mod N$
11		1cnd	$⊢ A \in ℝ \to 1 \in ℂ$
12		mulcl	$⊢ (1 \in ℂ \land N \in ℂ) \to 1 \cdot N \in ℂ$
13	11 1 12	syl2an	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to 1 \cdot N \in ℂ$
14		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
15	14	recnd	$⊢ A \in ℝ \to - A \in ℂ$
16	15	adantr	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to - A \in ℂ$
17	13 16	addcomd	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to 1 \cdot N + (- A) = - A + 1 \cdot N$
18	17	oveq1d	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (1 \cdot N + (- A)) \mod N = (- A + 1 \cdot N) \mod N$
19	14	adantr	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to - A \in ℝ$
20		simpr	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to N \in ℝ^{+}$
21		1zzd	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to 1 \in ℤ$
22		modcyc	$⊢ (- A \in ℝ \land N \in ℝ^{+} \land 1 \in ℤ) \to (- A + 1 \cdot N) \mod N = (- A) \mod N$
23	19 20 21 22	syl3anc	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (- A + 1 \cdot N) \mod N = (- A) \mod N$
24	18 23	eqtrd	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (1 \cdot N + (- A)) \mod N = (- A) \mod N$
25	6 10 24	3eqtr2rd	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (- A) \mod N = (N - A) \mod N$

Metamath Proof Explorer

Theorem negmod

Proof