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 48554

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 12978	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘5) ↔ (5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
2		4nn0 12632	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
3	2	a1i 11	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ ℕ₀)
4		simp2 1155	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℤ)
5		0red 11318	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 ∈ ℝ)
6		5re 12437	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ
7	6	a1i 11	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 5 ∈ ℝ)
8		zre 12704	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
9	8	3ad2ant2 1152	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℝ)
10		5pos 12462	. . . . . . . . . . . . . 14 ⊢ 0 < 5
11	10	a1i 11	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 < 5)
12		simp3 1156	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 5 ≤ 𝑁)
13	5, 7, 9, 11, 12	ltletrd 11477	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 < 𝑁)
14		elnnz 12710	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
15	4, 13, 14	sylanbrc 595	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℕ)
16		4re 12434	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℝ
17	16	a1i 11	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ ℝ)
18		4lt5 12529	. . . . . . . . . . . . 13 ⊢ 4 < 5
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 < 5)
20	17, 7, 9, 19, 12	ltletrd 11477	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 < 𝑁)
21		elfzo0 13842	. . . . . . . . . . 11 ⊢ (4 ∈ (0..^𝑁) ↔ (4 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 4 < 𝑁))
22	3, 15, 20, 21	syl3anbrc 1362	. . . . . . . . . 10 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ (0..^𝑁))
23	1, 22	sylbi 220	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 4 ∈ (0..^𝑁))
24		zmodidfzoimp 14048	. . . . . . . . 9 ⊢ (4 ∈ (0..^𝑁) → (4 mod 𝑁) = 4)
25	23, 24	syl 18	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → (4 mod 𝑁) = 4)
26		4ne0 12461	. . . . . . . . 9 ⊢ 4 ≠ 0
27	26	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 4 ≠ 0)
28	25, 27	eqnetrd 3022	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘5) → (4 mod 𝑁) ≠ 0)
29		df-ne 2956	. . . . . . . 8 ⊢ (((4 · 1) mod 𝑁) ≠ 0 ↔ ¬ ((4 · 1) mod 𝑁) = 0)
30		4cn 12435	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
31	30	mulridi 11320	. . . . . . . . . 10 ⊢ (4 · 1) = 4
32	31	oveq1i 7434	. . . . . . . . 9 ⊢ ((4 · 1) mod 𝑁) = (4 mod 𝑁)
33	32	neeq1i 3019	. . . . . . . 8 ⊢ (((4 · 1) mod 𝑁) ≠ 0 ↔ (4 mod 𝑁) ≠ 0)
34	29, 33	bitr3i 280	. . . . . . 7 ⊢ (¬ ((4 · 1) mod 𝑁) = 0 ↔ (4 mod 𝑁) ≠ 0)
35	28, 34	sylibr 237	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘5) → ¬ ((4 · 1) mod 𝑁) = 0)
36	35	3ad2ant1 1151	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → ¬ ((4 · 1) mod 𝑁) = 0)
37	36	adantr 486	. . . 4 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ¬ ((4 · 1) mod 𝑁) = 0)
38		uzuzle35 13021	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 𝑁 ∈ (ℤ_≥‘3))
39		eluz3nn 13023	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
40	38, 39	syl 18	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 𝑁 ∈ ℕ)
41	40	3ad2ant1 1151	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑁 ∈ ℕ)
42		elfzoelz 13800	. . . . . . . 8 ⊢ (𝑋 ∈ (0..^𝑁) → 𝑋 ∈ ℤ)
43		modm1nep1.i	. . . . . . . 8 ⊢ 𝐼 = (0..^𝑁)
44	42, 43	eleq2s 2878	. . . . . . 7 ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ ℤ)
45	44	3ad2ant2 1152	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑋 ∈ ℤ)
46		elfzoelz 13800	. . . . . . . 8 ⊢ (𝑌 ∈ (0..^𝑁) → 𝑌 ∈ ℤ)
47	46, 43	eleq2s 2878	. . . . . . 7 ⊢ (𝑌 ∈ 𝐼 → 𝑌 ∈ ℤ)
48	47	3ad2ant3 1153	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑌 ∈ ℤ)
49		1zzd 12734	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 1 ∈ ℤ)
50		modmkpkne 48545	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 1 ∈ ℤ)) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0)))
51	41, 45, 48, 49, 50	syl13anc 1399	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0)))
52	51	imp 412	. . . 4 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0))
53	37, 52	mtbird 328	. . 3 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ¬ ((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁))
54	53	neqned 2962	. 2 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ((𝑌 + 1) mod 𝑁) ≠ ((𝑋 − 1) mod 𝑁))
55	54	ex 418	1 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → ((𝑌 + 1) mod 𝑁) ≠ ((𝑋 − 1) mod 𝑁)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 ‘cfv 6543 (class class class)co 7424 ℝcr 11206 0cc0 11207 1c1 11208 + caddc 11210 · cmul 11212 < clt 11350 ≤ cle 11351 − cmin 11548 ℕcn 12342 3c3 12405 4c4 12406 5c5 12407 ℕ₀cn0 12613 ℤcz 12700 ℤ_≥cuz 12972 ..^cfzo 13795 mod cmo 14016

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-pre-sup 11285

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7882 df-1st 8005 df-2nd 8006 df-frecs 8306 df-wrecs 8337 df-recs 8386 df-rdg 8425 df-er 8724 df-en 8981 df-dom 8982 df-sdom 8983 df-sup 9441 df-inf 9442 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-div 11981 df-nn 12343 df-2 12412 df-3 12413 df-4 12414 df-5 12415 df-n0 12614 df-z 12701 df-uz 12973 df-rp 13128 df-fz 13647 df-fzo 13796 df-fl 13939 df-mod 14017 df-dvds 16432

This theorem is used by: gpgedg2ov 49272

W3C validator