# 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 ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({N}{A}+1\right)\mathrm{mod}{N}=1$

### Proof

Step Hyp Ref Expression
1 eluzelcn ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}\in ℂ$
2 1 adantl ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {N}\in ℂ$
3 zcn ${⊢}{A}\in ℤ\to {A}\in ℂ$
4 3 adantr ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {A}\in ℂ$
5 2 4 mulcomd ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {N}{A}={A}\cdot {N}$
6 5 oveq1d ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {N}{A}\mathrm{mod}{N}={A}\cdot {N}\mathrm{mod}{N}$
7 eluz2nn ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}\in ℕ$
8 7 nnrpd ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}\in {ℝ}^{+}$
9 mulmod0 ${⊢}\left({A}\in ℤ\wedge {N}\in {ℝ}^{+}\right)\to {A}\cdot {N}\mathrm{mod}{N}=0$
10 8 9 sylan2 ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {A}\cdot {N}\mathrm{mod}{N}=0$
11 6 10 eqtrd ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {N}{A}\mathrm{mod}{N}=0$
12 11 oveq1d ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({N}{A}\mathrm{mod}{N}\right)+1=0+1$
13 0p1e1 ${⊢}0+1=1$
14 12 13 eqtrdi ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({N}{A}\mathrm{mod}{N}\right)+1=1$
15 14 oveq1d ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left(\left({N}{A}\mathrm{mod}{N}\right)+1\right)\mathrm{mod}{N}=1\mathrm{mod}{N}$
16 eluzelre ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}\in ℝ$
17 16 adantl ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {N}\in ℝ$
18 zre ${⊢}{A}\in ℤ\to {A}\in ℝ$
19 18 adantr ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {A}\in ℝ$
20 17 19 remulcld ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {N}{A}\in ℝ$
21 1red ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to 1\in ℝ$
22 8 adantl ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to {N}\in {ℝ}^{+}$
23 modaddmod ${⊢}\left({N}{A}\in ℝ\wedge 1\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to \left(\left({N}{A}\mathrm{mod}{N}\right)+1\right)\mathrm{mod}{N}=\left({N}{A}+1\right)\mathrm{mod}{N}$
24 20 21 22 23 syl3anc ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left(\left({N}{A}\mathrm{mod}{N}\right)+1\right)\mathrm{mod}{N}=\left({N}{A}+1\right)\mathrm{mod}{N}$
25 eluz2gt1 ${⊢}{N}\in {ℤ}_{\ge 2}\to 1<{N}$
26 16 25 jca ${⊢}{N}\in {ℤ}_{\ge 2}\to \left({N}\in ℝ\wedge 1<{N}\right)$
27 26 adantl ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({N}\in ℝ\wedge 1<{N}\right)$
28 1mod ${⊢}\left({N}\in ℝ\wedge 1<{N}\right)\to 1\mathrm{mod}{N}=1$
29 27 28 syl ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to 1\mathrm{mod}{N}=1$
30 15 24 29 3eqtr3d ${⊢}\left({A}\in ℤ\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({N}{A}+1\right)\mathrm{mod}{N}=1$