Step |
Hyp |
Ref |
Expression |
1 |
|
gpg3kgrtriex.n |
|
2 |
|
gpg3kgrtriex.g |
Could not format G = ( N gPetersenGr K ) : No typesetting found for |- G = ( N gPetersenGr K ) with typecode |- |
3 |
|
1ex |
|
4 |
3
|
prid2 |
|
5 |
4
|
a1i |
|
6 |
|
3nn |
|
7 |
6
|
a1i |
|
8 |
|
id |
|
9 |
7 8
|
nnmulcld |
|
10 |
1 9
|
eqeltrid |
|
11 |
|
lbfzo0 |
|
12 |
10 11
|
sylibr |
|
13 |
5 12
|
opelxpd |
|
14 |
1
|
gpg3kgrtriexlem4 |
|
15 |
10 14
|
jca |
|
16 |
|
eqid |
|
17 |
|
eqid |
|
18 |
16 17
|
gpgvtx |
Could not format ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for |- ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode |- |
19 |
18
|
eleq2d |
Could not format ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) <-> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) ) : No typesetting found for |- ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) <-> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) ) with typecode |- |
20 |
15 19
|
syl |
Could not format ( K e. NN -> ( <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) <-> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) ) : No typesetting found for |- ( K e. NN -> ( <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) <-> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) ) with typecode |- |
21 |
13 20
|
mpbird |
Could not format ( K e. NN -> <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) ) : No typesetting found for |- ( K e. NN -> <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) ) with typecode |- |
22 |
2
|
fveq2i |
Could not format ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for |- ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) with typecode |- |
23 |
21 22
|
eleqtrrdi |
|
24 |
|
oveq2 |
|
25 |
|
biidd |
|
26 |
24 25
|
rexeqbidv |
|
27 |
24 26
|
rexeqbidv |
|
28 |
27
|
adantl |
|
29 |
1
|
gpg3kgrtriexlem3 |
|
30 |
|
eqid |
|
31 |
30
|
a1i |
|
32 |
31
|
olcd |
|
33 |
32 12
|
jca |
|
34 |
29 14
|
jca |
|
35 |
|
eqid |
|
36 |
17 16 2 35
|
opgpgvtx |
|
37 |
34 36
|
syl |
|
38 |
33 37
|
mpbird |
|
39 |
|
c0ex |
|
40 |
3 39
|
op1st |
|
41 |
40
|
a1i |
|
42 |
|
eqid |
|
43 |
16 2 35 42
|
gpgnbgrvtx1 |
|
44 |
29 14 38 41 43
|
syl22anc |
|
45 |
|
neeq1 |
|
46 |
|
preq1 |
|
47 |
46
|
eleq1d |
|
48 |
45 47
|
anbi12d |
|
49 |
|
neeq2 |
|
50 |
|
preq2 |
|
51 |
50
|
eleq1d |
|
52 |
49 51
|
anbi12d |
|
53 |
|
opex |
|
54 |
53
|
tpid1 |
|
55 |
|
eleq2 |
|
56 |
55
|
adantl |
|
57 |
54 56
|
mpbiri |
|
58 |
|
opex |
|
59 |
58
|
tpid3 |
|
60 |
|
eleq2 |
|
61 |
60
|
adantl |
|
62 |
59 61
|
mpbiri |
|
63 |
1
|
gpg3kgrtriexlem5 |
|
64 |
3 39
|
op2nd |
|
65 |
64
|
oveq1i |
|
66 |
|
nncn |
|
67 |
66
|
addlidd |
|
68 |
65 67
|
eqtrid |
|
69 |
68
|
oveq1d |
|
70 |
64
|
oveq1i |
|
71 |
70
|
a1i |
|
72 |
|
df-neg |
|
73 |
71 72
|
eqtr4di |
|
74 |
73
|
oveq1d |
|
75 |
63 69 74
|
3netr4d |
|
76 |
75
|
olcd |
|
77 |
|
ovex |
|
78 |
3 77
|
opthne |
|
79 |
76 78
|
sylibr |
|
80 |
64
|
a1i |
|
81 |
80
|
oveq1d |
|
82 |
81 67
|
eqtrd |
|
83 |
82
|
oveq1d |
|
84 |
83
|
opeq2d |
|
85 |
80
|
oveq1d |
|
86 |
85 72
|
eqtr4di |
|
87 |
86
|
oveq1d |
|
88 |
87
|
opeq2d |
|
89 |
84 88
|
preq12d |
|
90 |
|
eqid |
|
91 |
1 2 90
|
gpg3kgrtriexlem6 |
|
92 |
89 91
|
eqeltrd |
|
93 |
79 92
|
jca |
|
94 |
93
|
adantr |
|
95 |
48 52 57 62 94
|
2rspcedvdw |
|
96 |
44 95
|
mpdan |
|
97 |
23 28 96
|
rspcedvd |
|
98 |
|
gpgusgra |
Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) with typecode |- |
99 |
2 98
|
eqeltrid |
|
100 |
|
eqid |
|
101 |
|
eqid |
|
102 |
35 100 101
|
usgrgrtrirex |
Could not format ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( Vtx ` G ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) ) : No typesetting found for |- ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( Vtx ` G ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) ) with typecode |- |
103 |
34 99 102
|
3syl |
Could not format ( K e. NN -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( Vtx ` G ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) ) : No typesetting found for |- ( K e. NN -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( Vtx ` G ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) ) with typecode |- |
104 |
97 103
|
mpbird |
Could not format ( K e. NN -> E. t t e. ( GrTriangles ` G ) ) : No typesetting found for |- ( K e. NN -> E. t t e. ( GrTriangles ` G ) ) with typecode |- |