Theorem 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	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝑀 ) ≠ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2	1	a1i	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 2 ∈ ℤ )
3		nnz	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
4	3	adantr	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝑀 ∈ ℤ )
5		1red	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 1 ∈ ℝ )
6		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
7	6	ad2antrl	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝐵 ∈ ℝ )
8		nnre	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
9	8	adantr	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝑀 ∈ ℝ )
10		nnge1	⊢ ( 𝐵 ∈ ℕ → 1 ≤ 𝐵 )
11	10	ad2antrl	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 1 ≤ 𝐵 )
12		simprr	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝐵 < 𝑀 )
13	5 7 9 11 12	lelttrd	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 1 < 𝑀 )
14		1zzd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) → 1 ∈ ℤ )
15		zltp1le	⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 1 < 𝑀 ↔ ( 1 + 1 ) ≤ 𝑀 ) )
16	14 3 15	syl2anr	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 1 < 𝑀 ↔ ( 1 + 1 ) ≤ 𝑀 ) )
17		1p1e2	⊢ ( 1 + 1 ) = 2
18	17	breq1i	⊢ ( ( 1 + 1 ) ≤ 𝑀 ↔ 2 ≤ 𝑀 )
19	16 18	bitrdi	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 1 < 𝑀 ↔ 2 ≤ 𝑀 ) )
20	13 19	mpbid	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 2 ≤ 𝑀 )
21	2 4 20	3jca	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 2 ≤ 𝑀 ) )
22	21	3adant2	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 2 ≤ 𝑀 ) )
23		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 2 ≤ 𝑀 ) )
24	22 23	sylibr	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
25		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
26	25	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) → 𝐴 ∈ ℤ )
27	26	3ad2ant2	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝐴 ∈ ℤ )
28		simprl	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝐵 ∈ ℕ )
29		simpl	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝑀 ∈ ℕ )
30	28 29 12	3jca	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 𝐵 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝐵 < 𝑀 ) )
31	30	3adant2	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 𝐵 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝐵 < 𝑀 ) )
32		elfzo1	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝐵 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝐵 < 𝑀 ) )
33	31 32	sylibr	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → 𝐵 ∈ ( 1 ..^ 𝑀 ) )
34		zplusmodne	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 1 ..^ 𝑀 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝑀 ) ≠ ( 𝐴 mod 𝑀 ) )
35	24 27 33 34	syl3anc	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝑀 ) ≠ ( 𝐴 mod 𝑀 ) )
36		nnrp	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ+ )
37		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
38	37	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) → 𝐴 ∈ ℝ )
39	36 38	anim12ci	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ) → ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
40	39	3adant3	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
41		nn0ge0	⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
42	41	anim1i	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) → ( 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) )
43	42	3ad2ant2	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) )
44		modid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( 𝐴 mod 𝑀 ) = 𝐴 )
45	40 43 44	syl2anc	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( 𝐴 mod 𝑀 ) = 𝐴 )
46	35 45	neeqtrd	⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀 ) ∧ ( 𝐵 ∈ ℕ ∧ 𝐵 < 𝑀 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝑀 ) ≠ 𝐴 )