gpg3nbgrvtxlem

Description: Lemma for gpg3nbgrvtx0ALT and gpg3nbgrvtx1 . For this theorem, it is essential that 2 < N and K < ( N / 2 ) ! (Contributed by AV, 3-Sep-2025) (Proof shortened by AV, 9-Sep-2025)

		Ref	Expression
	Assertion	gpg3nbgrvtxlem	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉) \land A \in (0 ..^N)) \to (A + K) \mod N \neq (A - K) \mod N$

Proof

Step	Hyp	Ref	Expression
1		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
2	1	3ad2ant1	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉) \land A \in (0 ..^N)) \to N \in ℕ$
3		elfzoelz	$⊢ A \in (0 ..^N) \to A \in ℤ$
4	3	3ad2ant3	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉) \land A \in (0 ..^N)) \to A \in ℤ$
5		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
6	5	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉) \land A \in (0 ..^N)) \to K \in ℤ$
7	5	zcnd	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℂ$
8		2times	$⊢ K \in ℂ \to 2 K = K + K$
9	8	eqcomd	$⊢ K \in ℂ \to K + K = 2 K$
10	7 9	syl	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K + K = 2 K$
11	10	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to K + K = 2 K$
12		1red	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to 1 \in ℝ$
13	5	zred	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℝ$
14		2z	$⊢ 2 \in ℤ$
15	14	a1i	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to 2 \in ℤ$
16	15 5	zmulcld	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to 2 K \in ℤ$
17	16	zred	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to 2 K \in ℝ$
18		elfzole1	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to 1 \leq K$
19		elfzo1	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \leftrightarrow (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉)$
20	19	simp1bi	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℕ$
21	20	nnnn0d	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℕ_{0}$
22		nn0le2x	$⊢ K \in ℕ_{0} \to K \leq 2 K$
23	21 22	syl	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \leq 2 K$
24	12 13 17 18 23	letrd	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to 1 \leq 2 K$
25	24	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to 1 \leq 2 K$
26		2tceilhalfelfzo1	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to 2 K < N$
27	25 26	jca	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to (1 \leq 2 K \land 2 K < N)$
28		breq2	$⊢ K + K = 2 K \to (1 \leq K + K \leftrightarrow 1 \leq 2 K)$
29		breq1	$⊢ K + K = 2 K \to (K + K < N \leftrightarrow 2 K < N)$
30	28 29	anbi12d	$⊢ K + K = 2 K \to ((1 \leq K + K \land K + K < N) \leftrightarrow (1 \leq 2 K \land 2 K < N))$
31	27 30	syl5ibrcom	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to (K + K = 2 K \to (1 \leq K + K \land K + K < N))$
32	11 31	mpd	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to (1 \leq K + K \land K + K < N)$
33	32	3adant3	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉) \land A \in (0 ..^N)) \to (1 \leq K + K \land K + K < N)$
34		submodneaddmod	$⊢ (N \in ℕ \land (A \in ℤ \land K \in ℤ \land K \in ℤ) \land (1 \leq K + K \land K + K < N)) \to (A + K) \mod N \neq (A - K) \mod N$
35	2 4 6 6 33 34	syl131anc	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉) \land A \in (0 ..^N)) \to (A + K) \mod N \neq (A - K) \mod N$

Metamath Proof Explorer

Theorem gpg3nbgrvtxlem

Proof