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 x. K )
gpg3kgrtriex.g 
|- G = ( N gPetersenGr K )
gpg3kgrtriex.e 
|- E = { <. 1 , ( K mod N ) >. , <. 1 , ( -u K mod N ) >. }
Assertion gpg3kgrtriexlem6 
|- ( K e. NN -> E e. ( Edg ` G ) )

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n 
 |-  N = ( 3 x. K )
2 gpg3kgrtriex.g 
 |-  G = ( N gPetersenGr K )
3 gpg3kgrtriex.e 
 |-  E = { <. 1 , ( K mod N ) >. , <. 1 , ( -u K mod N ) >. }
4 nnz 
 |-  ( K e. NN -> K e. ZZ )
5 3nn 
 |-  3 e. NN
6 5 a1i 
 |-  ( K e. NN -> 3 e. NN )
7 id 
 |-  ( K e. NN -> K e. NN )
8 6 7 nnmulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. NN )
9 1 8 eqeltrid 
 |-  ( K e. NN -> N e. NN )
10 zmodfzo 
 |-  ( ( K e. ZZ /\ N e. NN ) -> ( K mod N ) e. ( 0 ..^ N ) )
11 4 9 10 syl2anc 
 |-  ( K e. NN -> ( K mod N ) e. ( 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 e. NN /\ 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 e. NN -> ( -u K mod N ) = ( ( ( K mod N ) + K ) mod N ) )
29 28 opeq2d 
 |-  ( K e. NN -> <. 1 , ( -u K mod N ) >. = <. 1 , ( ( ( K mod N ) + K ) mod N ) >. )
30 29 preq2d 
 |-  ( K e. NN -> { <. 1 , ( K mod N ) >. , <. 1 , ( -u K mod N ) >. } = { <. 1 , ( K mod N ) >. , <. 1 , ( ( ( K mod N ) + K ) mod N ) >. } )
31 3 30 eqtrid 
 |-  ( K e. NN -> E = { <. 1 , ( K mod N ) >. , <. 1 , ( ( ( K mod N ) + K ) mod N ) >. } )
32 31 3mix3d 
 |-  ( K e. NN -> ( 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 e. NN -> E. x e. ( 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 e. ZZ
35 34 a1i 
 |-  ( K e. NN -> 3 e. ZZ )
36 35 4 zmulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. ZZ )
37 3t1e3 
 |-  ( 3 x. 1 ) = 3
38 nnge1 
 |-  ( K e. NN -> 1 <_ K )
39 1red 
 |-  ( K e. NN -> 1 e. RR )
40 nnre 
 |-  ( K e. NN -> K e. RR )
41 3re 
 |-  3 e. RR
42 3pos 
 |-  0 < 3
43 41 42 pm3.2i 
 |-  ( 3 e. RR /\ 0 < 3 )
44 43 a1i 
 |-  ( K e. NN -> ( 3 e. RR /\ 0 < 3 ) )
45 lemul2 
 |-  ( ( 1 e. RR /\ K e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( 1 <_ K <-> ( 3 x. 1 ) <_ ( 3 x. K ) ) )
46 39 40 44 45 syl3anc 
 |-  ( K e. NN -> ( 1 <_ K <-> ( 3 x. 1 ) <_ ( 3 x. K ) ) )
47 38 46 mpbid 
 |-  ( K e. NN -> ( 3 x. 1 ) <_ ( 3 x. K ) )
48 37 47 eqbrtrrid 
 |-  ( K e. NN -> 3 <_ ( 3 x. K ) )
49 eluz2 
 |-  ( ( 3 x. K ) e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ ( 3 x. K ) e. ZZ /\ 3 <_ ( 3 x. K ) ) )
50 35 36 48 49 syl3anbrc 
 |-  ( K e. NN -> ( 3 x. K ) e. ( ZZ>= ` 3 ) )
51 1 50 eqeltrid 
 |-  ( K e. NN -> N e. ( ZZ>= ` 3 ) )
52 41 a1i 
 |-  ( K e. NN -> 3 e. RR )
53 52 40 remulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. RR )
54 1 53 eqeltrid 
 |-  ( K e. NN -> N e. RR )
55 54 rehalfcld 
 |-  ( K e. NN -> ( N / 2 ) e. RR )
56 55 ceilcld 
 |-  ( K e. NN -> ( |^ ` ( N / 2 ) ) e. ZZ )
57 56 zred 
 |-  ( K e. NN -> ( |^ ` ( N / 2 ) ) e. RR )
58 53 rehalfcld 
 |-  ( K e. NN -> ( ( 3 x. K ) / 2 ) e. RR )
59 58 ceilcld 
 |-  ( K e. NN -> ( |^ ` ( ( 3 x. K ) / 2 ) ) e. ZZ )
60 59 zred 
 |-  ( K e. NN -> ( |^ ` ( ( 3 x. K ) / 2 ) ) e. RR )
61 gpg3kgrtriexlem1 
 |-  ( K e. NN -> K < ( |^ ` ( ( 3 x. K ) / 2 ) ) )
62 40 60 61 ltled 
 |-  ( K e. NN -> K <_ ( |^ ` ( ( 3 x. K ) / 2 ) ) )
63 1 oveq1i 
 |-  ( N / 2 ) = ( ( 3 x. K ) / 2 )
64 63 fveq2i 
 |-  ( |^ ` ( N / 2 ) ) = ( |^ ` ( ( 3 x. K ) / 2 ) )
65 62 64 breqtrrdi 
 |-  ( K e. NN -> K <_ ( |^ ` ( N / 2 ) ) )
66 39 40 57 38 65 letrd 
 |-  ( K e. NN -> 1 <_ ( |^ ` ( N / 2 ) ) )
67 elnnz1 
 |-  ( ( |^ ` ( N / 2 ) ) e. NN <-> ( ( |^ ` ( N / 2 ) ) e. ZZ /\ 1 <_ ( |^ ` ( N / 2 ) ) ) )
68 56 66 67 sylanbrc 
 |-  ( K e. NN -> ( |^ ` ( N / 2 ) ) e. NN )
69 61 64 breqtrrdi 
 |-  ( K e. NN -> K < ( |^ ` ( N / 2 ) ) )
70 elfzo1 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) )
71 7 68 69 70 syl3anbrc 
 |-  ( K e. NN -> K e. ( 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 e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( E e. ( Edg ` G ) <-> E. x e. ( 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. NN -> ( E e. ( Edg ` G ) <-> E. x e. ( 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. NN -> E e. ( Edg ` G ) )