Metamath Proof Explorer


Theorem m1mod0mod1

Description: An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020)

Ref Expression
Assertion m1mod0mod1 A N 1 < N A 1 mod N = 0 A mod N = 1

Proof

Step Hyp Ref Expression
1 recn A A
2 npcan1 A A - 1 + 1 = A
3 2 eqcomd A A = A - 1 + 1
4 1 3 syl A A = A - 1 + 1
5 4 3ad2ant1 A N 1 < N A = A - 1 + 1
6 5 adantr A N 1 < N A 1 mod N = 0 A = A - 1 + 1
7 6 oveq1d A N 1 < N A 1 mod N = 0 A mod N = A - 1 + 1 mod N
8 simpr A N 1 < N A 1 mod N = 0 A 1 mod N = 0
9 1mod N 1 < N 1 mod N = 1
10 9 3adant1 A N 1 < N 1 mod N = 1
11 10 adantr A N 1 < N A 1 mod N = 0 1 mod N = 1
12 8 11 oveq12d A N 1 < N A 1 mod N = 0 A 1 mod N + 1 mod N = 0 + 1
13 12 oveq1d A N 1 < N A 1 mod N = 0 A 1 mod N + 1 mod N mod N = 0 + 1 mod N
14 peano2rem A A 1
15 14 3ad2ant1 A N 1 < N A 1
16 1red A N 1 < N 1
17 simpl N 1 < N N
18 0lt1 0 < 1
19 0re 0
20 1re 1
21 lttr 0 1 N 0 < 1 1 < N 0 < N
22 19 20 21 mp3an12 N 0 < 1 1 < N 0 < N
23 18 22 mpani N 1 < N 0 < N
24 23 imp N 1 < N 0 < N
25 17 24 elrpd N 1 < N N +
26 25 3adant1 A N 1 < N N +
27 15 16 26 3jca A N 1 < N A 1 1 N +
28 27 adantr A N 1 < N A 1 mod N = 0 A 1 1 N +
29 modaddabs A 1 1 N + A 1 mod N + 1 mod N mod N = A - 1 + 1 mod N
30 28 29 syl A N 1 < N A 1 mod N = 0 A 1 mod N + 1 mod N mod N = A - 1 + 1 mod N
31 0p1e1 0 + 1 = 1
32 31 oveq1i 0 + 1 mod N = 1 mod N
33 32 9 syl5eq N 1 < N 0 + 1 mod N = 1
34 33 3adant1 A N 1 < N 0 + 1 mod N = 1
35 34 adantr A N 1 < N A 1 mod N = 0 0 + 1 mod N = 1
36 13 30 35 3eqtr3d A N 1 < N A 1 mod N = 0 A - 1 + 1 mod N = 1
37 7 36 eqtrd A N 1 < N A 1 mod N = 0 A mod N = 1
38 simpr A N 1 < N A mod N = 1 A mod N = 1
39 38 eqcomd A N 1 < N A mod N = 1 1 = A mod N
40 39 oveq2d A N 1 < N A mod N = 1 A 1 = A A mod N
41 40 oveq1d A N 1 < N A mod N = 1 A 1 mod N = A A mod N mod N
42 simp1 A N 1 < N A
43 42 26 modcld A N 1 < N A mod N
44 43 recnd A N 1 < N A mod N
45 44 subidd A N 1 < N A mod N A mod N = 0
46 45 oveq1d A N 1 < N A mod N A mod N mod N = 0 mod N
47 modsubmod A A mod N N + A mod N A mod N mod N = A A mod N mod N
48 42 43 26 47 syl3anc A N 1 < N A mod N A mod N mod N = A A mod N mod N
49 0mod N + 0 mod N = 0
50 26 49 syl A N 1 < N 0 mod N = 0
51 46 48 50 3eqtr3d A N 1 < N A A mod N mod N = 0
52 51 adantr A N 1 < N A mod N = 1 A A mod N mod N = 0
53 41 52 eqtrd A N 1 < N A mod N = 1 A 1 mod N = 0
54 37 53 impbida A N 1 < N A 1 mod N = 0 A mod N = 1