Metamath Proof Explorer


Theorem mulp1mod1

Description: The product of an integer and an integer greater than 1 increased by 1 is 1 modulo the integer greater than 1. (Contributed by AV, 15-Jul-2021)

Ref Expression
Assertion mulp1mod1 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ( 𝑁 · 𝐴 ) + 1 ) mod 𝑁 ) = 1 )

Proof

Step Hyp Ref Expression
1 eluzelcn ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℂ )
2 1 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → 𝑁 ∈ ℂ )
3 zcn ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
4 3 adantr ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → 𝐴 ∈ ℂ )
5 2 4 mulcomd ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑁 · 𝐴 ) = ( 𝐴 · 𝑁 ) )
6 5 oveq1d ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑁 · 𝐴 ) mod 𝑁 ) = ( ( 𝐴 · 𝑁 ) mod 𝑁 ) )
7 eluz2nn ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℕ )
8 7 nnrpd ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℝ+ )
9 mulmod0 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝐴 · 𝑁 ) mod 𝑁 ) = 0 )
10 8 9 sylan2 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝐴 · 𝑁 ) mod 𝑁 ) = 0 )
11 6 10 eqtrd ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑁 · 𝐴 ) mod 𝑁 ) = 0 )
12 11 oveq1d ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ( 𝑁 · 𝐴 ) mod 𝑁 ) + 1 ) = ( 0 + 1 ) )
13 0p1e1 ( 0 + 1 ) = 1
14 12 13 eqtrdi ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ( 𝑁 · 𝐴 ) mod 𝑁 ) + 1 ) = 1 )
15 14 oveq1d ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ( ( 𝑁 · 𝐴 ) mod 𝑁 ) + 1 ) mod 𝑁 ) = ( 1 mod 𝑁 ) )
16 eluzelre ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℝ )
17 16 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → 𝑁 ∈ ℝ )
18 zre ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
19 18 adantr ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → 𝐴 ∈ ℝ )
20 17 19 remulcld ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑁 · 𝐴 ) ∈ ℝ )
21 1red ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → 1 ∈ ℝ )
22 8 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → 𝑁 ∈ ℝ+ )
23 modaddmod ( ( ( 𝑁 · 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( ( 𝑁 · 𝐴 ) mod 𝑁 ) + 1 ) mod 𝑁 ) = ( ( ( 𝑁 · 𝐴 ) + 1 ) mod 𝑁 ) )
24 20 21 22 23 syl3anc ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ( ( 𝑁 · 𝐴 ) mod 𝑁 ) + 1 ) mod 𝑁 ) = ( ( ( 𝑁 · 𝐴 ) + 1 ) mod 𝑁 ) )
25 eluz2gt1 ( 𝑁 ∈ ( ℤ ‘ 2 ) → 1 < 𝑁 )
26 16 25 jca ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) )
27 26 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) )
28 1mod ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 1 mod 𝑁 ) = 1 )
29 27 28 syl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 1 mod 𝑁 ) = 1 )
30 15 24 29 3eqtr3d ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ( 𝑁 · 𝐴 ) + 1 ) mod 𝑁 ) = 1 )