Metamath Proof Explorer


Theorem addmodlteqALT

Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. Shorter proof of addmodlteq based on the "divides" relation. (Contributed by AV, 14-Mar-2021) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion addmodlteqALT I0..^NJ0..^NSI+SmodN=J+SmodNI=J

Proof

Step Hyp Ref Expression
1 elfzo0 I0..^NI0NI<N
2 elfzoelz J0..^NJ
3 simplrr JI0NSN
4 nn0z I0I
5 4 ad2antrl JI0NI
6 zaddcl ISI+S
7 5 6 sylan JI0NSI+S
8 zaddcl JSJ+S
9 8 adantlr JI0NSJ+S
10 3 7 9 3jca JI0NSNI+SJ+S
11 10 exp31 JI0NSNI+SJ+S
12 2 11 syl J0..^NI0NSNI+SJ+S
13 12 com12 I0NJ0..^NSNI+SJ+S
14 13 3adant3 I0NI<NJ0..^NSNI+SJ+S
15 1 14 sylbi I0..^NJ0..^NSNI+SJ+S
16 15 3imp I0..^NJ0..^NSNI+SJ+S
17 moddvds NI+SJ+SI+SmodN=J+SmodNNI+S-J+S
18 16 17 syl I0..^NJ0..^NSI+SmodN=J+SmodNNI+S-J+S
19 elfzoel2 I0..^NN
20 zcn NN
21 20 subid1d NN0=N
22 21 eqcomd NN=N0
23 19 22 syl I0..^NN=N0
24 23 3ad2ant1 I0..^NJ0..^NSN=N0
25 elfzoelz I0..^NI
26 25 zcnd I0..^NI
27 2 zcnd J0..^NJ
28 zcn SS
29 pnpcan2 IJSI+S-J+S=IJ
30 26 27 28 29 syl3an I0..^NJ0..^NSI+S-J+S=IJ
31 24 30 breq12d I0..^NJ0..^NSNI+S-J+SN0IJ
32 fzocongeq I0..^NJ0..^NN0IJI=J
33 32 3adant3 I0..^NJ0..^NSN0IJI=J
34 18 31 33 3bitrd I0..^NJ0..^NSI+SmodN=J+SmodNI=J