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 47931

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 12839	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘5) ↔ (5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
2		4nn0 12494	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
3	2	a1i 11	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ ℕ₀)
4		simp2 1149	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℤ)
5		0red 11178	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 ∈ ℝ)
6		5re 12299	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ
7	6	a1i 11	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 5 ∈ ℝ)
8		zre 12566	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
9	8	3ad2ant2 1146	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℝ)
10		5pos 12324	. . . . . . . . . . . . . 14 ⊢ 0 < 5
11	10	a1i 11	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 < 5)
12		simp3 1150	. . . . . . . . . . . . 13 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 5 ≤ 𝑁)
13	5, 7, 9, 11, 12	ltletrd 11337	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 0 < 𝑁)
14		elnnz 12572	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
15	4, 13, 14	sylanbrc 592	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 𝑁 ∈ ℕ)
16		4re 12296	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℝ
17	16	a1i 11	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ ℝ)
18		4lt5 12391	. . . . . . . . . . . . 13 ⊢ 4 < 5
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 < 5)
20	17, 7, 9, 19, 12	ltletrd 11337	. . . . . . . . . . 11 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 < 𝑁)
21		elfzo0 13700	. . . . . . . . . . 11 ⊢ (4 ∈ (0..^𝑁) ↔ (4 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 4 < 𝑁))
22	3, 15, 20, 21	syl3anbrc 1356	. . . . . . . . . 10 ⊢ ((5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁) → 4 ∈ (0..^𝑁))
23	1, 22	sylbi 219	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 4 ∈ (0..^𝑁))
24		zmodidfzoimp 13905	. . . . . . . . 9 ⊢ (4 ∈ (0..^𝑁) → (4 mod 𝑁) = 4)
25	23, 24	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → (4 mod 𝑁) = 4)
26		4ne0 12323	. . . . . . . . 9 ⊢ 4 ≠ 0
27	26	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 4 ≠ 0)
28	25, 27	eqnetrd 3023	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘5) → (4 mod 𝑁) ≠ 0)
29		df-ne 2957	. . . . . . . 8 ⊢ (((4 · 1) mod 𝑁) ≠ 0 ↔ ¬ ((4 · 1) mod 𝑁) = 0)
30		4cn 12297	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
31	30	mulridi 11180	. . . . . . . . . 10 ⊢ (4 · 1) = 4
32	31	oveq1i 7401	. . . . . . . . 9 ⊢ ((4 · 1) mod 𝑁) = (4 mod 𝑁)
33	32	neeq1i 3020	. . . . . . . 8 ⊢ (((4 · 1) mod 𝑁) ≠ 0 ↔ (4 mod 𝑁) ≠ 0)
34	29, 33	bitr3i 279	. . . . . . 7 ⊢ (¬ ((4 · 1) mod 𝑁) = 0 ↔ (4 mod 𝑁) ≠ 0)
35	28, 34	sylibr 236	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘5) → ¬ ((4 · 1) mod 𝑁) = 0)
36	35	3ad2ant1 1145	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → ¬ ((4 · 1) mod 𝑁) = 0)
37	36	adantr 484	. . . 4 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ¬ ((4 · 1) mod 𝑁) = 0)
38		uzuzle35 12882	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 𝑁 ∈ (ℤ_≥‘3))
39		eluz3nn 12884	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
40	38, 39	syl 17	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 𝑁 ∈ ℕ)
41	40	3ad2ant1 1145	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑁 ∈ ℕ)
42		elfzoelz 13658	. . . . . . . 8 ⊢ (𝑋 ∈ (0..^𝑁) → 𝑋 ∈ ℤ)
43		modm1nep1.i	. . . . . . . 8 ⊢ 𝐼 = (0..^𝑁)
44	42, 43	eleq2s 2879	. . . . . . 7 ⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ ℤ)
45	44	3ad2ant2 1146	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑋 ∈ ℤ)
46		elfzoelz 13658	. . . . . . . 8 ⊢ (𝑌 ∈ (0..^𝑁) → 𝑌 ∈ ℤ)
47	46, 43	eleq2s 2879	. . . . . . 7 ⊢ (𝑌 ∈ 𝐼 → 𝑌 ∈ ℤ)
48	47	3ad2ant3 1147	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 𝑌 ∈ ℤ)
49		1zzd 12596	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → 1 ∈ ℤ)
50		modmkpkne 47922	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 1 ∈ ℤ)) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0)))
51	41, 45, 48, 49, 50	syl13anc 1390	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0)))
52	51	imp 410	. . . 4 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → (((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁) ↔ ((4 · 1) mod 𝑁) = 0))
53	37, 52	mtbird 327	. . 3 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ¬ ((𝑌 + 1) mod 𝑁) = ((𝑋 − 1) mod 𝑁))
54	53	neqned 2963	. 2 ⊢ (((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ ((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁)) → ((𝑌 + 1) mod 𝑁) ≠ ((𝑋 − 1) mod 𝑁))
55	54	ex 416	1 ⊢ ((𝑁 ∈ (ℤ_≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → ((𝑌 + 1) mod 𝑁) ≠ ((𝑋 − 1) mod 𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 class class class wbr 5097 ‘cfv 6516 (class class class)co 7391 ℝcr 11066 0cc0 11067 1c1 11068 + caddc 11070 · cmul 11072 < clt 11210 ≤ cle 11211 − cmin 11408 ℕcn 12204 3c3 12267 4c4 12268 5c5 12269 ℕ₀cn0 12475 ℤcz 12562 ℤ_≥cuz 12833 ..^cfzo 13653 mod cmo 13873

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-er 8672 df-en 8922 df-dom 8923 df-sdom 8924 df-sup 9382 df-inf 9383 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-n0 12476 df-z 12563 df-uz 12834 df-rp 12988 df-fz 13507 df-fzo 13654 df-fl 13796 df-mod 13874 df-dvds 16278

This theorem is referenced by: gpgedg2ov 48649

W3C validator