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 \in ℤ \land N \in ℤ_{\geq 2}) \to (N A + 1) \mod N = 1$

Proof

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

Metamath Proof Explorer

Theorem mulp1mod1

Proof