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 47344

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 12775	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘5) ↔ (5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
2		4nn0 12437	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
3	2	a1i 11	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ ℕ₀)
4		simp2 1137	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℤ)
5		0red 11153	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 ∈ ℝ)
6		5re 12249	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ
7	6	a1i 11	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 5 ∈ ℝ)
8		zre 12509	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
9	8	3ad2ant2 1134	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℝ)
10		5pos 12271	. . . . . . . . . . . . . 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 11310	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 < 𝑁)
14		elnnz 12515	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
15	4, 13, 14	sylanbrc 583	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℕ)
16		4re 12246	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℝ
17	16	a1i 11	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ ℝ)
18		4lt5 12334	. . . . . . . . . . . . 13 ⊢ 4 < 5
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 < 5)
20	17, 7, 9, 19, 12	ltletrd 11310	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 < 𝑁)
21		elfzo0 13637	. . . . . . . . . . 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 13839	. . . . . . . . 9 ⊢ (4 ∈ (0..^𝑁) → (4 mod 𝑁) = 4)
25	23, 24	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → (4 mod 𝑁) = 4)
26		4ne0 12270	. . . . . . . . 9 ⊢ 4 ≠ 0
27	26	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 4 ≠ 0)
28	25, 27	eqnetrd 2992	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘5) → (4 mod 𝑁) ≠ 0)
29		df-ne 2926	. . . . . . . 8 ⊢ (((4 · 1) mod 𝑁) ≠ 0 ↔ ¬ ((4 · 1) mod 𝑁) = 0)
30		4cn 12247	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
31	30	mulridi 11154	. . . . . . . . . 10 ⊢ (4 · 1) = 4
32	31	oveq1i 7379	. . . . . . . . 9 ⊢ ((4 · 1) mod 𝑁) = (4 mod 𝑁)
33	32	neeq1i 2989	. . . . . . . 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 12822	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 𝑁 ∈ (ℤ_≥‘3))
39		eluz3nn 12824	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
40	38, 39	syl 17	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 𝑁 ∈ ℕ)
41	40	3ad2ant1 1133	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑁 ∈ ℕ)
42		elfzoelz 13596	. . . . . . . 8 ⊢ (𝑋 ∈ (0..^𝑁) → 𝑋 ∈ ℤ)
43		modm1nep1.i	. . . . . . . 8 ⊢ 𝐼 = (0..^𝑁)
44	42, 43	eleq2s 2846	. . . . . . 7 ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ ℤ)
45	44	3ad2ant2 1134	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑋 ∈ ℤ)
46		elfzoelz 13596	. . . . . . . 8 ⊢ (𝑌 ∈ (0..^𝑁) → 𝑌 ∈ ℤ)
47	46, 43	eleq2s 2846	. . . . . . 7 ⊢ (𝑌 ∈ 𝐼 → 𝑌 ∈ ℤ)
48	47	3ad2ant3 1135	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑌 ∈ ℤ)
49		1zzd 12540	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 1 ∈ ℤ)
50		modmkpkne 47335	. . . . . 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 2932	. 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 1540 ∈ wcel 2109 ≠ wne 2925 class class class wbr 5102 ‘cfv 6499 (class class class)co 7369 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 · cmul 11049 < clt 11184 ≤ cle 11185 − cmin 11381 ℕcn 12162 3c3 12218 4c4 12219 5c5 12220 ℕ₀cn0 12418 ℤcz 12505 ℤ_≥cuz 12769 ..^cfzo 13591 mod cmo 13807

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-sup 9369 df-inf 9370 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-n0 12419 df-z 12506 df-uz 12770 df-rp 12928 df-fz 13445 df-fzo 13592 df-fl 13730 df-mod 13808 df-dvds 16199

This theorem is referenced by: gpgedg2ov 48030

W3C validator