addmodne

Description: The sum of a nonnegative integer and a positive integer modulo a number greater than both integers is not equal to the nonnegative integer. (Contributed by AV, 27-Aug-2025) (Proof shortened by AV, 6-Sep-2025)

		Ref	Expression
	Assertion	addmodne	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to (A + B) \mod M \neq A$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2	1	a1i	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to 2 \in ℤ$
3		nnz	$⊢ M \in ℕ \to M \in ℤ$
4	3	adantr	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to M \in ℤ$
5		1red	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to 1 \in ℝ$
6		nnre	$⊢ B \in ℕ \to B \in ℝ$
7	6	ad2antrl	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to B \in ℝ$
8		nnre	$⊢ M \in ℕ \to M \in ℝ$
9	8	adantr	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to M \in ℝ$
10		nnge1	$⊢ B \in ℕ \to 1 \leq B$
11	10	ad2antrl	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to 1 \leq B$
12		simprr	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to B < M$
13	5 7 9 11 12	lelttrd	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to 1 < M$
14		1zzd	$⊢ (B \in ℕ \land B < M) \to 1 \in ℤ$
15		zltp1le	$⊢ (1 \in ℤ \land M \in ℤ) \to (1 < M \leftrightarrow 1 + 1 \leq M)$
16	14 3 15	syl2anr	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to (1 < M \leftrightarrow 1 + 1 \leq M)$
17		1p1e2	$⊢ 1 + 1 = 2$
18	17	breq1i	$⊢ 1 + 1 \leq M \leftrightarrow 2 \leq M$
19	16 18	bitrdi	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to (1 < M \leftrightarrow 2 \leq M)$
20	13 19	mpbid	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to 2 \leq M$
21	2 4 20	3jca	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to (2 \in ℤ \land M \in ℤ \land 2 \leq M)$
22	21	3adant2	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to (2 \in ℤ \land M \in ℤ \land 2 \leq M)$
23		eluz2	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land M \in ℤ \land 2 \leq M)$
24	22 23	sylibr	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to M \in ℤ_{\geq 2}$
25		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
26	25	adantr	$⊢ (A \in ℕ_{0} \land A < M) \to A \in ℤ$
27	26	3ad2ant2	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to A \in ℤ$
28		simprl	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to B \in ℕ$
29		simpl	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to M \in ℕ$
30	28 29 12	3jca	$⊢ (M \in ℕ \land (B \in ℕ \land B < M)) \to (B \in ℕ \land M \in ℕ \land B < M)$
31	30	3adant2	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to (B \in ℕ \land M \in ℕ \land B < M)$
32		elfzo1	$⊢ B \in (1 ..^M) \leftrightarrow (B \in ℕ \land M \in ℕ \land B < M)$
33	31 32	sylibr	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to B \in (1 ..^M)$
34		zplusmodne	$⊢ (M \in ℤ_{\geq 2} \land A \in ℤ \land B \in (1 ..^M)) \to (A + B) \mod M \neq A \mod M$
35	24 27 33 34	syl3anc	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to (A + B) \mod M \neq A \mod M$
36		nnrp	$⊢ M \in ℕ \to M \in ℝ^{+}$
37		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
38	37	adantr	$⊢ (A \in ℕ_{0} \land A < M) \to A \in ℝ$
39	36 38	anim12ci	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M)) \to (A \in ℝ \land M \in ℝ^{+})$
40	39	3adant3	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to (A \in ℝ \land M \in ℝ^{+})$
41		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
42	41	anim1i	$⊢ (A \in ℕ_{0} \land A < M) \to (0 \leq A \land A < M)$
43	42	3ad2ant2	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to (0 \leq A \land A < M)$
44		modid	$⊢ ((A \in ℝ \land M \in ℝ^{+}) \land (0 \leq A \land A < M)) \to A \mod M = A$
45	40 43 44	syl2anc	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to A \mod M = A$
46	35 45	neeqtrd	$⊢ (M \in ℕ \land (A \in ℕ_{0} \land A < M) \land (B \in ℕ \land B < M)) \to (A + B) \mod M \neq A$

Metamath Proof Explorer

Theorem addmodne

Proof