Theorem 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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( - 𝐴 mod 𝑁 ) = ( ( 𝑁 − 𝐴 ) mod 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝑁 ∈ ℝ+ → 𝑁 ∈ ℂ )
2		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3		negsub	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑁 + - 𝐴 ) = ( 𝑁 − 𝐴 ) )
4	1 2 3	syl2anr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( 𝑁 + - 𝐴 ) = ( 𝑁 − 𝐴 ) )
5	4	eqcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( 𝑁 − 𝐴 ) = ( 𝑁 + - 𝐴 ) )
6	5	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑁 − 𝐴 ) mod 𝑁 ) = ( ( 𝑁 + - 𝐴 ) mod 𝑁 ) )
7	1	mulid2d	⊢ ( 𝑁 ∈ ℝ+ → ( 1 · 𝑁 ) = 𝑁 )
8	7	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( 1 · 𝑁 ) = 𝑁 )
9	8	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 1 · 𝑁 ) + - 𝐴 ) = ( 𝑁 + - 𝐴 ) )
10	9	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( 1 · 𝑁 ) + - 𝐴 ) mod 𝑁 ) = ( ( 𝑁 + - 𝐴 ) mod 𝑁 ) )
11		1cnd	⊢ ( 𝐴 ∈ ℝ → 1 ∈ ℂ )
12		mulcl	⊢ ( ( 1 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 1 · 𝑁 ) ∈ ℂ )
13	11 1 12	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( 1 · 𝑁 ) ∈ ℂ )
14		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
15	14	recnd	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℂ )
16	15	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → - 𝐴 ∈ ℂ )
17	13 16	addcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 1 · 𝑁 ) + - 𝐴 ) = ( - 𝐴 + ( 1 · 𝑁 ) ) )
18	17	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( 1 · 𝑁 ) + - 𝐴 ) mod 𝑁 ) = ( ( - 𝐴 + ( 1 · 𝑁 ) ) mod 𝑁 ) )
19	14	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → - 𝐴 ∈ ℝ )
20		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → 𝑁 ∈ ℝ+ )
21		1zzd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → 1 ∈ ℤ )
22		modcyc	⊢ ( ( - 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( - 𝐴 + ( 1 · 𝑁 ) ) mod 𝑁 ) = ( - 𝐴 mod 𝑁 ) )
23	19 20 21 22	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( - 𝐴 + ( 1 · 𝑁 ) ) mod 𝑁 ) = ( - 𝐴 mod 𝑁 ) )
24	18 23	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( 1 · 𝑁 ) + - 𝐴 ) mod 𝑁 ) = ( - 𝐴 mod 𝑁 ) )
25	6 10 24	3eqtr2rd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( - 𝐴 mod 𝑁 ) = ( ( 𝑁 − 𝐴 ) mod 𝑁 ) )