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 N = 3 K
gpg3kgrtriex.g No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
gpg3kgrtriex.e E = 1 K mod N 1 K mod N
Assertion gpg3kgrtriexlem6 K E Edg G

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n N = 3 K
2 gpg3kgrtriex.g Could not format G = ( N gPetersenGr K ) : No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
3 gpg3kgrtriex.e E = 1 K mod N 1 K mod N
4 nnz K K
5 3nn 3
6 5 a1i K 3
7 id K K
8 6 7 nnmulcld K 3 K
9 1 8 eqeltrid K N
10 zmodfzo K N K mod N 0 ..^ N
11 4 9 10 syl2anc K K mod N 0 ..^ N
12 opeq2 x = K mod N 0 x = 0 K mod N
13 oveq1 x = K mod N x + 1 = K mod N + 1
14 13 oveq1d x = K mod N x + 1 mod N = K mod N + 1 mod N
15 14 opeq2d x = K mod N 0 x + 1 mod N = 0 K mod N + 1 mod N
16 12 15 preq12d x = K mod N 0 x 0 x + 1 mod N = 0 K mod N 0 K mod N + 1 mod N
17 16 eqeq2d x = K mod N E = 0 x 0 x + 1 mod N E = 0 K mod N 0 K mod N + 1 mod N
18 opeq2 x = K mod N 1 x = 1 K mod N
19 12 18 preq12d x = K mod N 0 x 1 x = 0 K mod N 1 K mod N
20 19 eqeq2d x = K mod N E = 0 x 1 x E = 0 K mod N 1 K mod N
21 oveq1 x = K mod N x + K = K mod N + K
22 21 oveq1d x = K mod N x + K mod N = K mod N + K mod N
23 22 opeq2d x = K mod N 1 x + K mod N = 1 K mod N + K mod N
24 18 23 preq12d x = K mod N 1 x 1 x + K mod N = 1 K mod N 1 K mod N + K mod N
25 24 eqeq2d x = K mod N E = 1 x 1 x + K mod N E = 1 K mod N 1 K mod N + K mod N
26 17 20 25 3orbi123d x = K mod N E = 0 x 0 x + 1 mod N E = 0 x 1 x E = 1 x 1 x + K mod N E = 0 K mod N 0 K mod N + 1 mod N E = 0 K mod N 1 K mod N E = 1 K mod N 1 K mod N + K mod N
27 26 adantl K x = K mod N E = 0 x 0 x + 1 mod N E = 0 x 1 x E = 1 x 1 x + K mod N E = 0 K mod N 0 K mod N + 1 mod N E = 0 K mod N 1 K mod N E = 1 K mod N 1 K mod N + K mod N
28 1 gpg3kgrtriexlem2 K K mod N = K mod N + K mod N
29 28 opeq2d K 1 K mod N = 1 K mod N + K mod N
30 29 preq2d K 1 K mod N 1 K mod N = 1 K mod N 1 K mod N + K mod N
31 3 30 eqtrid K E = 1 K mod N 1 K mod N + K mod N
32 31 3mix3d K E = 0 K mod N 0 K mod N + 1 mod N E = 0 K mod N 1 K mod N E = 1 K mod N 1 K mod N + K mod N
33 11 27 32 rspcedvd K x 0 ..^ N E = 0 x 0 x + 1 mod N E = 0 x 1 x E = 1 x 1 x + K mod N
34 3z 3
35 34 a1i K 3
36 35 4 zmulcld K 3 K
37 3t1e3 3 1 = 3
38 nnge1 K 1 K
39 1red K 1
40 nnre K K
41 3re 3
42 3pos 0 < 3
43 41 42 pm3.2i 3 0 < 3
44 43 a1i K 3 0 < 3
45 lemul2 1 K 3 0 < 3 1 K 3 1 3 K
46 39 40 44 45 syl3anc K 1 K 3 1 3 K
47 38 46 mpbid K 3 1 3 K
48 37 47 eqbrtrrid K 3 3 K
49 eluz2 3 K 3 3 3 K 3 3 K
50 35 36 48 49 syl3anbrc K 3 K 3
51 1 50 eqeltrid K N 3
52 41 a1i K 3
53 52 40 remulcld K 3 K
54 1 53 eqeltrid K N
55 54 rehalfcld K N 2
56 55 ceilcld K N 2
57 56 zred K N 2
58 53 rehalfcld K 3 K 2
59 58 ceilcld K 3 K 2
60 59 zred K 3 K 2
61 gpg3kgrtriexlem1 K K < 3 K 2
62 40 60 61 ltled K K 3 K 2
63 1 oveq1i N 2 = 3 K 2
64 63 fveq2i N 2 = 3 K 2
65 62 64 breqtrrdi K K N 2
66 39 40 57 38 65 letrd K 1 N 2
67 elnnz1 N 2 N 2 1 N 2
68 56 66 67 sylanbrc K N 2
69 61 64 breqtrrdi K K < N 2
70 elfzo1 K 1 ..^ N 2 K N 2 K < N 2
71 7 68 69 70 syl3anbrc K K 1 ..^ N 2
72 eqid 0 ..^ N = 0 ..^ N
73 eqid 1 ..^ N 2 = 1 ..^ N 2
74 eqid Edg G = Edg G
75 72 73 2 74 gpgedgel N 3 K 1 ..^ N 2 E Edg G x 0 ..^ N E = 0 x 0 x + 1 mod N E = 0 x 1 x E = 1 x 1 x + K mod N
76 51 71 75 syl2anc K E Edg G x 0 ..^ N E = 0 x 0 x + 1 mod N E = 0 x 1 x E = 1 x 1 x + K mod N
77 33 76 mpbird K E Edg G