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 ⊢ A ∈ ℤ ∧ N ∈ ℤ ≥ 2 → N ⁢ A + 1 mod N = 1

Proof

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