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 )