Step |
Hyp |
Ref |
Expression |
1 |
|
5eluz3 |
|
2 |
|
3z |
|
3 |
|
1lt3 |
|
4 |
|
eluz2b1 |
|
5 |
2 3 4
|
mpbir2an |
|
6 |
|
fzo1lb |
|
7 |
5 6
|
mpbir |
|
8 |
|
ceil5half3 |
|
9 |
8
|
eqcomi |
|
10 |
9
|
oveq2i |
|
11 |
7 10
|
eleqtri |
|
12 |
|
gpgusgra |
Could not format ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 1 ) e. USGraph ) : No typesetting found for |- ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 1 ) e. USGraph ) with typecode |- |
13 |
1 11 12
|
mp2an |
Could not format ( 5 gPetersenGr 1 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 1 ) e. USGraph with typecode |- |
14 |
|
2nn |
|
15 |
|
3nn |
|
16 |
|
2lt3 |
|
17 |
|
elfzo1 |
|
18 |
14 15 16 17
|
mpbir3an |
|
19 |
18 10
|
eleqtri |
|
20 |
|
gpgusgra |
Could not format ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph ) : No typesetting found for |- ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph ) with typecode |- |
21 |
1 19 20
|
mp2an |
Could not format ( 5 gPetersenGr 2 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USGraph with typecode |- |
22 |
|
2eluzge1 |
|
23 |
|
eluzfz1 |
|
24 |
22 23
|
ax-mp |
|
25 |
|
gpg5order |
Could not format ( 1 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 ) : No typesetting found for |- ( 1 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 ) with typecode |- |
26 |
24 25
|
ax-mp |
Could not format ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 : No typesetting found for |- ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 with typecode |- |
27 |
|
eluzfz2 |
|
28 |
22 27
|
ax-mp |
|
29 |
|
gpg5order |
Could not format ( 2 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) : No typesetting found for |- ( 2 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) with typecode |- |
30 |
28 29
|
ax-mp |
Could not format ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 : No typesetting found for |- ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 with typecode |- |
31 |
|
eqtr3 |
Could not format ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |- |
32 |
|
fvex |
Could not format ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V with typecode |- |
33 |
|
10nn0 |
|
34 |
|
hashvnfin |
Could not format ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) ) : No typesetting found for |- ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) ) with typecode |- |
35 |
32 33 34
|
mp2an |
Could not format ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) : No typesetting found for |- ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) with typecode |- |
36 |
|
fvex |
Could not format ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V with typecode |- |
37 |
|
hashvnfin |
Could not format ( ( ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) ) : No typesetting found for |- ( ( ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) ) with typecode |- |
38 |
36 33 37
|
mp2an |
Could not format ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) : No typesetting found for |- ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) with typecode |- |
39 |
|
hashen |
Could not format ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin /\ ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) <-> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin /\ ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) <-> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |- |
40 |
35 38 39
|
syl2an |
Could not format ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) <-> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) <-> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |- |
41 |
31 40
|
mpbid |
Could not format ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) with typecode |- |
42 |
26 30 41
|
mp2an |
Could not format ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) with typecode |- |
43 |
13 21 42
|
3pm3.2i |
Could not format ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) with typecode |- |
44 |
|
eqid |
Could not format ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) : No typesetting found for |- ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) with typecode |- |
45 |
44
|
gpg5gricstgr3 |
Could not format ( ( 1 e. ( 1 ... 2 ) /\ v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( ( 1 e. ( 1 ... 2 ) /\ v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) ) with typecode |- |
46 |
24 45
|
mpan |
Could not format ( v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) ) with typecode |- |
47 |
46
|
rgen |
Could not format A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) : No typesetting found for |- A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) with typecode |- |
48 |
|
eqid |
Could not format ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) : No typesetting found for |- ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) with typecode |- |
49 |
48
|
gpg5gricstgr3 |
Could not format ( ( 2 e. ( 1 ... 2 ) /\ w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( ( 2 e. ( 1 ... 2 ) /\ w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) with typecode |- |
50 |
28 49
|
mpan |
Could not format ( w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) with typecode |- |
51 |
50
|
rgen |
Could not format A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) : No typesetting found for |- A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) with typecode |- |
52 |
|
3nn0 |
|
53 |
|
eqid |
Could not format ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( Vtx ` ( 5 gPetersenGr 1 ) ) : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( Vtx ` ( 5 gPetersenGr 1 ) ) with typecode |- |
54 |
|
eqid |
Could not format ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( Vtx ` ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( Vtx ` ( 5 gPetersenGr 2 ) ) with typecode |- |
55 |
52 53 54
|
clnbgr3stgrgrlic |
Could not format ( ( ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) /\ A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) /\ A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) -> ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( ( ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) /\ A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) /\ A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) -> ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) ) with typecode |- |
56 |
43 47 51 55
|
mp3an |
Could not format ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) : No typesetting found for |- ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) with typecode |- |