This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )