This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullidd ⊢ ( 𝑁 ∈ ℝ+ → ( 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 𝑁 ) )