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 
|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A - 1 ) mod N ) - ( A mod N ) ) = if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) )

Proof

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