difmodm1lt

Description: The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd A and N = 2 , since ( ( A mod N ) - ( ( A - 1 ) mod N ) ) would be ( 1 - 0 ) = 1 which is not less than ( N - 1 ) = 1 . (Contributed by AV, 6-Jun-2012)

		Ref	Expression
	Assertion	difmodm1lt	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \mod N) - ((A - 1) \mod N) < N - 1$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to A \mod N = 1$
2		zre	$⊢ A \in ℤ \to A \in ℝ$
3	2	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A \in ℝ$
4		nnre	$⊢ N \in ℕ \to N \in ℝ$
5	4	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to N \in ℝ$
6		1lt2	$⊢ 1 < 2$
7		1red	$⊢ N \in ℕ \to 1 \in ℝ$
8		2re	$⊢ 2 \in ℝ$
9	8	a1i	$⊢ N \in ℕ \to 2 \in ℝ$
10	7 9 4	3jca	$⊢ N \in ℕ \to (1 \in ℝ \land 2 \in ℝ \land N \in ℝ)$
11		lttr	$⊢ (1 \in ℝ \land 2 \in ℝ \land N \in ℝ) \to ((1 < 2 \land 2 < N) \to 1 < N)$
12	10 11	syl	$⊢ N \in ℕ \to ((1 < 2 \land 2 < N) \to 1 < N)$
13	6 12	mpani	$⊢ N \in ℕ \to (2 < N \to 1 < N)$
14	13	a1i	$⊢ A \in ℤ \to (N \in ℕ \to (2 < N \to 1 < N))$
15	14	3imp	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 1 < N$
16	3 5 15	3jca	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \in ℝ \land N \in ℝ \land 1 < N)$
17	16	adantl	$⊢ (A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A \in ℝ \land N \in ℝ \land 1 < N)$
18		m1mod0mod1	$⊢ (A \in ℝ \land N \in ℝ \land 1 < N) \to ((A - 1) \mod N = 0 \leftrightarrow A \mod N = 1)$
19	17 18	syl	$⊢ (A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to ((A - 1) \mod N = 0 \leftrightarrow A \mod N = 1)$
20	1 19	mpbird	$⊢ (A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A - 1) \mod N = 0$
21	1 20	oveq12d	$⊢ (A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A \mod N) - ((A - 1) \mod N) = 1 - 0$
22		df-2	$⊢ 2 = 1 + 1$
23	22	breq1i	$⊢ 2 < N \leftrightarrow 1 + 1 < N$
24	23	biimpi	$⊢ 2 < N \to 1 + 1 < N$
25	24	adantl	$⊢ (N \in ℕ \land 2 < N) \to 1 + 1 < N$
26		1red	$⊢ (N \in ℕ \land 2 < N) \to 1 \in ℝ$
27	4	adantr	$⊢ (N \in ℕ \land 2 < N) \to N \in ℝ$
28	26 26 27	ltaddsub2d	$⊢ (N \in ℕ \land 2 < N) \to (1 + 1 < N \leftrightarrow 1 < N - 1)$
29	25 28	mpbid	$⊢ (N \in ℕ \land 2 < N) \to 1 < N - 1$
30		1m0e1	$⊢ 1 - 0 = 1$
31	30	breq1i	$⊢ 1 - 0 < N - 1 \leftrightarrow 1 < N - 1$
32	29 31	sylibr	$⊢ (N \in ℕ \land 2 < N) \to 1 - 0 < N - 1$
33	32	3adant1	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 1 - 0 < N - 1$
34	33	adantl	$⊢ (A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to 1 - 0 < N - 1$
35	21 34	eqbrtrd	$⊢ (A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A \mod N) - ((A - 1) \mod N) < N - 1$
36		zmodfz	$⊢ (A \in ℤ \land N \in ℕ) \to A \mod N \in (0 \dots N - 1)$
37	36	3adant3	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A \mod N \in (0 \dots N - 1)$
38		elfzle2	$⊢ A \mod N \in (0 \dots N - 1) \to A \mod N \leq N - 1$
39	37 38	syl	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A \mod N \leq N - 1$
40	39	adantl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to A \mod N \leq N - 1$
41		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
42	41	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to N \in ℝ^{+}$
43	3 42	modcld	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A \mod N \in ℝ$
44		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
45	4 44	syl	$⊢ N \in ℕ \to N - 1 \in ℝ$
46	45	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to N - 1 \in ℝ$
47		peano2zm	$⊢ A \in ℤ \to A - 1 \in ℤ$
48	47	zred	$⊢ A \in ℤ \to A - 1 \in ℝ$
49	48	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A - 1 \in ℝ$
50	49 42	modcld	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A - 1) \mod N \in ℝ$
51	43 46 50	3jca	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \mod N \in ℝ \land N - 1 \in ℝ \land (A - 1) \mod N \in ℝ)$
52	51	adantl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A \mod N \in ℝ \land N - 1 \in ℝ \land (A - 1) \mod N \in ℝ)$
53		lesub1	$⊢ (A \mod N \in ℝ \land N - 1 \in ℝ \land (A - 1) \mod N \in ℝ) \to (A \mod N \leq N - 1 \leftrightarrow (A \mod N) - ((A - 1) \mod N) \leq N - 1 - ((A - 1) \mod N))$
54	52 53	syl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A \mod N \leq N - 1 \leftrightarrow (A \mod N) - ((A - 1) \mod N) \leq N - 1 - ((A - 1) \mod N))$
55	40 54	mpbid	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A \mod N) - ((A - 1) \mod N) \leq N - 1 - ((A - 1) \mod N)$
56	49 42	jca	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A - 1 \in ℝ \land N \in ℝ^{+})$
57	56	adantl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A - 1 \in ℝ \land N \in ℝ^{+})$
58		modge0	$⊢ (A - 1 \in ℝ \land N \in ℝ^{+}) \to 0 \leq (A - 1) \mod N$
59	57 58	syl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to 0 \leq (A - 1) \mod N$
60	16 18	syl	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to ((A - 1) \mod N = 0 \leftrightarrow A \mod N = 1)$
61	60	bicomd	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \mod N = 1 \leftrightarrow (A - 1) \mod N = 0)$
62	61	notbid	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (\neg A \mod N = 1 \leftrightarrow \neg (A - 1) \mod N = 0)$
63	62	biimpac	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to \neg (A - 1) \mod N = 0$
64	63	neqned	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A - 1) \mod N \neq 0$
65	59 64	jca	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (0 \leq (A - 1) \mod N \land (A - 1) \mod N \neq 0)$
66		0red	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 0 \in ℝ$
67	66 50	jca	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (0 \in ℝ \land (A - 1) \mod N \in ℝ)$
68	67	adantl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (0 \in ℝ \land (A - 1) \mod N \in ℝ)$
69		ltlen	$⊢ (0 \in ℝ \land (A - 1) \mod N \in ℝ) \to (0 < (A - 1) \mod N \leftrightarrow (0 \leq (A - 1) \mod N \land (A - 1) \mod N \neq 0))$
70	68 69	syl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (0 < (A - 1) \mod N \leftrightarrow (0 \leq (A - 1) \mod N \land (A - 1) \mod N \neq 0))$
71	65 70	mpbird	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to 0 < (A - 1) \mod N$
72	50 46	jca	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to ((A - 1) \mod N \in ℝ \land N - 1 \in ℝ)$
73	72	adantl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to ((A - 1) \mod N \in ℝ \land N - 1 \in ℝ)$
74		ltsubpos	$⊢ ((A - 1) \mod N \in ℝ \land N - 1 \in ℝ) \to (0 < (A - 1) \mod N \leftrightarrow N - 1 - ((A - 1) \mod N) < N - 1)$
75	73 74	syl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (0 < (A - 1) \mod N \leftrightarrow N - 1 - ((A - 1) \mod N) < N - 1)$
76	71 75	mpbid	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to N - 1 - ((A - 1) \mod N) < N - 1$
77	43 50	resubcld	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \mod N) - ((A - 1) \mod N) \in ℝ$
78	46 50	resubcld	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to N - 1 - ((A - 1) \mod N) \in ℝ$
79	77 78 46	3jca	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to ((A \mod N) - ((A - 1) \mod N) \in ℝ \land N - 1 - ((A - 1) \mod N) \in ℝ \land N - 1 \in ℝ)$
80	79	adantl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to ((A \mod N) - ((A - 1) \mod N) \in ℝ \land N - 1 - ((A - 1) \mod N) \in ℝ \land N - 1 \in ℝ)$
81		lelttr	$⊢ ((A \mod N) - ((A - 1) \mod N) \in ℝ \land N - 1 - ((A - 1) \mod N) \in ℝ \land N - 1 \in ℝ) \to (((A \mod N) - ((A - 1) \mod N) \leq N - 1 - ((A - 1) \mod N) \land N - 1 - ((A - 1) \mod N) < N - 1) \to (A \mod N) - ((A - 1) \mod N) < N - 1)$
82	80 81	syl	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (((A \mod N) - ((A - 1) \mod N) \leq N - 1 - ((A - 1) \mod N) \land N - 1 - ((A - 1) \mod N) < N - 1) \to (A \mod N) - ((A - 1) \mod N) < N - 1)$
83	55 76 82	mp2and	$⊢ (\neg A \mod N = 1 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to (A \mod N) - ((A - 1) \mod N) < N - 1$
84	35 83	pm2.61ian	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \mod N) - ((A - 1) \mod N) < N - 1$

Metamath Proof Explorer

Theorem difmodm1lt

Proof