m1mod0mod1

Description: An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020)

		Ref	Expression
	Assertion	m1mod0mod1	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to ((A - 1) \mod N = 0 \leftrightarrow A \mod N = 1)$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		npcan1	$⊢ A \in ℂ \to A - 1 + 1 = A$
3	2	eqcomd	$⊢ A \in ℂ \to A = A - 1 + 1$
4	1 3	syl	$⊢ A \in ℝ \to A = A - 1 + 1$
5	4	3ad2ant1	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to A = A - 1 + 1$
6	5	adantr	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to A = A - 1 + 1$
7	6	oveq1d	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to A \mod N = (A - 1 + 1) \mod N$
8		simpr	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to (A - 1) \mod N = 0$
9		1mod	$⊢ (N \in ℝ \land 1 < N) \to 1 \mod N = 1$
10	9	3adant1	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to 1 \mod N = 1$
11	10	adantr	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to 1 \mod N = 1$
12	8 11	oveq12d	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to ((A - 1) \mod N) + (1 \mod N) = 0 + 1$
13	12	oveq1d	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to (((A - 1) \mod N) + (1 \mod N)) \mod N = (0 + 1) \mod N$
14		peano2rem	$⊢ A \in ℝ \to A - 1 \in ℝ$
15	14	3ad2ant1	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to A - 1 \in ℝ$
16		1red	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to 1 \in ℝ$
17		simpl	$⊢ (N \in ℝ \land 1 < N) \to N \in ℝ$
18		0lt1	$⊢ 0 < 1$
19		0re	$⊢ 0 \in ℝ$
20		1re	$⊢ 1 \in ℝ$
21		lttr	$⊢ (0 \in ℝ \land 1 \in ℝ \land N \in ℝ) \to ((0 < 1 \land 1 < N) \to 0 < N)$
22	19 20 21	mp3an12	$⊢ N \in ℝ \to ((0 < 1 \land 1 < N) \to 0 < N)$
23	18 22	mpani	$⊢ N \in ℝ \to (1 < N \to 0 < N)$
24	23	imp	$⊢ (N \in ℝ \land 1 < N) \to 0 < N$
25	17 24	elrpd	$⊢ (N \in ℝ \land 1 < N) \to N \in ℝ^{+}$
26	25	3adant1	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to N \in ℝ^{+}$
27	15 16 26	3jca	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to (A - 1 \in ℝ \land 1 \in ℝ \land N \in ℝ^{+})$
28	27	adantr	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to (A - 1 \in ℝ \land 1 \in ℝ \land N \in ℝ^{+})$
29		modaddabs	$⊢ (A - 1 \in ℝ \land 1 \in ℝ \land N \in ℝ^{+}) \to (((A - 1) \mod N) + (1 \mod N)) \mod N = (A - 1 + 1) \mod N$
30	28 29	syl	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to (((A - 1) \mod N) + (1 \mod N)) \mod N = (A - 1 + 1) \mod N$
31		0p1e1	$⊢ 0 + 1 = 1$
32	31	oveq1i	$⊢ (0 + 1) \mod N = 1 \mod N$
33	32 9	eqtrid	$⊢ (N \in ℝ \land 1 < N) \to (0 + 1) \mod N = 1$
34	33	3adant1	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to (0 + 1) \mod N = 1$
35	34	adantr	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to (0 + 1) \mod N = 1$
36	13 30 35	3eqtr3d	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to (A - 1 + 1) \mod N = 1$
37	7 36	eqtrd	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land (A - 1) \mod N = 0) \to A \mod N = 1$
38		simpr	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land A \mod N = 1) \to A \mod N = 1$
39	38	eqcomd	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land A \mod N = 1) \to 1 = A \mod N$
40	39	oveq2d	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land A \mod N = 1) \to A - 1 = A - (A \mod N)$
41	40	oveq1d	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land A \mod N = 1) \to (A - 1) \mod N = (A - (A \mod N)) \mod N$
42		simp1	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to A \in ℝ$
43	42 26	modcld	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to A \mod N \in ℝ$
44	43	recnd	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to A \mod N \in ℂ$
45	44	subidd	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to (A \mod N) - (A \mod N) = 0$
46	45	oveq1d	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to ((A \mod N) - (A \mod N)) \mod N = 0 \mod N$
47		modsubmod	$⊢ (A \in ℝ \land A \mod N \in ℝ \land N \in ℝ^{+}) \to ((A \mod N) - (A \mod N)) \mod N = (A - (A \mod N)) \mod N$
48	42 43 26 47	syl3anc	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to ((A \mod N) - (A \mod N)) \mod N = (A - (A \mod N)) \mod N$
49		0mod	$⊢ N \in ℝ^{+} \to 0 \mod N = 0$
50	26 49	syl	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to 0 \mod N = 0$
51	46 48 50	3eqtr3d	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to (A - (A \mod N)) \mod N = 0$
52	51	adantr	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land A \mod N = 1) \to (A - (A \mod N)) \mod N = 0$
53	41 52	eqtrd	$⊢ ((A \in ℝ \land N \in ℝ \land 1 < N) \land A \mod N = 1) \to (A - 1) \mod N = 0$
54	37 53	impbida	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to ((A - 1) \mod N = 0 \leftrightarrow A \mod N = 1)$

Metamath Proof Explorer

Theorem m1mod0mod1

Proof