p1modz1

Description: If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022)

		Ref	Expression
	Assertion	p1modz1	$⊢ (M ∥ A \land 1 < M) \to (A + 1) \mod M = 1$

Proof

Step	Hyp	Ref	Expression
1		dvdszrcl	$⊢ M ∥ A \to (M \in ℤ \land A \in ℤ)$
2		0red	$⊢ (M \in ℤ \land 1 < M) \to 0 \in ℝ$
3		1red	$⊢ (M \in ℤ \land 1 < M) \to 1 \in ℝ$
4		zre	$⊢ M \in ℤ \to M \in ℝ$
5	4	adantr	$⊢ (M \in ℤ \land 1 < M) \to M \in ℝ$
6	2 3 5	3jca	$⊢ (M \in ℤ \land 1 < M) \to (0 \in ℝ \land 1 \in ℝ \land M \in ℝ)$
7		0lt1	$⊢ 0 < 1$
8	7	a1i	$⊢ M \in ℤ \to 0 < 1$
9	8	anim1i	$⊢ (M \in ℤ \land 1 < M) \to (0 < 1 \land 1 < M)$
10		lttr	$⊢ (0 \in ℝ \land 1 \in ℝ \land M \in ℝ) \to ((0 < 1 \land 1 < M) \to 0 < M)$
11	6 9 10	sylc	$⊢ (M \in ℤ \land 1 < M) \to 0 < M$
12	11	ex	$⊢ M \in ℤ \to (1 < M \to 0 < M)$
13		elnnz	$⊢ M \in ℕ \leftrightarrow (M \in ℤ \land 0 < M)$
14	13	simplbi2	$⊢ M \in ℤ \to (0 < M \to M \in ℕ)$
15	12 14	syld	$⊢ M \in ℤ \to (1 < M \to M \in ℕ)$
16	15	adantr	$⊢ (M \in ℤ \land A \in ℤ) \to (1 < M \to M \in ℕ)$
17	16	imp	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to M \in ℕ$
18		dvdsmod0	$⊢ (M \in ℕ \land M ∥ A) \to A \mod M = 0$
19	17 18	sylan	$⊢ (((M \in ℤ \land A \in ℤ) \land 1 < M) \land M ∥ A) \to A \mod M = 0$
20	19	ex	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to (M ∥ A \to A \mod M = 0)$
21		oveq1	$⊢ A \mod M = 0 \to (A \mod M) + 1 = 0 + 1$
22		0p1e1	$⊢ 0 + 1 = 1$
23	21 22	eqtrdi	$⊢ A \mod M = 0 \to (A \mod M) + 1 = 1$
24	23	oveq1d	$⊢ A \mod M = 0 \to ((A \mod M) + 1) \mod M = 1 \mod M$
25	24	adantl	$⊢ (((M \in ℤ \land A \in ℤ) \land 1 < M) \land A \mod M = 0) \to ((A \mod M) + 1) \mod M = 1 \mod M$
26		zre	$⊢ A \in ℤ \to A \in ℝ$
27	26	adantl	$⊢ (M \in ℤ \land A \in ℤ) \to A \in ℝ$
28	27	adantr	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to A \in ℝ$
29		1red	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to 1 \in ℝ$
30	17	nnrpd	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to M \in ℝ^{+}$
31	28 29 30	3jca	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to (A \in ℝ \land 1 \in ℝ \land M \in ℝ^{+})$
32	31	adantr	$⊢ (((M \in ℤ \land A \in ℤ) \land 1 < M) \land A \mod M = 0) \to (A \in ℝ \land 1 \in ℝ \land M \in ℝ^{+})$
33		modaddmod	$⊢ (A \in ℝ \land 1 \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) + 1) \mod M = (A + 1) \mod M$
34	32 33	syl	$⊢ (((M \in ℤ \land A \in ℤ) \land 1 < M) \land A \mod M = 0) \to ((A \mod M) + 1) \mod M = (A + 1) \mod M$
35	4	adantr	$⊢ (M \in ℤ \land A \in ℤ) \to M \in ℝ$
36		1mod	$⊢ (M \in ℝ \land 1 < M) \to 1 \mod M = 1$
37	35 36	sylan	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to 1 \mod M = 1$
38	37	adantr	$⊢ (((M \in ℤ \land A \in ℤ) \land 1 < M) \land A \mod M = 0) \to 1 \mod M = 1$
39	25 34 38	3eqtr3d	$⊢ (((M \in ℤ \land A \in ℤ) \land 1 < M) \land A \mod M = 0) \to (A + 1) \mod M = 1$
40	39	ex	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to (A \mod M = 0 \to (A + 1) \mod M = 1)$
41	20 40	syld	$⊢ ((M \in ℤ \land A \in ℤ) \land 1 < M) \to (M ∥ A \to (A + 1) \mod M = 1)$
42	41	ex	$⊢ (M \in ℤ \land A \in ℤ) \to (1 < M \to (M ∥ A \to (A + 1) \mod M = 1))$
43	42	com23	$⊢ (M \in ℤ \land A \in ℤ) \to (M ∥ A \to (1 < M \to (A + 1) \mod M = 1))$
44	1 43	mpcom	$⊢ M ∥ A \to (1 < M \to (A + 1) \mod M = 1)$
45	44	imp	$⊢ (M ∥ A \land 1 < M) \to (A + 1) \mod M = 1$

Metamath Proof Explorer

Theorem p1modz1

Proof