Metamath Proof Explorer

Theorem gpg3kgrtriexlem6

Description: Lemma 6 for gpg3kgrtriex : E is an edge in the generalized Petersen graph G(N,K) with N = 3 x. K . (Contributed by AV, 1-Oct-2025)

Ref Expression
Hypotheses gpg3kgrtriex.n ⊢ 𝑁 = ( 3 · 𝐾 )
gpg3kgrtriex.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
gpg3kgrtriex.e ⊢ 𝐸 = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ }
Assertion gpg3kgrtriexlem6 ( 𝐾 ∈ ℕ → 𝐸 ∈ ( Edg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n ⊢ 𝑁 = ( 3 · 𝐾 )
2 gpg3kgrtriex.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3 gpg3kgrtriex.e ⊢ 𝐸 = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ }
4 nnz ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
5 3nn ⊢ 3 ∈ ℕ
6 5 a1i ⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℕ )
7 id ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ )
8 6 7 nnmulcld ⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ℕ )
9 1 8 eqeltrid ⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ℕ )
10 zmodfzo ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
11 4 9 10 syl2anc ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
12 opeq2 ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ⟨ 0 , 𝑥 ⟩ = ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ )
13 oveq1 ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ( 𝑥 + 1 ) = ( ( 𝐾 mod 𝑁 ) + 1 ) )
14 13 oveq1d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ( ( 𝑥 + 1 ) mod 𝑁 ) = ( ( ( 𝐾 mod 𝑁 ) + 1 ) mod 𝑁 ) )
15 14 opeq2d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 𝐾 mod 𝑁 ) + 1 ) mod 𝑁 ) ⟩ )
16 12 15 preq12d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 𝐾 mod 𝑁 ) + 1 ) mod 𝑁 ) ⟩ } )
17 16 eqeq2d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ( 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ 𝐸 = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 𝐾 mod 𝑁 ) + 1 ) mod 𝑁 ) ⟩ } ) )
18 opeq2 ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ )
19 12 18 preq12d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ } )
20 19 eqeq2d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ( 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ 𝐸 = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ } ) )
21 oveq1 ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ( 𝑥 + 𝐾 ) = ( ( 𝐾 mod 𝑁 ) + 𝐾 ) )
22 21 oveq1d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ( ( 𝑥 + 𝐾 ) mod 𝑁 ) = ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) )
23 22 opeq2d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ )
24 18 23 preq12d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
25 24 eqeq2d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ( 𝐸 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ 𝐸 = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) )
26 17 20 25 3orbi123d ⊢ ( 𝑥 = ( 𝐾 mod 𝑁 ) → ( ( 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝐸 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( 𝐸 = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 𝐾 mod 𝑁 ) + 1 ) mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
27 26 adantl ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑥 = ( 𝐾 mod 𝑁 ) ) → ( ( 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝐸 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( 𝐸 = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 𝐾 mod 𝑁 ) + 1 ) mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
28 1 gpg3kgrtriexlem2 ⊢ ( 𝐾 ∈ ℕ → ( - 𝐾 mod 𝑁 ) = ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) )
29 28 opeq2d ⊢ ( 𝐾 ∈ ℕ → ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ )
30 29 preq2d ⊢ ( 𝐾 ∈ ℕ → { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
31 3 30 eqtrid ⊢ ( 𝐾 ∈ ℕ → 𝐸 = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
32 31 3mix3d ⊢ ( 𝐾 ∈ ℕ → ( 𝐸 = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 0 , ( ( ( 𝐾 mod 𝑁 ) + 1 ) mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 0 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 𝐾 mod 𝑁 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) )
33 11 27 32 rspcedvd ⊢ ( 𝐾 ∈ ℕ → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝐸 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
34 3z ⊢ 3 ∈ ℤ
35 34 a1i ⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℤ )
36 35 4 zmulcld ⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ℤ )
37 3t1e3 ⊢ ( 3 · 1 ) = 3
38 nnge1 ⊢ ( 𝐾 ∈ ℕ → 1 ≤ 𝐾 )
39 1red ⊢ ( 𝐾 ∈ ℕ → 1 ∈ ℝ )
40 nnre ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
41 3re ⊢ 3 ∈ ℝ
42 3pos ⊢ 0 < 3
43 41 42 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 0 < 3 )
44 43 a1i ⊢ ( 𝐾 ∈ ℕ → ( 3 ∈ ℝ ∧ 0 < 3 ) )
45 lemul2 ⊢ ( ( 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( 1 ≤ 𝐾 ↔ ( 3 · 1 ) ≤ ( 3 · 𝐾 ) ) )
46 39 40 44 45 syl3anc ⊢ ( 𝐾 ∈ ℕ → ( 1 ≤ 𝐾 ↔ ( 3 · 1 ) ≤ ( 3 · 𝐾 ) ) )
47 38 46 mpbid ⊢ ( 𝐾 ∈ ℕ → ( 3 · 1 ) ≤ ( 3 · 𝐾 ) )
48 37 47 eqbrtrrid ⊢ ( 𝐾 ∈ ℕ → 3 ≤ ( 3 · 𝐾 ) )
49 eluz2 ⊢ ( ( 3 · 𝐾 ) ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ ( 3 · 𝐾 ) ∈ ℤ ∧ 3 ≤ ( 3 · 𝐾 ) ) )
50 35 36 48 49 syl3anbrc ⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ( ℤ≥ ‘ 3 ) )
51 1 50 eqeltrid ⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
52 41 a1i ⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℝ )
53 52 40 remulcld ⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ℝ )
54 1 53 eqeltrid ⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ℝ )
55 54 rehalfcld ⊢ ( 𝐾 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℝ )
56 55 ceilcld ⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
57 56 zred ⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
58 53 rehalfcld ⊢ ( 𝐾 ∈ ℕ → ( ( 3 · 𝐾 ) / 2 ) ∈ ℝ )
59 58 ceilcld ⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) ∈ ℤ )
60 59 zred ⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) ∈ ℝ )
61 gpg3kgrtriexlem1 ⊢ ( 𝐾 ∈ ℕ → 𝐾 < ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) )
62 40 60 61 ltled ⊢ ( 𝐾 ∈ ℕ → 𝐾 ≤ ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) )
63 1 oveq1i ⊢ ( 𝑁 / 2 ) = ( ( 3 · 𝐾 ) / 2 )
64 63 fveq2i ⊢ ( ⌈ ‘ ( 𝑁 / 2 ) ) = ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) )
65 62 64 breqtrrdi ⊢ ( 𝐾 ∈ ℕ → 𝐾 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
66 39 40 57 38 65 letrd ⊢ ( 𝐾 ∈ ℕ → 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
67 elnnz1 ⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ↔ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
68 56 66 67 sylanbrc ⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ )
69 61 64 breqtrrdi ⊢ ( 𝐾 ∈ ℕ → 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) )
70 elfzo1 ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
71 7 68 69 70 syl3anbrc ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
72 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
73 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
74 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
75 72 73 2 74 gpgedgel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝐸 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
76 51 71 75 syl2anc ⊢ ( 𝐾 ∈ ℕ → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝐸 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝐸 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
77 33 76 mpbird ⊢ ( 𝐾 ∈ ℕ → 𝐸 ∈ ( Edg ‘ 𝐺 ) )