Metamath Proof Explorer

Theorem m1modmmod

Description: An integer decreased by 1 modulo a positive integer minus the integer modulo the same modulus is either -1 or the modulus minus 1. (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion m1modmmod ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( ( 𝐴 mod 𝑁 ) = 0 → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − 0 ) )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − 0 ) )
3 peano2zm ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℤ )
4 3 zred ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℝ )
5 4 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − 1 ) ∈ ℝ )
6 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
7 6 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ+ )
8 5 7 modcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) mod 𝑁 ) ∈ ℝ )
9 8 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) mod 𝑁 ) ∈ ℂ )
10 9 subid1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − 0 ) = ( ( 𝐴 − 1 ) mod 𝑁 ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − 0 ) = ( ( 𝐴 − 1 ) mod 𝑁 ) )
12 mod0mul ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) = 0 → ∃ 𝑥 ∈ ℤ 𝐴 = ( 𝑥 · 𝑁 ) ) )
13 12 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ∃ 𝑥 ∈ ℤ 𝐴 = ( 𝑥 · 𝑁 ) )
14 oveq1 ⊢ ( 𝐴 = ( 𝑥 · 𝑁 ) → ( 𝐴 − 1 ) = ( ( 𝑥 · 𝑁 ) − 1 ) )
15 14 oveq1d ⊢ ( 𝐴 = ( 𝑥 · 𝑁 ) → ( ( 𝐴 − 1 ) mod 𝑁 ) = ( ( ( 𝑥 · 𝑁 ) − 1 ) mod 𝑁 ) )
16 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
17 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
18 17 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
19 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑥 · 𝑁 ) ∈ ℂ )
20 16 18 19 syl2anr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝑁 ) ∈ ℂ )
21 18 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℂ )
22 20 21 npcand ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 · 𝑁 ) − 𝑁 ) + 𝑁 ) = ( 𝑥 · 𝑁 ) )
23 22 eqcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝑁 ) = ( ( ( 𝑥 · 𝑁 ) − 𝑁 ) + 𝑁 ) )
24 16 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℂ )
25 24 21 mulsubfacd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑁 ) − 𝑁 ) = ( ( 𝑥 − 1 ) · 𝑁 ) )
26 25 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 · 𝑁 ) − 𝑁 ) + 𝑁 ) = ( ( ( 𝑥 − 1 ) · 𝑁 ) + 𝑁 ) )
27 23 26 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝑁 ) = ( ( ( 𝑥 − 1 ) · 𝑁 ) + 𝑁 ) )
28 27 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑁 ) − 1 ) = ( ( ( ( 𝑥 − 1 ) · 𝑁 ) + 𝑁 ) − 1 ) )
29 peano2zm ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 − 1 ) ∈ ℤ )
30 29 zcnd ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 − 1 ) ∈ ℂ )
31 mulcl ⊢ ( ( ( 𝑥 − 1 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑥 − 1 ) · 𝑁 ) ∈ ℂ )
32 30 18 31 syl2anr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 − 1 ) · 𝑁 ) ∈ ℂ )
33 1cnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → 1 ∈ ℂ )
34 32 21 33 addsubassd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( ( 𝑥 − 1 ) · 𝑁 ) + 𝑁 ) − 1 ) = ( ( ( 𝑥 − 1 ) · 𝑁 ) + ( 𝑁 − 1 ) ) )
35 28 34 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑁 ) − 1 ) = ( ( ( 𝑥 − 1 ) · 𝑁 ) + ( 𝑁 − 1 ) ) )
36 35 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 · 𝑁 ) − 1 ) mod 𝑁 ) = ( ( ( ( 𝑥 − 1 ) · 𝑁 ) + ( 𝑁 − 1 ) ) mod 𝑁 ) )
37 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
38 peano2rem ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
39 37 38 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℝ )
40 39 recnd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
41 40 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℂ )
42 41 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑁 − 1 ) ∈ ℂ )
43 32 42 addcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 − 1 ) · 𝑁 ) + ( 𝑁 − 1 ) ) = ( ( 𝑁 − 1 ) + ( ( 𝑥 − 1 ) · 𝑁 ) ) )
44 43 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( ( 𝑥 − 1 ) · 𝑁 ) + ( 𝑁 − 1 ) ) mod 𝑁 ) = ( ( ( 𝑁 − 1 ) + ( ( 𝑥 − 1 ) · 𝑁 ) ) mod 𝑁 ) )
45 39 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℝ )
46 45 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑁 − 1 ) ∈ ℝ )
47 7 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℝ+ )
48 29 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 − 1 ) ∈ ℤ )
49 modcyc ⊢ ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ∧ ( 𝑥 − 1 ) ∈ ℤ ) → ( ( ( 𝑁 − 1 ) + ( ( 𝑥 − 1 ) · 𝑁 ) ) mod 𝑁 ) = ( ( 𝑁 − 1 ) mod 𝑁 ) )
50 46 47 48 49 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) + ( ( 𝑥 − 1 ) · 𝑁 ) ) mod 𝑁 ) = ( ( 𝑁 − 1 ) mod 𝑁 ) )
51 39 6 jca ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
52 51 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
53 52 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
54 nnm1ge0 ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 𝑁 − 1 ) )
55 54 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 0 ≤ ( 𝑁 − 1 ) )
56 55 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → 0 ≤ ( 𝑁 − 1 ) )
57 37 ltm1d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) < 𝑁 )
58 57 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) < 𝑁 )
59 58 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑁 − 1 ) < 𝑁 )
60 modid ⊢ ( ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑁 − 1 ) ∧ ( 𝑁 − 1 ) < 𝑁 ) ) → ( ( 𝑁 − 1 ) mod 𝑁 ) = ( 𝑁 − 1 ) )
61 53 56 59 60 syl12anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑁 − 1 ) mod 𝑁 ) = ( 𝑁 − 1 ) )
62 50 61 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) + ( ( 𝑥 − 1 ) · 𝑁 ) ) mod 𝑁 ) = ( 𝑁 − 1 ) )
63 36 44 62 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 · 𝑁 ) − 1 ) mod 𝑁 ) = ( 𝑁 − 1 ) )
64 15 63 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 = ( 𝑥 · 𝑁 ) ) → ( ( 𝐴 − 1 ) mod 𝑁 ) = ( 𝑁 − 1 ) )
65 64 rexlimdva2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℤ 𝐴 = ( 𝑥 · 𝑁 ) → ( ( 𝐴 − 1 ) mod 𝑁 ) = ( 𝑁 − 1 ) ) )
66 65 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( ∃ 𝑥 ∈ ℤ 𝐴 = ( 𝑥 · 𝑁 ) → ( ( 𝐴 − 1 ) mod 𝑁 ) = ( 𝑁 − 1 ) ) )
67 13 66 mpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( ( 𝐴 − 1 ) mod 𝑁 ) = ( 𝑁 − 1 ) )
68 2 11 67 3eqtrrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( 𝑁 − 1 ) = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) )
69 df-ne ⊢ ( ( 𝐴 mod 𝑁 ) ≠ 0 ↔ ¬ ( 𝐴 mod 𝑁 ) = 0 )
70 modn0mul ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) ≠ 0 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) )
71 oveq1 ⊢ ( 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) → ( 𝐴 − 1 ) = ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) − 1 ) )
72 71 oveq1d ⊢ ( 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) → ( ( 𝐴 − 1 ) mod 𝑁 ) = ( ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) − 1 ) mod 𝑁 ) )
73 oveq1 ⊢ ( 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) → ( 𝐴 mod 𝑁 ) = ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) mod 𝑁 ) )
74 72 73 oveq12d ⊢ ( 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = ( ( ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) − 1 ) mod 𝑁 ) − ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) mod 𝑁 ) ) )
75 16 adantr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → 𝑥 ∈ ℂ )
76 75 18 19 syl2anr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( 𝑥 · 𝑁 ) ∈ ℂ )
77 elfzoelz ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 𝑦 ∈ ℤ )
78 77 zcnd ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 𝑦 ∈ ℂ )
79 78 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → 𝑦 ∈ ℂ )
80 79 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → 𝑦 ∈ ℂ )
81 1cnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → 1 ∈ ℂ )
82 76 80 81 addsubassd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) − 1 ) = ( ( 𝑥 · 𝑁 ) + ( 𝑦 − 1 ) ) )
83 peano2zm ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 − 1 ) ∈ ℤ )
84 77 83 syl ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( 𝑦 − 1 ) ∈ ℤ )
85 84 zcnd ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( 𝑦 − 1 ) ∈ ℂ )
86 85 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑦 − 1 ) ∈ ℂ )
87 86 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( 𝑦 − 1 ) ∈ ℂ )
88 76 87 addcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( 𝑥 · 𝑁 ) + ( 𝑦 − 1 ) ) = ( ( 𝑦 − 1 ) + ( 𝑥 · 𝑁 ) ) )
89 82 88 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) − 1 ) = ( ( 𝑦 − 1 ) + ( 𝑥 · 𝑁 ) ) )
90 89 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) − 1 ) mod 𝑁 ) = ( ( ( 𝑦 − 1 ) + ( 𝑥 · 𝑁 ) ) mod 𝑁 ) )
91 84 zred ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( 𝑦 − 1 ) ∈ ℝ )
92 91 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑦 − 1 ) ∈ ℝ )
93 92 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( 𝑦 − 1 ) ∈ ℝ )
94 7 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → 𝑁 ∈ ℝ+ )
95 simprl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → 𝑥 ∈ ℤ )
96 modcyc ⊢ ( ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑦 − 1 ) + ( 𝑥 · 𝑁 ) ) mod 𝑁 ) = ( ( 𝑦 − 1 ) mod 𝑁 ) )
97 93 94 95 96 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( 𝑦 − 1 ) + ( 𝑥 · 𝑁 ) ) mod 𝑁 ) = ( ( 𝑦 − 1 ) mod 𝑁 ) )
98 90 97 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) − 1 ) mod 𝑁 ) = ( ( 𝑦 − 1 ) mod 𝑁 ) )
99 76 80 addcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( 𝑥 · 𝑁 ) + 𝑦 ) = ( 𝑦 + ( 𝑥 · 𝑁 ) ) )
100 99 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) mod 𝑁 ) = ( ( 𝑦 + ( 𝑥 · 𝑁 ) ) mod 𝑁 ) )
101 77 zred ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 𝑦 ∈ ℝ )
102 101 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → 𝑦 ∈ ℝ )
103 102 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → 𝑦 ∈ ℝ )
104 modcyc ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑦 + ( 𝑥 · 𝑁 ) ) mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
105 103 94 95 104 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( 𝑦 + ( 𝑥 · 𝑁 ) ) mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
106 7 102 anim12ci ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
107 elfzole1 ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 1 ≤ 𝑦 )
108 0lt1 ⊢ 0 < 1
109 0red ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 0 ∈ ℝ )
110 1red ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 1 ∈ ℝ )
111 ltleletr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 ≤ 𝑦 ) → 0 ≤ 𝑦 ) )
112 109 110 101 111 syl3anc ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( 0 < 1 ∧ 1 ≤ 𝑦 ) → 0 ≤ 𝑦 ) )
113 108 112 mpani ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( 1 ≤ 𝑦 → 0 ≤ 𝑦 ) )
114 107 113 mpd ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 0 ≤ 𝑦 )
115 elfzolt2 ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 𝑦 < 𝑁 )
116 114 115 jca ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) )
117 116 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) )
118 117 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) )
119 106 118 jca ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) )
120 modid ⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝑦 mod 𝑁 ) = 𝑦 )
121 119 120 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( 𝑦 mod 𝑁 ) = 𝑦 )
122 100 105 121 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) mod 𝑁 ) = 𝑦 )
123 98 122 oveq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) − 1 ) mod 𝑁 ) − ( ( ( 𝑥 · 𝑁 ) + 𝑦 ) mod 𝑁 ) ) = ( ( ( 𝑦 − 1 ) mod 𝑁 ) − 𝑦 ) )
124 74 123 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) ∧ 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = ( ( ( 𝑦 − 1 ) mod 𝑁 ) − 𝑦 ) )
125 7 92 anim12ci ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
126 elfzo2 ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) )
127 eluz2 ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 1 ≤ 𝑦 ) )
128 zre ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
129 zre ⊢ ( 1 ∈ ℤ → 1 ∈ ℝ )
130 subge0 ⊢ ( ( 𝑦 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ ( 𝑦 − 1 ) ↔ 1 ≤ 𝑦 ) )
131 128 129 130 syl2anr ⊢ ( ( 1 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 0 ≤ ( 𝑦 − 1 ) ↔ 1 ≤ 𝑦 ) )
132 131 biimp3ar ⊢ ( ( 1 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 1 ≤ 𝑦 ) → 0 ≤ ( 𝑦 − 1 ) )
133 127 132 sylbi ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) → 0 ≤ ( 𝑦 − 1 ) )
134 133 3ad2ant1 ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → 0 ≤ ( 𝑦 − 1 ) )
135 126 134 sylbi ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 0 ≤ ( 𝑦 − 1 ) )
136 135 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → 0 ≤ ( 𝑦 − 1 ) )
137 136 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → 0 ≤ ( 𝑦 − 1 ) )
138 eluzelz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) → 𝑦 ∈ ℤ )
139 138 zred ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) → 𝑦 ∈ ℝ )
140 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
141 ltle ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑦 < 𝑁 → 𝑦 ≤ 𝑁 ) )
142 139 140 141 syl2an ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑦 < 𝑁 → 𝑦 ≤ 𝑁 ) )
143 142 3impia ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → 𝑦 ≤ 𝑁 )
144 138 anim1i ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
145 144 3adant3 ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
146 zlem1lt ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑦 ≤ 𝑁 ↔ ( 𝑦 − 1 ) < 𝑁 ) )
147 145 146 syl ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → ( 𝑦 ≤ 𝑁 ↔ ( 𝑦 − 1 ) < 𝑁 ) )
148 143 147 mpbid ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → ( 𝑦 − 1 ) < 𝑁 )
149 148 a1d ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑦 − 1 ) < 𝑁 ) )
150 126 149 sylbi ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑦 − 1 ) < 𝑁 ) )
151 150 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑦 − 1 ) < 𝑁 ) )
152 151 impcom ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( 𝑦 − 1 ) < 𝑁 )
153 modid ⊢ ( ( ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑦 − 1 ) ∧ ( 𝑦 − 1 ) < 𝑁 ) ) → ( ( 𝑦 − 1 ) mod 𝑁 ) = ( 𝑦 − 1 ) )
154 125 137 152 153 syl12anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( 𝑦 − 1 ) mod 𝑁 ) = ( 𝑦 − 1 ) )
155 154 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( 𝑦 − 1 ) mod 𝑁 ) − 𝑦 ) = ( ( 𝑦 − 1 ) − 𝑦 ) )
156 1cnd ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 1 ∈ ℂ )
157 78 156 78 sub32d ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑦 − 1 ) − 𝑦 ) = ( ( 𝑦 − 𝑦 ) − 1 ) )
158 78 subidd ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( 𝑦 − 𝑦 ) = 0 )
159 158 oveq1d ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑦 − 𝑦 ) − 1 ) = ( 0 − 1 ) )
160 157 159 eqtrd ⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑦 − 1 ) − 𝑦 ) = ( 0 − 1 ) )
161 160 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑦 − 1 ) − 𝑦 ) = ( 0 − 1 ) )
162 161 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( 𝑦 − 1 ) − 𝑦 ) = ( 0 − 1 ) )
163 df-neg ⊢ - 1 = ( 0 − 1 )
164 162 163 eqtr4di ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( 𝑦 − 1 ) − 𝑦 ) = - 1 )
165 155 164 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( ( ( 𝑦 − 1 ) mod 𝑁 ) − 𝑦 ) = - 1 )
166 165 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) ∧ 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) → ( ( ( 𝑦 − 1 ) mod 𝑁 ) − 𝑦 ) = - 1 )
167 124 166 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) ∧ 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = - 1 )
168 167 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) ∧ 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) → - 1 = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) )
169 168 ex ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) → ( 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) → - 1 = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) ) )
170 169 rexlimdvva ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) → - 1 = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) ) )
171 70 170 syld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) ≠ 0 → - 1 = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) ) )
172 69 171 biimtrrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ¬ ( 𝐴 mod 𝑁 ) = 0 → - 1 = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) ) )
173 172 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 mod 𝑁 ) = 0 ) → - 1 = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) )
174 68 173 ifeqda ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) = ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) )
175 174 eqcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) − ( 𝐴 mod 𝑁 ) ) = if ( ( 𝐴 mod 𝑁 ) = 0 , ( 𝑁 − 1 ) , - 1 ) )