Metamath Proof Explorer

Theorem p1modz1

Description: If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022)

Ref Expression
Assertion p1modz1 ( ( 𝑀 ∥ 𝐴 ∧ 1 < 𝑀 ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = 1 )

Proof

Step Hyp Ref Expression
1 dvdszrcl ⊢ ( 𝑀 ∥ 𝐴 → ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
2 0red ⊢ ( ( 𝑀 ∈ ℤ ∧ 1 < 𝑀 ) → 0 ∈ ℝ )
3 1red ⊢ ( ( 𝑀 ∈ ℤ ∧ 1 < 𝑀 ) → 1 ∈ ℝ )
4 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
5 4 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 1 < 𝑀 ) → 𝑀 ∈ ℝ )
6 2 3 5 3jca ⊢ ( ( 𝑀 ∈ ℤ ∧ 1 < 𝑀 ) → ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
7 0lt1 ⊢ 0 < 1
8 7 a1i ⊢ ( 𝑀 ∈ ℤ → 0 < 1 )
9 8 anim1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 1 < 𝑀 ) → ( 0 < 1 ∧ 1 < 𝑀 ) )
10 lttr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝑀 ) → 0 < 𝑀 ) )
11 6 9 10 sylc ⊢ ( ( 𝑀 ∈ ℤ ∧ 1 < 𝑀 ) → 0 < 𝑀 )
12 11 ex ⊢ ( 𝑀 ∈ ℤ → ( 1 < 𝑀 → 0 < 𝑀 ) )
13 elnnz ⊢ ( 𝑀 ∈ ℕ ↔ ( 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
14 13 simplbi2 ⊢ ( 𝑀 ∈ ℤ → ( 0 < 𝑀 → 𝑀 ∈ ℕ ) )
15 12 14 syld ⊢ ( 𝑀 ∈ ℤ → ( 1 < 𝑀 → 𝑀 ∈ ℕ ) )
16 15 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 1 < 𝑀 → 𝑀 ∈ ℕ ) )
17 16 imp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → 𝑀 ∈ ℕ )
18 dvdsmod0 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝐴 ) → ( 𝐴 mod 𝑀 ) = 0 )
19 17 18 sylan ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) ∧ 𝑀 ∥ 𝐴 ) → ( 𝐴 mod 𝑀 ) = 0 )
20 19 ex ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → ( 𝑀 ∥ 𝐴 → ( 𝐴 mod 𝑀 ) = 0 ) )
21 oveq1 ⊢ ( ( 𝐴 mod 𝑀 ) = 0 → ( ( 𝐴 mod 𝑀 ) + 1 ) = ( 0 + 1 ) )
22 0p1e1 ⊢ ( 0 + 1 ) = 1
23 21 22 eqtrdi ⊢ ( ( 𝐴 mod 𝑀 ) = 0 → ( ( 𝐴 mod 𝑀 ) + 1 ) = 1 )
24 23 oveq1d ⊢ ( ( 𝐴 mod 𝑀 ) = 0 → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( 1 mod 𝑀 ) )
25 24 adantl ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) ∧ ( 𝐴 mod 𝑀 ) = 0 ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( 1 mod 𝑀 ) )
26 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
27 26 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℝ )
28 27 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → 𝐴 ∈ ℝ )
29 1red ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → 1 ∈ ℝ )
30 17 nnrpd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → 𝑀 ∈ ℝ+ )
31 28 29 30 3jca ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
32 31 adantr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) ∧ ( 𝐴 mod 𝑀 ) = 0 ) → ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
33 modaddmod ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( 𝐴 + 1 ) mod 𝑀 ) )
34 32 33 syl ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) ∧ ( 𝐴 mod 𝑀 ) = 0 ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( 𝐴 + 1 ) mod 𝑀 ) )
35 4 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → 𝑀 ∈ ℝ )
36 1mod ⊢ ( ( 𝑀 ∈ ℝ ∧ 1 < 𝑀 ) → ( 1 mod 𝑀 ) = 1 )
37 35 36 sylan ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → ( 1 mod 𝑀 ) = 1 )
38 37 adantr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) ∧ ( 𝐴 mod 𝑀 ) = 0 ) → ( 1 mod 𝑀 ) = 1 )
39 25 34 38 3eqtr3d ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) ∧ ( 𝐴 mod 𝑀 ) = 0 ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = 1 )
40 39 ex ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → ( ( 𝐴 mod 𝑀 ) = 0 → ( ( 𝐴 + 1 ) mod 𝑀 ) = 1 ) )
41 20 40 syld ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 1 < 𝑀 ) → ( 𝑀 ∥ 𝐴 → ( ( 𝐴 + 1 ) mod 𝑀 ) = 1 ) )
42 41 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 1 < 𝑀 → ( 𝑀 ∥ 𝐴 → ( ( 𝐴 + 1 ) mod 𝑀 ) = 1 ) ) )
43 42 com23 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑀 ∥ 𝐴 → ( 1 < 𝑀 → ( ( 𝐴 + 1 ) mod 𝑀 ) = 1 ) ) )
44 1 43 mpcom ⊢ ( 𝑀 ∥ 𝐴 → ( 1 < 𝑀 → ( ( 𝐴 + 1 ) mod 𝑀 ) = 1 ) )
45 44 imp ⊢ ( ( 𝑀 ∥ 𝐴 ∧ 1 < 𝑀 ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = 1 )