Metamath Proof Explorer

Theorem 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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 + 𝐾 ) mod 𝑁 ) ≠ ( ( 𝐴 − 𝐾 ) mod 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eluzge3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
2 1 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ )
3 elfzoelz ⊢ ( 𝐴 ∈ ( 0 ..^ 𝑁 ) → 𝐴 ∈ ℤ )
4 3 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℤ )
5 elfzoelz ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
6 5 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → 𝐾 ∈ ℤ )
7 5 zcnd ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℂ )
8 2times ⊢ ( 𝐾 ∈ ℂ → ( 2 · 𝐾 ) = ( 𝐾 + 𝐾 ) )
9 8 eqcomd ⊢ ( 𝐾 ∈ ℂ → ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) )
10 7 9 syl ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) )
11 10 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) )
12 1red ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 1 ∈ ℝ )
13 5 zred ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℝ )
14 2z ⊢ 2 ∈ ℤ
15 14 a1i ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 2 ∈ ℤ )
16 15 5 zmulcld ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → ( 2 · 𝐾 ) ∈ ℤ )
17 16 zred ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → ( 2 · 𝐾 ) ∈ ℝ )
18 elfzole1 ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 1 ≤ 𝐾 )
19 elfzo1 ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
20 19 simp1bi ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℕ )
21 20 nnnn0d ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℕ0 )
22 nn0le2x ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ≤ ( 2 · 𝐾 ) )
23 21 22 syl ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ≤ ( 2 · 𝐾 ) )
24 12 13 17 18 23 letrd ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 1 ≤ ( 2 · 𝐾 ) )
25 24 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → 1 ≤ ( 2 · 𝐾 ) )
26 2tceilhalfelfzo1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 2 · 𝐾 ) < 𝑁 )
27 25 26 jca ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 1 ≤ ( 2 · 𝐾 ) ∧ ( 2 · 𝐾 ) < 𝑁 ) )
28 breq2 ⊢ ( ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) → ( 1 ≤ ( 𝐾 + 𝐾 ) ↔ 1 ≤ ( 2 · 𝐾 ) ) )
29 breq1 ⊢ ( ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) → ( ( 𝐾 + 𝐾 ) < 𝑁 ↔ ( 2 · 𝐾 ) < 𝑁 ) )
30 28 29 anbi12d ⊢ ( ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) → ( ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) ↔ ( 1 ≤ ( 2 · 𝐾 ) ∧ ( 2 · 𝐾 ) < 𝑁 ) ) )
31 27 30 syl5ibrcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) → ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) ) )
32 11 31 mpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) )
33 32 3adant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) )
34 submodneaddmod ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) ) → ( ( 𝐴 + 𝐾 ) mod 𝑁 ) ≠ ( ( 𝐴 − 𝐾 ) mod 𝑁 ) )
35 2 4 6 6 33 34 syl131anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 + 𝐾 ) mod 𝑁 ) ≠ ( ( 𝐴 − 𝐾 ) mod 𝑁 ) )