modm1p1ne - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > modm1p1ne		Structured version Visualization version GIF version

Theorem modm1p1ne 47532

Description: If an integer minus one equals another integer plus one modulo an integer greater than 4, then the first integer plus one is not equal to the second integer minus one modulo the same modulus. (Contributed by AV, 15-Nov-2025.)

**Hypothesis**
Ref	Expression
modm1nep1.i	⊢ 𝐼 = (0..^𝑁)

**Assertion**
Ref	Expression
modm1p1ne	⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → ((𝑌 + 1) mod 𝑁) ≠ ((𝑋 − 1) mod 𝑁)))

**Proof of Theorem modm1p1ne**
Step	Hyp	Ref	Expression
1		eluz2 12748	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘5) ↔ (5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
2		4nn0 12411	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
3	2	a1i 11	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ ℕ₀)
4		simp2 1137	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℤ)
5		0red 11126	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 ∈ ℝ)
6		5re 12223	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ
7	6	a1i 11	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 5 ∈ ℝ)
8		zre 12483	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
9	8	3ad2ant2 1134	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℝ)
10		5pos 12245	. . . . . . . . . . . . . 14 ⊢ 0 < 5
11	10	a1i 11	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 < 5)
12		simp3 1138	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 5 ≤ 𝑁)
13	5, 7, 9, 11, 12	ltletrd 11284	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 < 𝑁)
14		elnnz 12489	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
15	4, 13, 14	sylanbrc 583	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℕ)
16		4re 12220	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℝ
17	16	a1i 11	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ ℝ)
18		4lt5 12308	. . . . . . . . . . . . 13 ⊢ 4 < 5
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 < 5)
20	17, 7, 9, 19, 12	ltletrd 11284	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 < 𝑁)
21		elfzo0 13607	. . . . . . . . . . 11 ⊢ (4 ∈ (0..^𝑁) ↔ (4 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 4 < 𝑁))
22	3, 15, 20, 21	syl3anbrc 1344	. . . . . . . . . 10 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ (0..^𝑁))
23	1, 22	sylbi 217	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 4 ∈ (0..^𝑁))
24		zmodidfzoimp 13812	. . . . . . . . 9 ⊢ (4 ∈ (0..^𝑁) → (4 mod 𝑁) = 4)
25	23, 24	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → (4 mod 𝑁) = 4)
26		4ne0 12244	. . . . . . . . 9 ⊢ 4 ≠ 0
27	26	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 4 ≠ 0)
28	25, 27	eqnetrd 2996	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘5) → (4 mod 𝑁) ≠ 0)
29		df-ne 2930	. . . . . . . 8 ⊢ (((4 · 1) mod 𝑁) ≠ 0 ↔ ¬ ((4 · 1) mod 𝑁) = 0)
30		4cn 12221	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
31	30	mulridi 11127	. . . . . . . . . 10 ⊢ (4 · 1) = 4
32	31	oveq1i 7365	. . . . . . . . 9 ⊢ ((4 · 1) mod 𝑁) = (4 mod 𝑁)
33	32	neeq1i 2993	. . . . . . . 8 ⊢ (((4 · 1) mod 𝑁) ≠ 0 ↔ (4 mod 𝑁) ≠ 0)
34	29, 33	bitr3i 277	. . . . . . 7 ⊢ (¬ ((4 · 1) mod 𝑁) = 0 ↔ (4 mod 𝑁) ≠ 0)
35	28, 34	sylibr 234	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘5) → ¬ ((4 · 1) mod 𝑁) = 0)
36	35	3ad2ant1 1133	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → ¬ ((4 · 1) mod 𝑁) = 0)
37	36	adantr 480	. . . 4 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ¬ ((4 · 1) mod 𝑁) = 0)
38		uzuzle35 12791	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 𝑁 ∈ (ℤ_≥‘3))
39		eluz3nn 12793	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
40	38, 39	syl 17	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 𝑁 ∈ ℕ)
41	40	3ad2ant1 1133	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑁 ∈ ℕ)
42		elfzoelz 13566	. . . . . . . 8 ⊢ (𝑋 ∈ (0..^𝑁) → 𝑋 ∈ ℤ)
43		modm1nep1.i	. . . . . . . 8 ⊢ 𝐼 = (0..^𝑁)
44	42, 43	eleq2s 2851	. . . . . . 7 ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ ℤ)
45	44	3ad2ant2 1134	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑋 ∈ ℤ)
46		elfzoelz 13566	. . . . . . . 8 ⊢ (𝑌 ∈ (0..^𝑁) → 𝑌 ∈ ℤ)
47	46, 43	eleq2s 2851	. . . . . . 7 ⊢ (𝑌 ∈ 𝐼 → 𝑌 ∈ ℤ)
48	47	3ad2ant3 1135	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑌 ∈ ℤ)
49		1zzd 12513	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 1 ∈ ℤ)
50		modmkpkne 47523	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 1 ∈ ℤ)) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0)))
51	41, 45, 48, 49, 50	syl13anc 1374	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0)))
52	51	imp 406	. . . 4 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0))
53	37, 52	mtbird 325	. . 3 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ¬ ((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁))
54	53	neqned 2936	. 2 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ((𝑌 + 1) mod 𝑁) ≠ ((𝑋 − 1) mod 𝑁))
55	54	ex 412	1 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → ((𝑌 + 1) mod 𝑁) ≠ ((𝑋 − 1) mod 𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 class class class wbr 5095 ‘cfv 6489 (class class class)co 7355 ℝcr 11016 0cc0 11017 1c1 11018 + caddc 11020 · cmul 11022 < clt 11157 ≤ cle 11158 − cmin 11355 ℕcn 12136 3c3 12192 4c4 12193 5c5 12194 ℕ₀cn0 12392 ℤcz 12479 ℤ_≥cuz 12742 ..^cfzo 13561 mod cmo 13780

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094 ax-pre-sup 11095

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-om 7806 df-1st 7930 df-2nd 7931 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-er 8631 df-en 8880 df-dom 8881 df-sdom 8882 df-sup 9337 df-inf 9338 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-div 11786 df-nn 12137 df-2 12199 df-3 12200 df-4 12201 df-5 12202 df-n0 12393 df-z 12480 df-uz 12743 df-rp 12897 df-fz 13415 df-fzo 13562 df-fl 13703 df-mod 13781 df-dvds 16171

This theorem is referenced by: gpgedg2ov 48228

W3C validator