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 ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( ( ( 𝐴 − 1 ) mod 𝑁 ) = 0 ↔ ( 𝐴 mod 𝑁 ) = 1 ) )

Proof

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